From 184d8dfa4dd613993a9f27454c7d54852a1903bb Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Mon, 29 Jun 2026 19:42:21 +0100 Subject: [PATCH 1/6] feat(HeckeRing): add abstract Hecke ring definition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Port the core definitions of the abstract Hecke ring (following Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Ch. 3) from AINTLIB: the arithmetic pair HeckePair (H, Delta), the double-coset quotient HeckeCoset, and the Hecke ring type 𝕋 of formal Z-linear combinations of double cosets. Definitions only -- the convolution product and its properties are not included yet. Part of #75. Co-Authored-By: Claude Opus 4.8 (1M context) --- LeanBridge.lean | 1 + LeanBridge/ForMathlib/AbstractHeckeRing.lean | 75 ++++++++++++++++++++ 2 files changed, 76 insertions(+) create mode 100644 LeanBridge/ForMathlib/AbstractHeckeRing.lean diff --git a/LeanBridge.lean b/LeanBridge.lean index 9009ac5d..4acde80f 100644 --- a/LeanBridge.lean +++ b/LeanBridge.lean @@ -1 +1,2 @@ import LeanBridge.Example +import LeanBridge.ForMathlib.AbstractHeckeRing diff --git a/LeanBridge/ForMathlib/AbstractHeckeRing.lean b/LeanBridge/ForMathlib/AbstractHeckeRing.lean new file mode 100644 index 00000000..1b5829c0 --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing.lean @@ -0,0 +1,75 @@ +/- +Copyright (c) 2024 Chris Birkbeck. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Birkbeck +-/ +import Mathlib.GroupTheory.Commensurable +import Mathlib.GroupTheory.DoubleCoset +import Mathlib.Data.Finsupp.Pointwise + +/-! +# Hecke rings: definition + +The abstract Hecke ring, following Shimura, *Introduction to the Arithmetic Theory of +Automorphic Functions*, Ch. 3. + +This file contains only the core **definitions**: + +* `HeckeRing.HeckePair` — an arithmetic pair `(H, Δ)` with `H ≤ Δ ≤ commensurator(H)`; +* `HeckeRing.HeckeCoset` — the double-coset quotient `Δ / (HgH = HhH)`, the basis of the ring; +* `HeckeRing.𝕋` — the Hecke ring itself, formal `Z`-linear combinations of double cosets. + +The ring operations (convolution product) and their properties are intentionally **not** +included here; they will be added in follow-up work. + +Ported from the AINTLIB project +(`projects/LeanModularForms/LeanModularForms/HeckeRIngs/AbstractHeckeRing/Basic.lean`). +-/ + +open Set DoubleCoset Subgroup Subgroup.Commensurable + +open scoped Pointwise + +namespace HeckeRing + +variable {G : Type*} [Group G] + +/-- An arithmetic group pair `(H, Δ)` consisting of a subgroup `H` and a submonoid `Δ` +of a group `G`, satisfying `H ≤ Δ ≤ commensurator(H)`. -/ +@[ext] +structure HeckePair (G : Type*) [Group G] where + H : Subgroup G + Δ : Submonoid G + h₀ : H.toSubmonoid ≤ Δ + h₁ : Δ ≤ (commensurator H).toSubmonoid + +/-- Two elements of `Δ` define the same double coset `HgH = HhH`. -/ +def dcRel (P : HeckePair G) (g h : P.Δ) : Prop := + DoubleCoset.doubleCoset (g : G) P.H P.H = DoubleCoset.doubleCoset (h : G) P.H P.H + +/-- The setoid on `Δ` identifying elements with the same double coset. -/ +instance dcSetoid (P : HeckePair G) : Setoid P.Δ where + r := dcRel P + iseqv := ⟨fun _ ↦ rfl, Eq.symm, Eq.trans⟩ + +/-- A Hecke double coset: an equivalence class of `Δ`-elements under `HgH = HhH`. + This is the basis type for the Hecke ring. -/ +def HeckeCoset (P : HeckePair G) := Quotient (dcSetoid P) + +noncomputable instance instDecidableEqHeckeCoset (P : HeckePair G) : + DecidableEq (HeckeCoset P) := Classical.decEq _ + +/-- The Hecke ring type: formal `Z`-linear combinations of double cosets `HeckeCoset P`. -/ +def 𝕋 (P : HeckePair G) (Z : Type*) [CommRing Z] := Finsupp (HeckeCoset P) Z + +/-- `FunLike` instance for `𝕋 P Z`: treat elements as functions `HeckeCoset P → Z`. -/ +instance instFunLike𝕋 (P : HeckePair G) (Z : Type*) [CommRing Z] : + FunLike (𝕋 P Z) (HeckeCoset P) Z := + inferInstanceAs (FunLike (HeckeCoset P →₀ Z) (HeckeCoset P) Z) + +/-- The additive commutative group structure on the Hecke ring. -/ +noncomputable instance instAddCommGroup𝕋 (P : HeckePair G) (Z : Type*) [CommRing Z] : + AddCommGroup (𝕋 P Z) := + inferInstanceAs (AddCommGroup ((HeckeCoset P) →₀ Z)) + +end HeckeRing From 6275249ccd3e72f265cef33e6ea5d40dce1adc85 Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Mon, 29 Jun 2026 20:46:15 +0100 Subject: [PATCH 2/6] feat(CommensurableLimit): modular forms over a commensurability class + commensurator action MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Port from AINTLIB (self-contained on mathlib): the space of modular forms of weight k over the commensurability class of a fixed group Γ₀ as a direct limit, with the commensurator action and the level-invariants theorem. In its own folder LeanBridge/CommensurableLimit/, separate from the existing code. - CommensurabilityClass.lean: directed index `CommIndex Γ₀` (det-one subgroups commensurable with Γ₀, reverse-inclusion order) + gap lemmas `HasDetOne.of_le`, `commensurable_inf`, `commensurable_le_commensurator`. - DirectLimit.lean: `ModularFormCommensurable Γ₀ k := Module.DirectLimit (ModularForm Γ k)` over CommIndex Γ₀, with ofLevel / lift / injectivity; headline `ModularFormArithmetic` at 𝒮ℒ. - CommensuratorAction.lean: `PComm Γ₀ := commensurator Γ₀ ⊓ GL(2,ℝ)⁺` acts via the ℂ-linear slash-translate, bundled `commRep : Representation ℂ (PComm Γ₀) (limit)`; theorem `range_ofLevel_eq_invariants` — the Γ-invariants of the action are exactly `ModularForm Γ.carrier k`. Builds on mathlib v4.31.0; sorry-free; axioms only propext/Classical.choice/Quot.sound. Co-Authored-By: Claude Opus 4.8 (1M context) --- LeanBridge.lean | 1 + LeanBridge/CommensurableLimit.lean | 3 + .../CommensurabilityClass.lean | 105 ++++++ .../CommensuratorAction.lean | 315 ++++++++++++++++++ .../CommensurableLimit/DirectLimit.lean | 154 +++++++++ 5 files changed, 578 insertions(+) create mode 100644 LeanBridge/CommensurableLimit.lean create mode 100644 LeanBridge/CommensurableLimit/CommensurabilityClass.lean create mode 100644 LeanBridge/CommensurableLimit/CommensuratorAction.lean create mode 100644 LeanBridge/CommensurableLimit/DirectLimit.lean diff --git a/LeanBridge.lean b/LeanBridge.lean index 4acde80f..e5207c9c 100644 --- a/LeanBridge.lean +++ b/LeanBridge.lean @@ -1,2 +1,3 @@ import LeanBridge.Example import LeanBridge.ForMathlib.AbstractHeckeRing +import LeanBridge.CommensurableLimit diff --git a/LeanBridge/CommensurableLimit.lean b/LeanBridge/CommensurableLimit.lean new file mode 100644 index 00000000..9c23f220 --- /dev/null +++ b/LeanBridge/CommensurableLimit.lean @@ -0,0 +1,3 @@ +import LeanBridge.CommensurableLimit.CommensurabilityClass +import LeanBridge.CommensurableLimit.DirectLimit +import LeanBridge.CommensurableLimit.CommensuratorAction diff --git a/LeanBridge/CommensurableLimit/CommensurabilityClass.lean b/LeanBridge/CommensurableLimit/CommensurabilityClass.lean new file mode 100644 index 00000000..73fe4fae --- /dev/null +++ b/LeanBridge/CommensurableLimit/CommensurabilityClass.lean @@ -0,0 +1,105 @@ +/- +Copyright (c) 2026 Chris Birkbeck. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Birkbeck +-/ +import Mathlib.GroupTheory.Commensurable +import Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups + +/-! +# The commensurability class of a subgroup as a directed index + +Fix a subgroup `Γ₀ ≤ GL₂(ℝ)`. This file packages the subgroups commensurable with `Γ₀` that lie in +the determinant-one part as a **directed index type** `ModularForm.CommIndex Γ₀`, ordered by +*reverse* inclusion (`i ≤ j ↔ j.carrier ≤ i.carrier`). + +This is the index over which `CommensurableLimit/DirectLimit.lean` forms the direct limit of the +spaces `ModularForm Γ k`: the transition map `Mₖ(Γ) → Mₖ(Γ′)` exists exactly when `Γ′ ≤ Γ`, so the +diagram is covariant for the reverse-inclusion order, and the class being closed under intersection +makes the index directed. + +## Main definitions + +* `ModularForm.CommIndex Γ₀` — a subgroup of `GL₂(ℝ)` commensurable with `Γ₀` and determinant-one, + bundled with those two facts. + +## Main results + +* `Subgroup.HasDetOne.of_le` — `HasDetOne` is antitone: it passes to subgroups. +* `Subgroup.commensurable_inf` — the meet of two subgroups commensurable with `Γ₀` is commensurable + with `Γ₀` (general base; the body mirrors `Subgroup.IsArithmetic.inter`). +* `Preorder`, `Nonempty` and `IsDirected` (reverse inclusion) instances on `CommIndex Γ₀`, making it + a directed index for a direct limit. +-/ + +open scoped MatrixGroups + +namespace Subgroup + +/-- `HasDetOne` is antitone: a subgroup of a determinant-one subgroup is itself determinant-one. +(Mathlib only provides the `⊓` special cases; this is the general monotonicity.) -/ +theorem HasDetOne.of_le {n : Type*} [Fintype n] [DecidableEq n] {R : Type*} [CommRing R] + {Γ' Γ : Subgroup (GL n R)} (h : Γ' ≤ Γ) [Γ.HasDetOne] : Γ'.HasDetOne := + ⟨fun hg ↦ HasDetOne.det_eq (h hg)⟩ + +/-- The meet of two subgroups commensurable with a fixed `Γ₀` is again commensurable with `Γ₀`. -/ +theorem commensurable_inf {G : Type*} [Group G] {Γ₁ Γ₂ Γ₀ : Subgroup G} + (h₁ : Commensurable Γ₁ Γ₀) (h₂ : Commensurable Γ₂ Γ₀) : + Commensurable (Γ₁ ⊓ Γ₂) Γ₀ := by + refine ⟨relIndex_inf_ne_zero h₁.1 h₂.1, relIndex_ne_zero_trans (K := Γ₁) h₁.2 ?_⟩ + rw [relIndex_eq_one.mpr inf_le_left] + exact one_ne_zero + +end Subgroup + +namespace ModularForm + +open Subgroup + +/-- Index type for the commensurability-class direct limit: a subgroup of `GL₂(ℝ)` that is +commensurable with `Γ₀` and lies in the determinant-one part, bundled with those facts. + +Ordered by **reverse inclusion** (`i ≤ j ↔ j.carrier ≤ i.carrier`), so that the restriction maps of +the modular-form direct limit run in the direction of increasing `≤`. -/ +structure CommIndex (Γ₀ : Subgroup (GL (Fin 2) ℝ)) where + /-- the underlying subgroup -/ + carrier : Subgroup (GL (Fin 2) ℝ) + /-- it is commensurable with the fixed base `Γ₀` -/ + commensurable : Commensurable carrier Γ₀ + /-- it lies in the determinant-one part of `GL₂(ℝ)` -/ + hasDetOne : carrier.HasDetOne + +namespace CommIndex + +variable {Γ₀ : Subgroup (GL (Fin 2) ℝ)} + +/-- Every index carries the determinant-one structure of its underlying subgroup, so the spaces +`ModularForm i.carrier k` are `ℂ`-vector spaces. -/ +instance (i : CommIndex Γ₀) : i.carrier.HasDetOne := i.hasDetOne + +/-- Reverse-inclusion preorder: `i ≤ j` means `j.carrier ≤ i.carrier`. -/ +instance : Preorder (CommIndex Γ₀) where + le i j := j.carrier ≤ i.carrier + le_refl i := le_refl i.carrier + le_trans _ _ _ hij hjk := le_trans hjk hij + +@[simp] lemma le_def {i j : CommIndex Γ₀} : i ≤ j ↔ j.carrier ≤ i.carrier := Iff.rfl + +/-- The base `Γ₀` (when determinant-one) is itself an index, so the class is nonempty. -/ +instance [Γ₀.HasDetOne] : Nonempty (CommIndex Γ₀) := + ⟨⟨Γ₀, .refl Γ₀, inferInstance⟩⟩ + +/-- The commensurability class is directed under reverse inclusion: two indices have their meet as a +common upper bound (it is commensurable with `Γ₀` and determinant-one). -/ +instance : IsDirected (CommIndex Γ₀) (· ≤ ·) where + directed i j := + ⟨⟨i.carrier ⊓ j.carrier, commensurable_inf i.commensurable j.commensurable, inferInstance⟩, + le_def.mpr inf_le_left, le_def.mpr inf_le_right⟩ + +/-- `Module.DirectLimit` needs decidable equality on the index; subgroup equality is not decidable, +so we use the classical instance. -/ +noncomputable instance : DecidableEq (CommIndex Γ₀) := Classical.decEq _ + +end CommIndex + +end ModularForm diff --git a/LeanBridge/CommensurableLimit/CommensuratorAction.lean b/LeanBridge/CommensurableLimit/CommensuratorAction.lean new file mode 100644 index 00000000..2cc7a0a6 --- /dev/null +++ b/LeanBridge/CommensurableLimit/CommensuratorAction.lean @@ -0,0 +1,315 @@ +/- +Copyright (c) 2026 Chris Birkbeck. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Birkbeck +-/ +import LeanBridge.CommensurableLimit.DirectLimit +import Mathlib.RepresentationTheory.Invariants + +/-! +# The commensurator action on the direct limit, and its level invariants + +The commensurator `commensurator Γ₀` acts on `ModularFormCommensurable Γ₀ k` by the weight-`k` slash +action (a `g` sends the level-`Γ` piece to the level-`gΓg⁻¹` piece via `f ↦ f ∣[k] g⁻¹`). Because the +slash action is `ℂ`-linear only in positive determinant, the acting group is the positive-determinant +part `PComm Γ₀ := commensurator Γ₀ ⊓ GL(2,ℝ)⁺`. We prove that the `Γ`-invariants of the limit are +exactly `ModularForm Γ k` (the image of `ofLevel Γ`). + +## Main definitions + +* `ModularForm.PComm` — the positive-determinant part of the commensurator of `Γ₀` (the acting + group). +* `ModularForm.CommIndex.conj` — the conjugation action of a commensurator element on the index. +* `ModularForm.translateₗ` — slash by a positive-determinant `g` as a `ℂ`-linear map + `ModularForm Γ k → ModularForm (g⁻¹Γg) k`. +* `ModularFormCommensurable.smulMap` — the action of `g ∈ PComm Γ₀` on the direct limit. +* `ModularFormCommensurable.toFunₗ` — the injective `ℂ`-linear map from the limit to functions + `ℍ → ℂ`. +* `ModularFormCommensurable.commRep` — the weight-`k` representation of `PComm Γ₀` on the limit. +* `ModularFormCommensurable.ofLevelInvariantsEquiv` — the `ℂ`-linear isomorphism of + `ModularForm Γ.carrier k` with the level invariants. + +## Main results + +* `Subgroup.commensurable_le_commensurator` — a subgroup commensurable with `Γ₀` lies in its + commensurator. +* `ModularFormCommensurable.range_ofLevel_eq_invariants` — the level-`Γ` invariants of the + commensurator action are exactly the image of `ModularForm Γ.carrier k` under `ofLevel`. +-/ + +open scoped MatrixGroups Pointwise + +namespace Subgroup + +variable {G : Type*} [Group G] + +/-- A subgroup commensurable with `Γ₀` is contained in the commensurator of `Γ₀`. -/ +theorem commensurable_le_commensurator {Γ Γ₀ : Subgroup G} (h : Commensurable Γ Γ₀) : + Γ ≤ Commensurable.commensurator Γ₀ := by + intro g hg + rw [Commensurable.commensurator_mem_iff] + have hΓ : ConjAct.toConjAct g • Γ = Γ := by + ext x + rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ConjAct.smul_def, map_inv, + ConjAct.ofConjAct_toConjAct, inv_inv] + refine ⟨fun hx ↦ ?_, fun hx ↦ Γ.mul_mem (Γ.mul_mem (Γ.inv_mem hg) hx) hg⟩ + have hxx : x = g * (g⁻¹ * x * g) * g⁻¹ := by group + rw [hxx] + exact Γ.mul_mem (Γ.mul_mem hg hx) (Γ.inv_mem hg) + have h1 := h.symm.conj (ConjAct.toConjAct g) + rw [hΓ] at h1 + exact h1.trans h + +end Subgroup + +namespace ModularForm + +open Subgroup + +/-- Determinant-one passes to conjugates: if `Γ` has determinant one, so does any conjugate +`g • Γ` (the determinant is conjugation-invariant). -/ +instance HasDetOne.conj {g : GL (Fin 2) ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] : + (ConjAct.toConjAct g • Γ).HasDetOne := by + refine ⟨fun {x} hx ↦ ?_⟩ + rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem] at hx + simpa [ConjAct.smul_def, map_inv, ConjAct.ofConjAct_toConjAct, map_mul, mul_comm, mul_left_comm] + using HasDetOne.det_eq hx + +/-- The acting group of the commensurator action: the positive-determinant part of the commensurator +of `Γ₀`. (Positive determinant is exactly where the slash action is `ℂ`-linear.) -/ +noncomputable def PComm (Γ₀ : Subgroup (GL (Fin 2) ℝ)) : Subgroup (GL (Fin 2) ℝ) := + Commensurable.commensurator Γ₀ ⊓ Matrix.GLPos (Fin 2) ℝ + +namespace CommIndex + +variable {Γ₀ : Subgroup (GL (Fin 2) ℝ)} + +/-- The conjugation action of a commensurator element on the index of the direct limit: +`g` sends the level `Γ` to the conjugate level `gΓg⁻¹`, which stays in the commensurability class. -/ +def conj (g : GL (Fin 2) ℝ) (hg : g ∈ Commensurable.commensurator Γ₀) (i : CommIndex Γ₀) : + CommIndex Γ₀ where + carrier := ConjAct.toConjAct g • i.carrier + commensurable := (i.commensurable.conj (ConjAct.toConjAct g)).trans + ((Commensurable.commensurator_mem_iff Γ₀ g).mp hg) + hasDetOne := HasDetOne.conj + +@[simp] lemma conj_carrier (g : GL (Fin 2) ℝ) (hg : g ∈ Commensurable.commensurator Γ₀) + (i : CommIndex Γ₀) : (conj g hg i).carrier = ConjAct.toConjAct g • i.carrier := rfl + +end CommIndex + +/-- `σ g = id` for positive-determinant `g`, by unfolding `UpperHalfPlane.σ` +(`if 0 < det then refl else conj`); this is where the slash action is `ℂ`-linear. -/ +private lemma sigma_eq_refl_of_pos_det {g : GL (Fin 2) ℝ} (hg : 0 < g.det.val) : + UpperHalfPlane.σ g = ContinuousAlgEquiv.refl ℝ ℂ := if_pos hg + +variable {k : ℤ} + +/-- Translation by `g` (slash by `g`) as a `ℂ`-linear map +`ModularForm Γ k → ModularForm (g⁻¹Γg) k`, for positive-determinant `g` (where the slash action is +`ℂ`-linear, the `σ`-twist being trivial). The underlying function is `⇑f ∣[k] g`. -/ +noncomputable def translateₗ (g : GL (Fin 2) ℝ) (hg : 0 < g.det.val) + {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] : + ModularForm Γ k →ₗ[ℂ] ModularForm (ConjAct.toConjAct g⁻¹ • Γ) k where + toFun f := ModularForm.translate f g + map_add' f₁ f₂ := by + ext z + simp only [ModularForm.coe_translate, ModularForm.coe_add, SlashAction.add_slash, Pi.add_apply] + map_smul' c f := by + ext z + change (⇑(c • f) ∣[k] g) z = c • ((⇑f ∣[k] g) z) + simp only [show (⇑(c • f) : UpperHalfPlane → ℂ) = c • ⇑f from rfl, + ModularForm.smul_slash, sigma_eq_refl_of_pos_det hg, ContinuousAlgEquiv.refl_apply, + Pi.smul_apply, smul_eq_mul] + +@[simp] lemma coe_translateₗ (g : GL (Fin 2) ℝ) (hg : 0 < g.det.val) + {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (f : ModularForm Γ k) : + ⇑(translateₗ g hg f) = ⇑f ∣[k] g := rfl + +private lemma det_inv_pos {g : GL (Fin 2) ℝ} (hg : 0 < g.det.val) : 0 < (g⁻¹).det.val := by + rwa [map_inv, Units.val_inv_eq_inv_val, inv_pos] + +variable {Γ₀ : Subgroup (GL (Fin 2) ℝ)} + +/-- An element of `PComm Γ₀` lies in the commensurator of `Γ₀`. -/ +lemma mem_commensurator_of_mem_PComm (g : ↥(PComm Γ₀)) : + (g : GL (Fin 2) ℝ) ∈ Commensurable.commensurator Γ₀ := + (Subgroup.mem_inf.mp g.2).1 + +/-- An element of `PComm Γ₀` has positive determinant. -/ +lemma det_pos_of_mem_PComm (g : ↥(PComm Γ₀)) : 0 < (g : GL (Fin 2) ℝ).det.val := + (Matrix.mem_glpos _).mp (Subgroup.mem_inf.mp g.2).2 + +end ModularForm + +namespace ModularFormCommensurable + +open ModularForm + +variable (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] (k : ℤ) + +/-- The action of `g ∈ PComm Γ₀` on the direct limit: on the level-`i` piece it translates by `g⁻¹` +(a `ℂ`-linear map, as `g` has positive determinant) into the conjugate level `g i g⁻¹`. -/ +noncomputable def smulMap (g : ↥(PComm Γ₀)) : + ModularFormCommensurable Γ₀ k →ₗ[ℂ] ModularFormCommensurable Γ₀ k := + lift Γ₀ k + (fun i ↦ (ofLevel Γ₀ k (CommIndex.conj g.1 (mem_commensurator_of_mem_PComm g) i)).comp + (translateₗ g.1⁻¹ (det_inv_pos (det_pos_of_mem_PComm g)))) + (fun i j h x ↦ by + have hconj : CommIndex.conj g.1 (mem_commensurator_of_mem_PComm g) i + ≤ CommIndex.conj g.1 (mem_commensurator_of_mem_PComm g) j := by + rw [CommIndex.le_def, CommIndex.conj_carrier, CommIndex.conj_carrier] + exact Subgroup.pointwise_smul_le_pointwise_smul_iff.mpr (CommIndex.le_def.mp h) + have hcomm : translateₗ g.1⁻¹ (det_inv_pos (det_pos_of_mem_PComm g)) (restrictSubgroupₗ h x) + = restrictSubgroupₗ hconj + (translateₗ g.1⁻¹ (det_inv_pos (det_pos_of_mem_PComm g)) x) := by + ext z; rfl + simp only [LinearMap.comp_apply] + exact (congrArg (ofLevel Γ₀ k (CommIndex.conj g.1 (mem_commensurator_of_mem_PComm g) j)) + hcomm).trans + (ofLevel_restrict Γ₀ k hconj + (translateₗ g.1⁻¹ (det_inv_pos (det_pos_of_mem_PComm g)) x))) + +lemma smulMap_ofLevel (g : ↥(PComm Γ₀)) (i : CommIndex Γ₀) (f : ModularForm i.carrier k) : + smulMap Γ₀ k g (ofLevel Γ₀ k i f) + = ofLevel Γ₀ k (CommIndex.conj g.1 (mem_commensurator_of_mem_PComm g) i) + (translateₗ g.1⁻¹ (det_inv_pos (det_pos_of_mem_PComm g)) f) := + lift_ofLevel Γ₀ k _ _ i f + +/-- The `ℂ`-linear inclusion of a single level into functions `ℍ → ℂ`. -/ +def coeₗ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] : + ModularForm Γ k →ₗ[ℂ] (UpperHalfPlane → ℂ) where + toFun f := ⇑f + map_add' _ _ := rfl + map_smul' _ _ := rfl + +@[simp] lemma coeₗ_apply {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (f : ModularForm Γ k) : + coeₗ k f = ⇑f := rfl + +/-- Induction principle for the limit phrased with `ofLevel` rather than the raw +`Module.DirectLimit.of` (to which it is definitionally equal). -/ +@[elab_as_elim] +lemma ofLevel_induction {C : ModularFormCommensurable Γ₀ k → Prop} + (z : ModularFormCommensurable Γ₀ k) + (ih : ∀ (i : CommIndex Γ₀) (f : ModularForm i.carrier k), C (ofLevel Γ₀ k i f)) : C z := + Module.DirectLimit.induction_on z ih + +/-- Every element of the limit comes from some level. -/ +lemma exists_ofLevel (z : ModularFormCommensurable Γ₀ k) : + ∃ (i : CommIndex Γ₀) (f : ModularForm i.carrier k), ofLevel Γ₀ k i f = z := + Module.DirectLimit.exists_of z + +/-- The underlying-function map out of the limit: a form over the class restricts to an honest +function `ℍ → ℂ`. It is `ℂ`-linear and injective, and intertwines `smulMap g` with `· ∣[k] g⁻¹`. -/ +noncomputable def toFunₗ : ModularFormCommensurable Γ₀ k →ₗ[ℂ] (UpperHalfPlane → ℂ) := + lift Γ₀ k (fun _ ↦ coeₗ k) + (fun i j h x ↦ by simp only [coeₗ_apply, coe_restrictSubgroupₗ]) + +@[simp] lemma toFunₗ_ofLevel (i : CommIndex Γ₀) (f : ModularForm i.carrier k) : + toFunₗ Γ₀ k (ofLevel Γ₀ k i f) = ⇑f := by + unfold toFunₗ + simp only [lift_ofLevel, coeₗ_apply] + +lemma toFunₗ_injective : Function.Injective (toFunₗ Γ₀ k) := by + unfold toFunₗ lift + apply Module.DirectLimit.lift_injective + intro i a b hab + exact DFunLike.coe_injective hab + +lemma toFunₗ_smulMap (g : ↥(PComm Γ₀)) (x : ModularFormCommensurable Γ₀ k) : + toFunₗ Γ₀ k (smulMap Γ₀ k g x) = toFunₗ Γ₀ k x ∣[k] g.1⁻¹ := by + induction x using ofLevel_induction with + | ih i f => rw [smulMap_ofLevel, toFunₗ_ofLevel, toFunₗ_ofLevel]; rfl + +lemma smulMap_one : smulMap Γ₀ k (1 : ↥(PComm Γ₀)) = LinearMap.id := by + ext x + apply toFunₗ_injective + simp only [toFunₗ_smulMap, LinearMap.id_coe, id_eq, OneMemClass.coe_one, inv_one, + SlashAction.slash_one] + +lemma smulMap_mul (g h : ↥(PComm Γ₀)) : + smulMap Γ₀ k (g * h) = smulMap Γ₀ k g ∘ₗ smulMap Γ₀ k h := by + ext x + apply toFunₗ_injective + simp only [toFunₗ_smulMap, LinearMap.comp_apply, Subgroup.coe_mul, mul_inv_rev, + SlashAction.slash_mul] + +/-- The weight-`k` action of `PComm Γ₀` on `ModularFormCommensurable Γ₀ k` as a `ℂ`-linear +representation: `g` acts by the slash action of `g⁻¹` (well-defined and `ℂ`-linear because `g` has +positive determinant), permuting the levels by conjugation. -/ +noncomputable def commRep : Representation ℂ (↥(PComm Γ₀)) (ModularFormCommensurable Γ₀ k) where + toFun := smulMap Γ₀ k + map_one' := smulMap_one Γ₀ k + map_mul' := smulMap_mul Γ₀ k + +@[simp] lemma commRep_apply (g : ↥(PComm Γ₀)) : commRep Γ₀ k g = smulMap Γ₀ k g := rfl + +omit [Γ₀.HasDetOne] in +/-- A level (a determinant-one subgroup commensurable with `Γ₀`) lies in the acting group +`PComm Γ₀` — it is in the commensurator and, being determinant-one, has positive determinant. -/ +lemma carrier_le_PComm (Γ : CommIndex Γ₀) : Γ.carrier ≤ PComm Γ₀ := by + refine le_inf (Subgroup.commensurable_le_commensurator Γ.commensurable) (fun γ hγ ↦ ?_) + rw [Matrix.mem_glpos, show (γ.det : ℝˣ) = 1 from Subgroup.HasDetOne.det_eq hγ, Units.val_one] + exact one_pos + +omit [Γ₀.HasDetOne] in +/-- The inclusion of a level into the acting group `PComm Γ₀`. -/ +noncomputable def levelIncl (Γ : CommIndex Γ₀) : Γ.carrier →* ↥(PComm Γ₀) := + Subgroup.inclusion (carrier_le_PComm Γ₀ Γ) + +omit [Γ₀.HasDetOne] in +@[simp] lemma coe_levelIncl (Γ : CommIndex Γ₀) (γ : Γ.carrier) : + ((levelIncl Γ₀ Γ γ : ↥(PComm Γ₀)) : GL (Fin 2) ℝ) = (γ : GL (Fin 2) ℝ) := rfl + +/-- **The level invariants of the commensurator action are the modular forms of that level.** + +For a level `Γ` in the commensurability class, the image of `ModularForm Γ.carrier k` under `ofLevel` +is exactly the submodule of `ModularFormCommensurable Γ₀ k` fixed by the action of all of `Γ.carrier` +(restricted from the `commRep` action of `PComm Γ₀`). -/ +theorem range_ofLevel_eq_invariants (Γ : CommIndex Γ₀) : + LinearMap.range (ofLevel Γ₀ k Γ) + = Representation.invariants ((commRep Γ₀ k).comp (levelIncl Γ₀ Γ)) := by + apply le_antisymm + · rintro _ ⟨f, rfl⟩ + rw [Representation.mem_invariants] + intro γ + change smulMap Γ₀ k (levelIncl Γ₀ Γ γ) (ofLevel Γ₀ k Γ f) = ofLevel Γ₀ k Γ f + apply toFunₗ_injective + rw [toFunₗ_smulMap, toFunₗ_ofLevel, coe_levelIncl] + exact SlashInvariantForm.slash_action_eqn f _ (Γ.carrier.inv_mem γ.2) + · intro x hx + rw [Representation.mem_invariants] at hx + obtain ⟨Λ, f, rfl⟩ := exists_ofLevel Γ₀ k x + set Λ' : CommIndex Γ₀ := + ⟨Λ.carrier ⊓ Γ.carrier, Subgroup.commensurable_inf Λ.commensurable Γ.commensurable, + inferInstance⟩ + have hΛΛ' : Λ ≤ Λ' := CommIndex.le_def.mpr inf_le_left + have hΓΛ' : Γ ≤ Λ' := CommIndex.le_def.mpr inf_le_right + have hcomm : Subgroup.Commensurable Λ.carrier Γ.carrier := + Λ.commensurable.trans Γ.commensurable.symm + have key : ∀ g : Γ.carrier, (⇑f : UpperHalfPlane → ℂ) ∣[k] (g : GL (Fin 2) ℝ)⁻¹ = ⇑f := by + intro g + have h2 := congrArg (toFunₗ Γ₀ k) (hx g) + rwa [MonoidHom.comp_apply, commRep_apply, toFunₗ_smulMap, toFunₗ_ofLevel, + coe_levelIncl] at h2 + let F : ModularForm Γ.carrier k := + { toFun := ⇑f + slash_action_eq' := fun δ hδ ↦ by + simpa only [inv_inv] using key ⟨δ⁻¹, Γ.carrier.inv_mem hδ⟩ + holo' := f.holo' + bdd_at_cusps' := fun {c} hc ↦ + f.bdd_at_cusps' ((Subgroup.Commensurable.isCusp_iff hcomm).mpr hc) } + refine ⟨F, ?_⟩ + have e1 : restrictSubgroupₗ hΓΛ' F = restrictSubgroupₗ hΛΛ' f := by ext z; rfl + rw [← ofLevel_restrict Γ₀ k hΓΛ' F, e1] + exact ofLevel_restrict Γ₀ k hΛΛ' f + +/-- **Corollary.** `ModularForm Γ.carrier k` is `ℂ`-linearly isomorphic to the `Γ.carrier`-invariants +of the limit, via `ofLevel`. -/ +noncomputable def ofLevelInvariantsEquiv (Γ : CommIndex Γ₀) : + ModularForm Γ.carrier k ≃ₗ[ℂ] + Representation.invariants ((commRep Γ₀ k).comp (levelIncl Γ₀ Γ)) := + (LinearEquiv.ofInjective (ofLevel Γ₀ k Γ) (ofLevel_injective Γ₀ k Γ)).trans + (LinearEquiv.ofEq _ _ (range_ofLevel_eq_invariants Γ₀ k Γ)) + +end ModularFormCommensurable diff --git a/LeanBridge/CommensurableLimit/DirectLimit.lean b/LeanBridge/CommensurableLimit/DirectLimit.lean new file mode 100644 index 00000000..dceef7f5 --- /dev/null +++ b/LeanBridge/CommensurableLimit/DirectLimit.lean @@ -0,0 +1,154 @@ +/- +Copyright (c) 2026 Chris Birkbeck. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Birkbeck +-/ +import LeanBridge.CommensurableLimit.CommensurabilityClass +import Mathlib.Algebra.Colimit.Module +import Mathlib.NumberTheory.ModularForms.Basic + +/-! +# Modular forms of weight `k` over a commensurability class, as a direct limit + +Fix `Γ₀ ≤ GL₂(ℝ)` in the determinant-one part. For each subgroup `Γ` commensurable with `Γ₀` (and +determinant-one) we have the space `ModularForm Γ k`, and for `Γ′ ≤ Γ` the restriction map +`ModularForm Γ k → ModularForm Γ′ k` (a form invariant under the bigger group is invariant under the +smaller one). Indexed by `ModularForm.CommIndex Γ₀` under reverse inclusion — a directed poset — +this is a directed system of `ℂ`-vector spaces, and we define + +`ModularFormCommensurable Γ₀ k` := its `Module.DirectLimit`. + +For `Γ₀ = 𝒮ℒ` (the image of `SL₂(ℤ)`) this is the space of modular forms of weight `k` for *some* +group commensurable with `SL₂(ℤ)` — the natural space on which the commensurator (Hecke) action +lives; see `ModularFormArithmetic`. + +## Main definitions + +* `ModularForm.restrictSubgroupₗ` — restriction along `Γ′ ≤ Γ` as a `ℂ`-linear map. +* `ModularFormCommensurable Γ₀ k` — the direct limit; an `AddCommGroup` and a `Module ℂ`. +* `ModularFormCommensurable.ofLevel` — the canonical map of each level into the limit. +* `ModularFormCommensurable.lift` — the universal property out of the limit. +* `ModularFormArithmetic k` — the headline instance at `Γ₀ = 𝒮ℒ`. + +## Main results + +* `ModularFormCommensurable.ofLevel_restrict` — compatibility of `ofLevel` with restriction. +* `ModularFormCommensurable.ofLevel_injective` — each level embeds into the limit. +* `ModularFormCommensurable.lift_ofLevel` — computation rule for `lift`. +-/ + +open scoped MatrixGroups + +namespace ModularForm + +variable {k : ℤ} + +/-- Restriction of a modular form along a subgroup inclusion `Γ′ ≤ Γ`, as a `ℂ`-linear map. + +The unbundled version is `ModularForm.restrictSubgroup` +(`LeanModularForms/HeckeRIngs/GL2/LevelRaise.lean`); this is its `ℂ`-linear packaging, reproduced +here so the direct-limit construction depends only on mathlib. The underlying function is unchanged, +so additivity and `ℂ`-homogeneity are definitional. -/ +def restrictSubgroupₗ {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] [Γ'.HasDetOne] + (h : Γ' ≤ Γ) : ModularForm Γ k →ₗ[ℂ] ModularForm Γ' k where + toFun f := + { toFun := f.toFun + slash_action_eq' := fun γ hγ ↦ f.slash_action_eq' γ (h hγ) + holo' := f.holo' + bdd_at_cusps' := fun hc ↦ f.bdd_at_cusps' (hc.mono h) } + map_add' f g := by ext z; rfl + map_smul' c f := by ext z; rfl + +@[simp] +lemma coe_restrictSubgroupₗ {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] [Γ'.HasDetOne] + (h : Γ' ≤ Γ) (f : ModularForm Γ k) : ⇑(restrictSubgroupₗ h f) = ⇑f := rfl + +lemma restrictSubgroupₗ_injective {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] [Γ'.HasDetOne] + (h : Γ' ≤ Γ) : Function.Injective (restrictSubgroupₗ (k := k) h) := by + intro f g hfg + ext z + simpa using DFunLike.congr_fun hfg z + +end ModularForm + +open ModularForm + +/-- The transition maps of the commensurability-class directed system: for `i ≤ j` (i.e. +`j.carrier ≤ i.carrier`), restriction `ModularForm i.carrier k → ModularForm j.carrier k`. -/ +noncomputable def commTransition (Γ₀ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) : + ∀ i j : CommIndex Γ₀, i ≤ j → (ModularForm i.carrier k →ₗ[ℂ] ModularForm j.carrier k) := + fun _ _ h ↦ ModularForm.restrictSubgroupₗ h + +/-- The restriction maps form a directed system (each is the identity on underlying functions). -/ +instance commDirectedSystem (Γ₀ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) : + DirectedSystem (fun i : CommIndex Γ₀ ↦ ModularForm i.carrier k) + (fun i j h ↦ (commTransition Γ₀ k i j h : + ModularForm i.carrier k → ModularForm j.carrier k)) where + map_self := by intros; ext z; rfl + map_map := by intros; ext z; rfl + +/-- **Modular forms of weight `k` over the commensurability class of `Γ₀`**, defined as the direct +limit of `ModularForm Γ k` over all determinant-one subgroups `Γ` commensurable with `Γ₀`, ordered +by reverse inclusion with restriction as the transition maps. -/ +noncomputable def ModularFormCommensurable (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] + (k : ℤ) : Type := + Module.DirectLimit (fun i : CommIndex Γ₀ ↦ ModularForm i.carrier k) (commTransition Γ₀ k) + +namespace ModularFormCommensurable + +noncomputable instance (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] (k : ℤ) : + AddCommGroup (ModularFormCommensurable Γ₀ k) := + inferInstanceAs (AddCommGroup + (Module.DirectLimit (fun i : CommIndex Γ₀ ↦ ModularForm i.carrier k) (commTransition Γ₀ k))) + +noncomputable instance (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] (k : ℤ) : + Module ℂ (ModularFormCommensurable Γ₀ k) := + inferInstanceAs (Module ℂ + (Module.DirectLimit (fun i : CommIndex Γ₀ ↦ ModularForm i.carrier k) (commTransition Γ₀ k))) + +variable (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] (k : ℤ) + +/-- The canonical `ℂ`-linear map of the level-`i` modular forms into the direct limit. -/ +noncomputable def ofLevel (i : CommIndex Γ₀) : + ModularForm i.carrier k →ₗ[ℂ] ModularFormCommensurable Γ₀ k := + Module.DirectLimit.of ℂ (CommIndex Γ₀) (fun i ↦ ModularForm i.carrier k) (commTransition Γ₀ k) i + +/-- `ofLevel` is compatible with restriction: restricting to a finer level then including agrees +with including directly. -/ +@[simp] +lemma ofLevel_restrict {i j : CommIndex Γ₀} (h : i ≤ j) (f : ModularForm i.carrier k) : + ofLevel Γ₀ k j (restrictSubgroupₗ h f) = ofLevel Γ₀ k i f := + Module.DirectLimit.of_f + +/-- Each level embeds into the direct limit: `ofLevel` is injective. -/ +lemma ofLevel_injective (i : CommIndex Γ₀) : Function.Injective (ofLevel Γ₀ k i) := by + intro x y hxy + obtain ⟨j, hij, hj⟩ := Module.DirectLimit.exists_eq_of_of_eq hxy + exact restrictSubgroupₗ_injective hij hj + +/-- **Universal property**: a family of `ℂ`-linear maps `gᵢ : ModularForm i.carrier k → P` that is +compatible with restriction factors (uniquely) through the direct limit. -/ +noncomputable def lift {P : Type*} [AddCommGroup P] [Module ℂ P] + (g : ∀ i : CommIndex Γ₀, ModularForm i.carrier k →ₗ[ℂ] P) + (Hg : ∀ (i j : CommIndex Γ₀) (h : i ≤ j) (x : ModularForm i.carrier k), + g j (restrictSubgroupₗ h x) = g i x) : + ModularFormCommensurable Γ₀ k →ₗ[ℂ] P := + Module.DirectLimit.lift ℂ (CommIndex Γ₀) (fun i ↦ ModularForm i.carrier k) (commTransition Γ₀ k) + g Hg + +@[simp] +lemma lift_ofLevel {P : Type*} [AddCommGroup P] [Module ℂ P] + (g : ∀ i : CommIndex Γ₀, ModularForm i.carrier k →ₗ[ℂ] P) + (Hg : ∀ (i j : CommIndex Γ₀) (h : i ≤ j) (x : ModularForm i.carrier k), + g j (restrictSubgroupₗ h x) = g i x) + (i : CommIndex Γ₀) (x : ModularForm i.carrier k) : + lift Γ₀ k g Hg (ofLevel Γ₀ k i x) = g i x := + Module.DirectLimit.lift_of _ _ _ + +end ModularFormCommensurable + +/-- **Modular forms of weight `k` over the commensurability class of `SL₂(ℤ)`** (i.e. `Γ₀ = 𝒮ℒ`, the +image of `SL₂(ℤ)` in `GL₂(ℝ)`). The indexing class is exactly the determinant-one subgroups `Γ` with +`Subgroup.IsArithmetic Γ`. -/ +noncomputable abbrev ModularFormArithmetic (k : ℤ) : Type := + ModularFormCommensurable 𝒮ℒ k From 76398bf2602e9a40e25544d070b28251af2fdbde Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Tue, 30 Jun 2026 16:34:16 +0100 Subject: [PATCH 3/6] feat(CommensurableLimit): relax ModularFormCommensurable base to HasDetPlusMinusOne MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The base Γ₀ of ModularFormCommensurable only needs det = ±1, not det = 1: the ℂ-vector-space structure of the direct limit comes from the index subgroups (CommIndex.carrier, each HasDetOne), not from Γ₀. So weaken the hypothesis [Γ₀.HasDetOne] to [Γ₀.HasDetPlusMinusOne] on the def and its AddCommGroup/Module instances. ModularFormArithmetic (Γ₀ = 𝒮ℒ) is unaffected since HasDetOne ⇒ HasDetPlusMinusOne. Co-Authored-By: Claude Opus 4.8 (1M context) --- LeanBridge/CommensurableLimit/DirectLimit.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/LeanBridge/CommensurableLimit/DirectLimit.lean b/LeanBridge/CommensurableLimit/DirectLimit.lean index dceef7f5..5dec6c9b 100644 --- a/LeanBridge/CommensurableLimit/DirectLimit.lean +++ b/LeanBridge/CommensurableLimit/DirectLimit.lean @@ -10,8 +10,7 @@ import Mathlib.NumberTheory.ModularForms.Basic /-! # Modular forms of weight `k` over a commensurability class, as a direct limit -Fix `Γ₀ ≤ GL₂(ℝ)` in the determinant-one part. For each subgroup `Γ` commensurable with `Γ₀` (and -determinant-one) we have the space `ModularForm Γ k`, and for `Γ′ ≤ Γ` the restriction map +Fix `Γ₀ ≤ GL₂(ℝ)` with `det = ±1`. For each determinant-one subgroup `Γ` commensurable with `Γ₀` we have the space `ModularForm Γ k`, and for `Γ′ ≤ Γ` the restriction map `ModularForm Γ k → ModularForm Γ′ k` (a form invariant under the bigger group is invariant under the smaller one). Indexed by `ModularForm.CommIndex Γ₀` under reverse inclusion — a directed poset — this is a directed system of `ℂ`-vector spaces, and we define @@ -90,23 +89,23 @@ instance commDirectedSystem (Γ₀ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) : /-- **Modular forms of weight `k` over the commensurability class of `Γ₀`**, defined as the direct limit of `ModularForm Γ k` over all determinant-one subgroups `Γ` commensurable with `Γ₀`, ordered by reverse inclusion with restriction as the transition maps. -/ -noncomputable def ModularFormCommensurable (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] +noncomputable def ModularFormCommensurable (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetPlusMinusOne] (k : ℤ) : Type := Module.DirectLimit (fun i : CommIndex Γ₀ ↦ ModularForm i.carrier k) (commTransition Γ₀ k) namespace ModularFormCommensurable -noncomputable instance (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] (k : ℤ) : +noncomputable instance (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetPlusMinusOne] (k : ℤ) : AddCommGroup (ModularFormCommensurable Γ₀ k) := inferInstanceAs (AddCommGroup (Module.DirectLimit (fun i : CommIndex Γ₀ ↦ ModularForm i.carrier k) (commTransition Γ₀ k))) -noncomputable instance (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] (k : ℤ) : +noncomputable instance (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetPlusMinusOne] (k : ℤ) : Module ℂ (ModularFormCommensurable Γ₀ k) := inferInstanceAs (Module ℂ (Module.DirectLimit (fun i : CommIndex Γ₀ ↦ ModularForm i.carrier k) (commTransition Γ₀ k))) -variable (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] (k : ℤ) +variable (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetPlusMinusOne] (k : ℤ) /-- The canonical `ℂ`-linear map of the level-`i` modular forms into the direct limit. -/ noncomputable def ofLevel (i : CommIndex Γ₀) : From cd536ebe6d84174393737c375aace97fb145ae52 Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Tue, 30 Jun 2026 17:23:03 +0100 Subject: [PATCH 4/6] =?UTF-8?q?feat(CommensurableLimit):=20make=20commRep?= =?UTF-8?q?=20an=20=E2=84=9D-representation=20of=20the=20whole=20commensur?= =?UTF-8?q?ator?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Generalize the commensurator action from the positive-determinant part PComm = commensurator ⊓ GLPos (a ℂ-representation) to the FULL commensurator (an ℝ-representation). A det < 0 commensurator element acts by the slash action with σ = complex conjugation, which is ℝ-linear but not ℂ-linear, so the representation is over ℝ; ModularFormCommensurable stays a ℂ-vector space (the ℝ-structure is restriction of scalars). - add translateℝ: ℝ-linear translate for any determinant (replaces translateₗ) - build the ℝ-linear smulMap on the ℂ-direct-limit via an ℝ-linear equiv to the same system rebuilt over ℝ (Module.DirectLimit ℝ) - commRep : Representation ℝ (commensurator Γ₀) (ModularFormCommensurable Γ₀ k) - update smulMap_one/_mul, toFunₗ_smulMap, range_ofLevel_eq_invariants, ofLevelInvariantsEquiv (now ≃ₗ[ℝ]); drop PComm and the det>0 machinery Co-Authored-By: Claude Opus 4.8 (1M context) --- .../CommensuratorAction.lean | 235 ++++++++++-------- 1 file changed, 137 insertions(+), 98 deletions(-) diff --git a/LeanBridge/CommensurableLimit/CommensuratorAction.lean b/LeanBridge/CommensurableLimit/CommensuratorAction.lean index 2cc7a0a6..c5b83084 100644 --- a/LeanBridge/CommensurableLimit/CommensuratorAction.lean +++ b/LeanBridge/CommensurableLimit/CommensuratorAction.lean @@ -10,23 +10,24 @@ import Mathlib.RepresentationTheory.Invariants # The commensurator action on the direct limit, and its level invariants The commensurator `commensurator Γ₀` acts on `ModularFormCommensurable Γ₀ k` by the weight-`k` slash -action (a `g` sends the level-`Γ` piece to the level-`gΓg⁻¹` piece via `f ↦ f ∣[k] g⁻¹`). Because the -slash action is `ℂ`-linear only in positive determinant, the acting group is the positive-determinant -part `PComm Γ₀ := commensurator Γ₀ ⊓ GL(2,ℝ)⁺`. We prove that the `Γ`-invariants of the limit are -exactly `ModularForm Γ k` (the image of `ofLevel Γ`). +action (a `g` sends the level-`Γ` piece to the level-`gΓg⁻¹` piece via `f ↦ f ∣[k] g⁻¹`). For an +element of *negative* determinant the slash action carries a `σ`-twist by complex conjugation, so it +is only `ℝ`-linear (`ℂ`-conjugate-linear) rather than `ℂ`-linear. We therefore view +`ModularFormCommensurable Γ₀ k` as an `ℝ`-vector space (by restriction of scalars from its +`ℂ`-structure) and build the action as a `Representation ℝ` of the *whole* commensurator. We prove +that the `Γ`-invariants of the limit are exactly `ModularForm Γ k` (the image of `ofLevel Γ`). ## Main definitions -* `ModularForm.PComm` — the positive-determinant part of the commensurator of `Γ₀` (the acting - group). * `ModularForm.CommIndex.conj` — the conjugation action of a commensurator element on the index. -* `ModularForm.translateₗ` — slash by a positive-determinant `g` as a `ℂ`-linear map - `ModularForm Γ k → ModularForm (g⁻¹Γg) k`. -* `ModularFormCommensurable.smulMap` — the action of `g ∈ PComm Γ₀` on the direct limit. +* `ModularForm.translateℝ` — slash by an arbitrary `g ∈ GL(2,ℝ)` (either determinant sign) as an + `ℝ`-linear map `ModularForm Γ k → ModularForm (g⁻¹Γg) k`. +* `ModularFormCommensurable.smulMap` — the `ℝ`-linear action of `g ∈ commensurator Γ₀` on the limit. * `ModularFormCommensurable.toFunₗ` — the injective `ℂ`-linear map from the limit to functions `ℍ → ℂ`. -* `ModularFormCommensurable.commRep` — the weight-`k` representation of `PComm Γ₀` on the limit. -* `ModularFormCommensurable.ofLevelInvariantsEquiv` — the `ℂ`-linear isomorphism of +* `ModularFormCommensurable.commRep` — the weight-`k` `ℝ`-representation of `commensurator Γ₀` on the + limit. +* `ModularFormCommensurable.ofLevelInvariantsEquiv` — the `ℝ`-linear isomorphism of `ModularForm Γ.carrier k` with the level invariants. ## Main results @@ -35,6 +36,15 @@ exactly `ModularForm Γ k` (the image of `ofLevel Γ`). commensurator. * `ModularFormCommensurable.range_ofLevel_eq_invariants` — the level-`Γ` invariants of the commensurator action are exactly the image of `ModularForm Γ.carrier k` under `ofLevel`. + +## Implementation notes + +`ModularFormCommensurable Γ₀ k` is a `ℂ`-vector space built as a `Module.DirectLimit` over `ℂ`, and +the `ℂ`-linear universal property (`lift`) cannot produce the merely-`ℝ`-linear maps coming from +negative-determinant elements. To build the `ℝ`-linear `smulMap` we transport the `ℝ`-linear +universal property along the canonical `ℝ`-linear isomorphism `equivℝ` between the `ℂ`-built limit +and the same directed system rebuilt over `ℝ` (by `restrictScalars`); the two limits agree because +the components and the transition maps are unchanged — only the scalar ring is restricted. -/ open scoped MatrixGroups Pointwise @@ -75,11 +85,6 @@ instance HasDetOne.conj {g : GL (Fin 2) ℝ} {Γ : Subgroup (GL (Fin 2) ℝ)} [ simpa [ConjAct.smul_def, map_inv, ConjAct.ofConjAct_toConjAct, map_mul, mul_comm, mul_left_comm] using HasDetOne.det_eq hx -/-- The acting group of the commensurator action: the positive-determinant part of the commensurator -of `Γ₀`. (Positive determinant is exactly where the slash action is `ℂ`-linear.) -/ -noncomputable def PComm (Γ₀ : Subgroup (GL (Fin 2) ℝ)) : Subgroup (GL (Fin 2) ℝ) := - Commensurable.commensurator Γ₀ ⊓ Matrix.GLPos (Fin 2) ℝ - namespace CommIndex variable {Γ₀ : Subgroup (GL (Fin 2) ℝ)} @@ -98,83 +103,114 @@ def conj (g : GL (Fin 2) ℝ) (hg : g ∈ Commensurable.commensurator Γ₀) (i end CommIndex -/-- `σ g = id` for positive-determinant `g`, by unfolding `UpperHalfPlane.σ` -(`if 0 < det then refl else conj`); this is where the slash action is `ℂ`-linear. -/ -private lemma sigma_eq_refl_of_pos_det {g : GL (Fin 2) ℝ} (hg : 0 < g.det.val) : - UpperHalfPlane.σ g = ContinuousAlgEquiv.refl ℝ ℂ := if_pos hg - variable {k : ℤ} -/-- Translation by `g` (slash by `g`) as a `ℂ`-linear map -`ModularForm Γ k → ModularForm (g⁻¹Γg) k`, for positive-determinant `g` (where the slash action is -`ℂ`-linear, the `σ`-twist being trivial). The underlying function is `⇑f ∣[k] g`. -/ -noncomputable def translateₗ (g : GL (Fin 2) ℝ) (hg : 0 < g.det.val) - {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] : - ModularForm Γ k →ₗ[ℂ] ModularForm (ConjAct.toConjAct g⁻¹ • Γ) k where +open ConjAct Pointwise UpperHalfPlane in +/-- `ℝ`-linear translate for ANY `g ∈ GL(2,ℝ)` (either determinant sign): the slash action is +`σ`-semilinear and `σ` fixes `ℝ`, so it is `ℝ`-linear regardless of `det g`. The underlying function +is `⇑f ∣[k] g`. -/ +noncomputable def translateℝ (g : GL (Fin 2) ℝ) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] : + ModularForm Γ k →ₗ[ℝ] ModularForm (toConjAct g⁻¹ • Γ) k where toFun f := ModularForm.translate f g map_add' f₁ f₂ := by ext z simp only [ModularForm.coe_translate, ModularForm.coe_add, SlashAction.add_slash, Pi.add_apply] map_smul' c f := by ext z - change (⇑(c • f) ∣[k] g) z = c • ((⇑f ∣[k] g) z) - simp only [show (⇑(c • f) : UpperHalfPlane → ℂ) = c • ⇑f from rfl, - ModularForm.smul_slash, sigma_eq_refl_of_pos_det hg, ContinuousAlgEquiv.refl_apply, - Pi.smul_apply, smul_eq_mul] - -@[simp] lemma coe_translateₗ (g : GL (Fin 2) ℝ) (hg : 0 < g.det.val) - {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] (f : ModularForm Γ k) : - ⇑(translateₗ g hg f) = ⇑f ∣[k] g := rfl + simp only [RingHom.id_apply, ModularForm.coe_translate, ModularForm.coe_smul] + have h : ((c • ⇑f : UpperHalfPlane → ℂ)) ∣[k] g = c • ((⇑f : UpperHalfPlane → ℂ) ∣[k] g) := by + rw [← smul_one_smul ℂ c (⇑f : UpperHalfPlane → ℂ), smul_slash, + ← smul_one_smul ℂ c ((⇑f : UpperHalfPlane → ℂ) ∣[k] g)] + congr 1 + rw [Complex.real_smul, mul_one, σ_ofReal] + exact congrFun h z -private lemma det_inv_pos {g : GL (Fin 2) ℝ} (hg : 0 < g.det.val) : 0 < (g⁻¹).det.val := by - rwa [map_inv, Units.val_inv_eq_inv_val, inv_pos] - -variable {Γ₀ : Subgroup (GL (Fin 2) ℝ)} - -/-- An element of `PComm Γ₀` lies in the commensurator of `Γ₀`. -/ -lemma mem_commensurator_of_mem_PComm (g : ↥(PComm Γ₀)) : - (g : GL (Fin 2) ℝ) ∈ Commensurable.commensurator Γ₀ := - (Subgroup.mem_inf.mp g.2).1 - -/-- An element of `PComm Γ₀` has positive determinant. -/ -lemma det_pos_of_mem_PComm (g : ↥(PComm Γ₀)) : 0 < (g : GL (Fin 2) ℝ).det.val := - (Matrix.mem_glpos _).mp (Subgroup.mem_inf.mp g.2).2 +@[simp] lemma coe_translateℝ (g : GL (Fin 2) ℝ) {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] + (f : ModularForm Γ k) : ⇑(translateℝ g f) = ⇑f ∣[k] g := rfl end ModularForm namespace ModularFormCommensurable -open ModularForm +open ModularForm Subgroup + +/-- The `ℝ`-vector-space structure on the limit, by restriction of scalars from its `ℂ`-structure +(via `algebraMap ℝ ℂ`). The negative-determinant part of the commensurator acts only `ℝ`-linearly, +so the representation lives over `ℝ`. -/ +noncomputable instance instModuleReal (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetPlusMinusOne] + (k : ℤ) : Module ℝ (ModularFormCommensurable Γ₀ k) := + Module.compHom _ (algebraMap ℝ ℂ) + +instance (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetPlusMinusOne] (k : ℤ) : + IsScalarTower ℝ ℂ (ModularFormCommensurable Γ₀ k) where + smul_assoc r c m := by + show (algebraMap ℝ ℂ r * c) • m = algebraMap ℝ ℂ r • (c • m) + rw [mul_smul] variable (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] (k : ℤ) -/-- The action of `g ∈ PComm Γ₀` on the direct limit: on the level-`i` piece it translates by `g⁻¹` -(a `ℂ`-linear map, as `g` has positive determinant) into the conjugate level `g i g⁻¹`. -/ -noncomputable def smulMap (g : ↥(PComm Γ₀)) : - ModularFormCommensurable Γ₀ k →ₗ[ℂ] ModularFormCommensurable Γ₀ k := - lift Γ₀ k - (fun i ↦ (ofLevel Γ₀ k (CommIndex.conj g.1 (mem_commensurator_of_mem_PComm g) i)).comp - (translateₗ g.1⁻¹ (det_inv_pos (det_pos_of_mem_PComm g)))) +/-- The transition maps of the directed system, made `ℝ`-linear by restriction of scalars; the +underlying functions are unchanged. -/ +private noncomputable def commTransitionℝ : + ∀ i j : CommIndex Γ₀, i ≤ j → (ModularForm i.carrier k →ₗ[ℝ] ModularForm j.carrier k) := + fun _ _ h ↦ (restrictSubgroupₗ h).restrictScalars ℝ + +/-- The same directed system rebuilt over `ℝ`. Auxiliary: only used to transport the `ℝ`-linear +universal property to the `ℂ`-built limit `ModularFormCommensurable Γ₀ k`. -/ +private noncomputable abbrev limℝ : Type := + Module.DirectLimit (fun i : CommIndex Γ₀ ↦ ModularForm i.carrier k) (commTransitionℝ Γ₀ k) + +/-- The canonical `ℝ`-linear map from the `ℝ`-built limit to the `ℂ`-built limit: it sends each +level-`i` piece to itself, with scalars restricted. -/ +private noncomputable def fromLimℝ : limℝ Γ₀ k →ₗ[ℝ] ModularFormCommensurable Γ₀ k := + Module.DirectLimit.lift ℝ (CommIndex Γ₀) _ (commTransitionℝ Γ₀ k) + (fun i ↦ (ofLevel Γ₀ k i).restrictScalars ℝ) (fun _ _ h x ↦ ofLevel_restrict Γ₀ k h x) + +/-- The canonical `ℝ`-linear isomorphism between the `ℂ`-built limit and the `ℝ`-built limit: both +glue the same components along the same (scalar-restricted) transition maps. -/ +private noncomputable def equivℝ : ModularFormCommensurable Γ₀ k ≃ₗ[ℝ] limℝ Γ₀ k := + (LinearEquiv.ofBijective (fromLimℝ Γ₀ k) + ⟨Module.DirectLimit.lift_injective _ _ (fun i ↦ ofLevel_injective Γ₀ k i), fun y ↦ by + obtain ⟨i, x, rfl⟩ := Module.DirectLimit.exists_of y + exact ⟨Module.DirectLimit.of ℝ _ _ _ i x, Module.DirectLimit.lift_of _ _ _⟩⟩).symm + +private lemma equivℝ_ofLevel (i : CommIndex Γ₀) (f : ModularForm i.carrier k) : + equivℝ Γ₀ k (ofLevel Γ₀ k i f) = Module.DirectLimit.of ℝ _ _ _ i f := by + rw [equivℝ, LinearEquiv.symm_apply_eq, LinearEquiv.ofBijective_apply, fromLimℝ, + Module.DirectLimit.lift_of] + rfl + +/-- The action of `g ∈ commensurator Γ₀` on the `ℝ`-built limit: on the level-`i` piece it +translates by `g⁻¹` into the conjugate level `g i g⁻¹`. Assembled via the `ℝ`-linear universal +property of `limℝ`. -/ +private noncomputable def actℝ (g : ↥(Commensurable.commensurator Γ₀)) : + limℝ Γ₀ k →ₗ[ℝ] ModularFormCommensurable Γ₀ k := + Module.DirectLimit.lift ℝ (CommIndex Γ₀) _ (commTransitionℝ Γ₀ k) + (fun i ↦ (ofLevel Γ₀ k (CommIndex.conj g.1 g.2 i)).restrictScalars ℝ ∘ₗ translateℝ g.1⁻¹) (fun i j h x ↦ by - have hconj : CommIndex.conj g.1 (mem_commensurator_of_mem_PComm g) i - ≤ CommIndex.conj g.1 (mem_commensurator_of_mem_PComm g) j := by + have hconj : CommIndex.conj g.1 g.2 i ≤ CommIndex.conj g.1 g.2 j := by rw [CommIndex.le_def, CommIndex.conj_carrier, CommIndex.conj_carrier] exact Subgroup.pointwise_smul_le_pointwise_smul_iff.mpr (CommIndex.le_def.mp h) - have hcomm : translateₗ g.1⁻¹ (det_inv_pos (det_pos_of_mem_PComm g)) (restrictSubgroupₗ h x) - = restrictSubgroupₗ hconj - (translateₗ g.1⁻¹ (det_inv_pos (det_pos_of_mem_PComm g)) x) := by - ext z; rfl - simp only [LinearMap.comp_apply] - exact (congrArg (ofLevel Γ₀ k (CommIndex.conj g.1 (mem_commensurator_of_mem_PComm g) j)) - hcomm).trans - (ofLevel_restrict Γ₀ k hconj - (translateₗ g.1⁻¹ (det_inv_pos (det_pos_of_mem_PComm g)) x))) - -lemma smulMap_ofLevel (g : ↥(PComm Γ₀)) (i : CommIndex Γ₀) (f : ModularForm i.carrier k) : + have hcomm : translateℝ g.1⁻¹ (restrictSubgroupₗ h x) + = restrictSubgroupₗ hconj (translateℝ g.1⁻¹ x) := by ext z; rfl + show ofLevel Γ₀ k (CommIndex.conj g.1 g.2 j) (translateℝ g.1⁻¹ (restrictSubgroupₗ h x)) + = ofLevel Γ₀ k (CommIndex.conj g.1 g.2 i) (translateℝ g.1⁻¹ x) + rw [hcomm, ofLevel_restrict Γ₀ k hconj]) + +/-- The `ℝ`-linear action of `g ∈ commensurator Γ₀` on the direct limit: on the level-`i` piece it +translates by `g⁻¹` (an `ℝ`-linear map for any determinant) into the conjugate level `g i g⁻¹`. It is +assembled via the `ℝ`-linear universal property of `limℝ`, transported along `equivℝ`. -/ +noncomputable def smulMap (g : ↥(Commensurable.commensurator Γ₀)) : + ModularFormCommensurable Γ₀ k →ₗ[ℝ] ModularFormCommensurable Γ₀ k := + actℝ Γ₀ k g ∘ₗ (equivℝ Γ₀ k : ModularFormCommensurable Γ₀ k →ₗ[ℝ] limℝ Γ₀ k) + +lemma smulMap_ofLevel (g : ↥(Commensurable.commensurator Γ₀)) (i : CommIndex Γ₀) + (f : ModularForm i.carrier k) : smulMap Γ₀ k g (ofLevel Γ₀ k i f) - = ofLevel Γ₀ k (CommIndex.conj g.1 (mem_commensurator_of_mem_PComm g) i) - (translateₗ g.1⁻¹ (det_inv_pos (det_pos_of_mem_PComm g)) f) := - lift_ofLevel Γ₀ k _ _ i f + = ofLevel Γ₀ k (CommIndex.conj g.1 g.2 i) (translateℝ g.1⁻¹ f) := by + rw [smulMap, LinearMap.comp_apply, LinearEquiv.coe_coe, equivℝ_ofLevel, actℝ, + Module.DirectLimit.lift_of] + rfl /-- The `ℂ`-linear inclusion of a single level into functions `ℍ → ℂ`. -/ def coeₗ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] : @@ -216,58 +252,61 @@ lemma toFunₗ_injective : Function.Injective (toFunₗ Γ₀ k) := by intro i a b hab exact DFunLike.coe_injective hab -lemma toFunₗ_smulMap (g : ↥(PComm Γ₀)) (x : ModularFormCommensurable Γ₀ k) : +lemma toFunₗ_smulMap (g : ↥(Commensurable.commensurator Γ₀)) + (x : ModularFormCommensurable Γ₀ k) : toFunₗ Γ₀ k (smulMap Γ₀ k g x) = toFunₗ Γ₀ k x ∣[k] g.1⁻¹ := by induction x using ofLevel_induction with | ih i f => rw [smulMap_ofLevel, toFunₗ_ofLevel, toFunₗ_ofLevel]; rfl -lemma smulMap_one : smulMap Γ₀ k (1 : ↥(PComm Γ₀)) = LinearMap.id := by +lemma smulMap_one : smulMap Γ₀ k (1 : ↥(Commensurable.commensurator Γ₀)) = LinearMap.id := by ext x apply toFunₗ_injective simp only [toFunₗ_smulMap, LinearMap.id_coe, id_eq, OneMemClass.coe_one, inv_one, SlashAction.slash_one] -lemma smulMap_mul (g h : ↥(PComm Γ₀)) : +lemma smulMap_mul (g h : ↥(Commensurable.commensurator Γ₀)) : smulMap Γ₀ k (g * h) = smulMap Γ₀ k g ∘ₗ smulMap Γ₀ k h := by ext x apply toFunₗ_injective simp only [toFunₗ_smulMap, LinearMap.comp_apply, Subgroup.coe_mul, mul_inv_rev, SlashAction.slash_mul] -/-- The weight-`k` action of `PComm Γ₀` on `ModularFormCommensurable Γ₀ k` as a `ℂ`-linear -representation: `g` acts by the slash action of `g⁻¹` (well-defined and `ℂ`-linear because `g` has -positive determinant), permuting the levels by conjugation. -/ -noncomputable def commRep : Representation ℂ (↥(PComm Γ₀)) (ModularFormCommensurable Γ₀ k) where +/-- The weight-`k` action of `commensurator Γ₀` on `ModularFormCommensurable Γ₀ k` as an `ℝ`-linear +representation: `g` acts by the slash action of `g⁻¹` (well-defined and `ℝ`-linear for any +determinant — the `σ`-twist by complex conjugation fixes `ℝ`), permuting the levels by conjugation.-/ +noncomputable def commRep : + Representation ℝ (↥(Commensurable.commensurator Γ₀)) (ModularFormCommensurable Γ₀ k) where toFun := smulMap Γ₀ k map_one' := smulMap_one Γ₀ k map_mul' := smulMap_mul Γ₀ k -@[simp] lemma commRep_apply (g : ↥(PComm Γ₀)) : commRep Γ₀ k g = smulMap Γ₀ k g := rfl +@[simp] lemma commRep_apply (g : ↥(Commensurable.commensurator Γ₀)) : + commRep Γ₀ k g = smulMap Γ₀ k g := rfl omit [Γ₀.HasDetOne] in -/-- A level (a determinant-one subgroup commensurable with `Γ₀`) lies in the acting group -`PComm Γ₀` — it is in the commensurator and, being determinant-one, has positive determinant. -/ -lemma carrier_le_PComm (Γ : CommIndex Γ₀) : Γ.carrier ≤ PComm Γ₀ := by - refine le_inf (Subgroup.commensurable_le_commensurator Γ.commensurable) (fun γ hγ ↦ ?_) - rw [Matrix.mem_glpos, show (γ.det : ℝˣ) = 1 from Subgroup.HasDetOne.det_eq hγ, Units.val_one] - exact one_pos +/-- A level (a determinant-one subgroup commensurable with `Γ₀`) lies in the commensurator of `Γ₀`.-/ +lemma carrier_le_commensurator (Γ : CommIndex Γ₀) : + Γ.carrier ≤ Commensurable.commensurator Γ₀ := + Subgroup.commensurable_le_commensurator Γ.commensurable omit [Γ₀.HasDetOne] in -/-- The inclusion of a level into the acting group `PComm Γ₀`. -/ -noncomputable def levelIncl (Γ : CommIndex Γ₀) : Γ.carrier →* ↥(PComm Γ₀) := - Subgroup.inclusion (carrier_le_PComm Γ₀ Γ) +/-- The inclusion of a level into the commensurator `commensurator Γ₀`. -/ +noncomputable def levelIncl (Γ : CommIndex Γ₀) : + Γ.carrier →* ↥(Commensurable.commensurator Γ₀) := + Subgroup.inclusion (carrier_le_commensurator Γ₀ Γ) omit [Γ₀.HasDetOne] in @[simp] lemma coe_levelIncl (Γ : CommIndex Γ₀) (γ : Γ.carrier) : - ((levelIncl Γ₀ Γ γ : ↥(PComm Γ₀)) : GL (Fin 2) ℝ) = (γ : GL (Fin 2) ℝ) := rfl + ((levelIncl Γ₀ Γ γ : ↥(Commensurable.commensurator Γ₀)) : GL (Fin 2) ℝ) = + (γ : GL (Fin 2) ℝ) := rfl /-- **The level invariants of the commensurator action are the modular forms of that level.** For a level `Γ` in the commensurability class, the image of `ModularForm Γ.carrier k` under `ofLevel` -is exactly the submodule of `ModularFormCommensurable Γ₀ k` fixed by the action of all of `Γ.carrier` -(restricted from the `commRep` action of `PComm Γ₀`). -/ +(as an `ℝ`-submodule) is exactly the submodule of `ModularFormCommensurable Γ₀ k` fixed by the action +of all of `Γ.carrier` (restricted from the `commRep` action of `commensurator Γ₀`). -/ theorem range_ofLevel_eq_invariants (Γ : CommIndex Γ₀) : - LinearMap.range (ofLevel Γ₀ k Γ) + LinearMap.range ((ofLevel Γ₀ k Γ).restrictScalars ℝ) = Representation.invariants ((commRep Γ₀ k).comp (levelIncl Γ₀ Γ)) := by apply le_antisymm · rintro _ ⟨f, rfl⟩ @@ -290,8 +329,7 @@ theorem range_ofLevel_eq_invariants (Γ : CommIndex Γ₀) : have key : ∀ g : Γ.carrier, (⇑f : UpperHalfPlane → ℂ) ∣[k] (g : GL (Fin 2) ℝ)⁻¹ = ⇑f := by intro g have h2 := congrArg (toFunₗ Γ₀ k) (hx g) - rwa [MonoidHom.comp_apply, commRep_apply, toFunₗ_smulMap, toFunₗ_ofLevel, - coe_levelIncl] at h2 + rwa [MonoidHom.comp_apply, commRep_apply, toFunₗ_smulMap, toFunₗ_ofLevel, coe_levelIncl] at h2 let F : ModularForm Γ.carrier k := { toFun := ⇑f slash_action_eq' := fun δ hδ ↦ by @@ -300,16 +338,17 @@ theorem range_ofLevel_eq_invariants (Γ : CommIndex Γ₀) : bdd_at_cusps' := fun {c} hc ↦ f.bdd_at_cusps' ((Subgroup.Commensurable.isCusp_iff hcomm).mpr hc) } refine ⟨F, ?_⟩ + rw [LinearMap.restrictScalars_apply] have e1 : restrictSubgroupₗ hΓΛ' F = restrictSubgroupₗ hΛΛ' f := by ext z; rfl rw [← ofLevel_restrict Γ₀ k hΓΛ' F, e1] exact ofLevel_restrict Γ₀ k hΛΛ' f -/-- **Corollary.** `ModularForm Γ.carrier k` is `ℂ`-linearly isomorphic to the `Γ.carrier`-invariants +/-- **Corollary.** `ModularForm Γ.carrier k` is `ℝ`-linearly isomorphic to the `Γ.carrier`-invariants of the limit, via `ofLevel`. -/ noncomputable def ofLevelInvariantsEquiv (Γ : CommIndex Γ₀) : - ModularForm Γ.carrier k ≃ₗ[ℂ] + ModularForm Γ.carrier k ≃ₗ[ℝ] Representation.invariants ((commRep Γ₀ k).comp (levelIncl Γ₀ Γ)) := - (LinearEquiv.ofInjective (ofLevel Γ₀ k Γ) (ofLevel_injective Γ₀ k Γ)).trans + (LinearEquiv.ofInjective ((ofLevel Γ₀ k Γ).restrictScalars ℝ) (ofLevel_injective Γ₀ k Γ)).trans (LinearEquiv.ofEq _ _ (range_ofLevel_eq_invariants Γ₀ k Γ)) end ModularFormCommensurable From 957695600200473f9c14d48be2834fff9154f462 Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Tue, 30 Jun 2026 17:53:36 +0100 Subject: [PATCH 5/6] feat(CommensurableLimit): relax commensurator action to HasDetPlusMinusOne bases MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The whole ModularFormCommensurable section (commRep, ofLevelInvariantsEquiv, range_ofLevel_eq_invariants, ...) was still pinned to [Γ₀.HasDetOne] solely because Nonempty (CommIndex Γ₀) only had a HasDetOne instance (Γ₀ itself as the witness level). Add a Nonempty (CommIndex Γ₀) instance for HasDetPlusMinusOne bases, with witness the determinant-one part Γ₀ ⊓ ker(det): for det = ±1 groups the determinant maps Γ₀ onto a subgroup of {±1}, so the det-one part has index ≤ 2 (proved via Subgroup.index_ker + finiteness of the det image), hence is commensurable with Γ₀ and determinant-one. Then relax the CommensuratorAction section variable to [Γ₀.HasDetPlusMinusOne]; the action now works for genuinely det = ±1 bases, not just det = 1. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../CommensurabilityClass.lean | 22 ++++++++++++++++--- .../CommensuratorAction.lean | 8 +++---- 2 files changed, 23 insertions(+), 7 deletions(-) diff --git a/LeanBridge/CommensurableLimit/CommensurabilityClass.lean b/LeanBridge/CommensurableLimit/CommensurabilityClass.lean index 73fe4fae..f24a3231 100644 --- a/LeanBridge/CommensurableLimit/CommensurabilityClass.lean +++ b/LeanBridge/CommensurableLimit/CommensurabilityClass.lean @@ -85,9 +85,25 @@ instance : Preorder (CommIndex Γ₀) where @[simp] lemma le_def {i j : CommIndex Γ₀} : i ≤ j ↔ j.carrier ≤ i.carrier := Iff.rfl -/-- The base `Γ₀` (when determinant-one) is itself an index, so the class is nonempty. -/ -instance [Γ₀.HasDetOne] : Nonempty (CommIndex Γ₀) := - ⟨⟨Γ₀, .refl Γ₀, inferInstance⟩⟩ +/-- The determinant-one part `Γ₀ ⊓ ker det` is a determinant-one subgroup commensurable with `Γ₀` +(when `Γ₀` has determinant `±1` its determinant maps onto a subgroup of `{±1}`, so the det-one part +has index ≤ 2), hence a valid index — so the class is nonempty. This subsumes the determinant-one +case via `HasDetOne → HasDetPlusMinusOne`. -/ +instance [Γ₀.HasDetPlusMinusOne] : Nonempty (CommIndex Γ₀) := by + refine ⟨⟨Γ₀ ⊓ (Matrix.GeneralLinearGroup.det).ker, ⟨?_, ?_⟩, + ⟨fun {g} hg => MonoidHom.mem_ker.mp (Subgroup.mem_inf.mp hg).2⟩⟩⟩ + · have hsub : (Γ₀ ⊓ (Matrix.GeneralLinearGroup.det).ker).subgroupOf Γ₀ + = ((Matrix.GeneralLinearGroup.det).comp Γ₀.subtype).ker := by + rw [Subgroup.inf_subgroupOf_left, Subgroup.subgroupOf, MonoidHom.comap_ker] + show ((Γ₀ ⊓ (Matrix.GeneralLinearGroup.det).ker).subgroupOf Γ₀).index ≠ 0 + rw [hsub, Subgroup.index_ker] + have hfin : (((Matrix.GeneralLinearGroup.det).comp Γ₀.subtype).range : Set ℝˣ) ⊆ {1, -1} := by + rintro x ⟨g, rfl⟩ + simpa using HasDetPlusMinusOne.det_eq g.2 + have : Finite ((Matrix.GeneralLinearGroup.det).comp Γ₀.subtype).range := + (Set.Finite.subset ((Set.finite_singleton (-1 : ℝˣ)).insert 1) hfin).to_subtype + exact Nat.card_ne_zero.mpr ⟨⟨1, one_mem _⟩, this⟩ + · rw [Subgroup.relIndex_eq_one.mpr inf_le_left]; exact one_ne_zero /-- The commensurability class is directed under reverse inclusion: two indices have their meet as a common upper bound (it is commensurable with `Γ₀` and determinant-one). -/ diff --git a/LeanBridge/CommensurableLimit/CommensuratorAction.lean b/LeanBridge/CommensurableLimit/CommensuratorAction.lean index c5b83084..06575c99 100644 --- a/LeanBridge/CommensurableLimit/CommensuratorAction.lean +++ b/LeanBridge/CommensurableLimit/CommensuratorAction.lean @@ -147,7 +147,7 @@ instance (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetPlusMinusOne] (k : ℤ show (algebraMap ℝ ℂ r * c) • m = algebraMap ℝ ℂ r • (c • m) rw [mul_smul] -variable (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetOne] (k : ℤ) +variable (Γ₀ : Subgroup (GL (Fin 2) ℝ)) [Γ₀.HasDetPlusMinusOne] (k : ℤ) /-- The transition maps of the directed system, made `ℝ`-linear by restriction of scalars; the underlying functions are unchanged. -/ @@ -283,19 +283,19 @@ noncomputable def commRep : @[simp] lemma commRep_apply (g : ↥(Commensurable.commensurator Γ₀)) : commRep Γ₀ k g = smulMap Γ₀ k g := rfl -omit [Γ₀.HasDetOne] in +omit [Γ₀.HasDetPlusMinusOne] in /-- A level (a determinant-one subgroup commensurable with `Γ₀`) lies in the commensurator of `Γ₀`.-/ lemma carrier_le_commensurator (Γ : CommIndex Γ₀) : Γ.carrier ≤ Commensurable.commensurator Γ₀ := Subgroup.commensurable_le_commensurator Γ.commensurable -omit [Γ₀.HasDetOne] in +omit [Γ₀.HasDetPlusMinusOne] in /-- The inclusion of a level into the commensurator `commensurator Γ₀`. -/ noncomputable def levelIncl (Γ : CommIndex Γ₀) : Γ.carrier →* ↥(Commensurable.commensurator Γ₀) := Subgroup.inclusion (carrier_le_commensurator Γ₀ Γ) -omit [Γ₀.HasDetOne] in +omit [Γ₀.HasDetPlusMinusOne] in @[simp] lemma coe_levelIncl (Γ : CommIndex Γ₀) (γ : Γ.carrier) : ((levelIncl Γ₀ Γ γ : ↥(Commensurable.commensurator Γ₀)) : GL (Fin 2) ℝ) = (γ : GL (Fin 2) ℝ) := rfl From 69b7f47f7a705919ed1766b4664ac50aa4bdb5a0 Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Tue, 30 Jun 2026 21:01:56 +0100 Subject: [PATCH 6/6] =?UTF-8?q?refactor(HeckeRing):=20generalise=20?= =?UTF-8?q?=F0=9D=95=8B=20additive=20instances=20to=20AddCommMonoid/AddCom?= =?UTF-8?q?mGroup?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Hecke ring type 𝕋 P Z and its additive structure only need additive structure on the coefficients Z, not a full CommRing. Weaken the 𝕋 definition and FunLike instance to [Zero Z], add an AddCommMonoid (𝕋 P Z) instance for [AddCommMonoid Z], and state the AddCommGroup instance over [AddCommGroup Z]. Co-Authored-By: Claude Opus 4.8 (1M context) --- LeanBridge/ForMathlib/AbstractHeckeRing.lean | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/LeanBridge/ForMathlib/AbstractHeckeRing.lean b/LeanBridge/ForMathlib/AbstractHeckeRing.lean index 1b5829c0..73f87359 100644 --- a/LeanBridge/ForMathlib/AbstractHeckeRing.lean +++ b/LeanBridge/ForMathlib/AbstractHeckeRing.lean @@ -59,16 +59,25 @@ def HeckeCoset (P : HeckePair G) := Quotient (dcSetoid P) noncomputable instance instDecidableEqHeckeCoset (P : HeckePair G) : DecidableEq (HeckeCoset P) := Classical.decEq _ -/-- The Hecke ring type: formal `Z`-linear combinations of double cosets `HeckeCoset P`. -/ -def 𝕋 (P : HeckePair G) (Z : Type*) [CommRing Z] := Finsupp (HeckeCoset P) Z +/-- The Hecke ring type: formal `Z`-linear combinations of double cosets `HeckeCoset P`. The +coefficients `Z` need only carry a `Zero` for the type to make sense; algebraic structure on `Z` +is added by the instances below at the weakest level each requires. -/ +def 𝕋 (P : HeckePair G) (Z : Type*) [Zero Z] := Finsupp (HeckeCoset P) Z /-- `FunLike` instance for `𝕋 P Z`: treat elements as functions `HeckeCoset P → Z`. -/ -instance instFunLike𝕋 (P : HeckePair G) (Z : Type*) [CommRing Z] : +instance instFunLike𝕋 (P : HeckePair G) (Z : Type*) [Zero Z] : FunLike (𝕋 P Z) (HeckeCoset P) Z := inferInstanceAs (FunLike (HeckeCoset P →₀ Z) (HeckeCoset P) Z) -/-- The additive commutative group structure on the Hecke ring. -/ -noncomputable instance instAddCommGroup𝕋 (P : HeckePair G) (Z : Type*) [CommRing Z] : +/-- The additive commutative monoid structure on the Hecke ring, for any `AddCommMonoid` of +coefficients. -/ +noncomputable instance instAddCommMonoid𝕋 (P : HeckePair G) (Z : Type*) [AddCommMonoid Z] : + AddCommMonoid (𝕋 P Z) := + inferInstanceAs (AddCommMonoid ((HeckeCoset P) →₀ Z)) + +/-- The additive commutative group structure on the Hecke ring, when the coefficients form an +`AddCommGroup`. -/ +noncomputable instance instAddCommGroup𝕋 (P : HeckePair G) (Z : Type*) [AddCommGroup Z] : AddCommGroup (𝕋 P Z) := inferInstanceAs (AddCommGroup ((HeckeCoset P) →₀ Z))