From bc285719fe4e34649f0f74e2f7424f9517788a4d Mon Sep 17 00:00:00 2001 From: Chris Birkbeck Date: Wed, 1 Jul 2026 09:32:41 +0100 Subject: [PATCH] feat(HeckeRing): the abstract Hecke ring is a Ring MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove Ring (𝕋 P ℤ) for the abstract Hecke ring of a Hecke pair (Shimura, Ch. 3): the double-coset quotient basis (Basic), the convolution product via Shimura's integer multiplicities (Multiplication), the module action used in the associativity argument (Module), associativity (Associativity), and the Ring instance (Ring). Only the ring structure -- commutativity, the degree map, and further API are left to follow-up PRs. Part of #75. Co-Authored-By: Claude Opus 4.8 (1M context) --- LeanBridge.lean | 1 + LeanBridge/ForMathlib/AbstractHeckeRing.lean | 26 + .../AbstractHeckeRing/Associativity.lean | 749 ++++++++++++++++++ .../ForMathlib/AbstractHeckeRing/Basic.lean | 345 ++++++++ .../ForMathlib/AbstractHeckeRing/Module.lean | 268 +++++++ .../AbstractHeckeRing/Multiplication.lean | 688 ++++++++++++++++ .../ForMathlib/AbstractHeckeRing/Ring.lean | 189 +++++ 7 files changed, 2266 insertions(+) create mode 100644 LeanBridge/ForMathlib/AbstractHeckeRing.lean create mode 100644 LeanBridge/ForMathlib/AbstractHeckeRing/Associativity.lean create mode 100644 LeanBridge/ForMathlib/AbstractHeckeRing/Basic.lean create mode 100644 LeanBridge/ForMathlib/AbstractHeckeRing/Module.lean create mode 100644 LeanBridge/ForMathlib/AbstractHeckeRing/Multiplication.lean create mode 100644 LeanBridge/ForMathlib/AbstractHeckeRing/Ring.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..848e46bb --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing.lean @@ -0,0 +1,26 @@ +/- +Copyright (c) 2024 Chris Birkbeck. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Birkbeck +-/ +import LeanBridge.ForMathlib.AbstractHeckeRing.Ring + +/-! +# Abstract Hecke ring: the ring structure + +The abstract Hecke ring of a Hecke pair `(H, Δ)`, following Shimura, *Introduction to the Arithmetic +Theory of Automorphic Functions*, Ch. 3, together with the proof that it is a `Ring`. For an +arithmetic pair `H ≤ Δ ≤ commensurator(H)` this assembles: + +* `HeckeRing.HeckePair`, the double-coset quotient `HeckeRing.HeckeCoset`, and the Hecke ring type + `HeckeRing.𝕋` (`Basic`); +* the convolution product via Shimura's multiplicities (`Multiplication`), the module action used in + the associativity argument (`Module`), associativity of the product (`Associativity`), and the + resulting `Ring (𝕋 P ℤ)` instance (`Ring`). + +Commutativity (from an anti-involution), the degree map, and the remaining API are deliberately left +to follow-up PRs. + +Ported from the AINTLIB project +(`projects/LeanModularForms/LeanModularForms/HeckeRIngs/AbstractHeckeRing`). +-/ diff --git a/LeanBridge/ForMathlib/AbstractHeckeRing/Associativity.lean b/LeanBridge/ForMathlib/AbstractHeckeRing/Associativity.lean new file mode 100644 index 00000000..6289bfac --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing/Associativity.lean @@ -0,0 +1,749 @@ +/- +Copyright (c) 2024 Chris Birkbeck. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Birkbeck +-/ +import LeanBridge.ForMathlib.AbstractHeckeRing.Module + +/-! +# Hecke Rings: Associativity + +The `IsScalarTower` instance proving that the module action is compatible with multiplication, +which is equivalent to associativity of multiplication in the Hecke ring. This is Shimura +Proposition 3.4. + +## Main results + +* `HeckeRing.heckeMultiplicity_uniform`: the number of coset pairs `(i, j)` mapping to a given + left coset within a double coset is independent of the chosen representative. +* `HeckeRing.instIsScalarTower`: the scalar tower property `(x * y) • z = y • (x • z)`, + which is equivalent to associativity of multiplication in the Hecke ring. +-/ + +open Classical + +open scoped Pointwise + +namespace HeckeRing + +variable {G : Type*} [Group G] + +variable (P : HeckePair G) (Z : Type*) [CommRing Z] + +private lemma smulOrbit_map_injective (g β : P.Δ) : + Function.Injective (fun i : decompQuot P g ↦ + (⟦⟨(β : G) * (i.out : G) * (g : G), + delta_mul_mem P.H P.Δ i.out β g P.h₀⟩⟧ : HeckeLeftCoset P)) := by + intro i₁ i₂ heq + by_contra hne + have hmem : (β : G) * (i₁.out : G) * (g : G) ∈ + ({(β : G) * (i₂.out : G) * (g : G)} : Set G) * + (P.H : Set G) := by + rw [← (Quotient.exact heq : ({(β : G) * (i₁.out : G) * (g : G)} : Set G) * (P.H : Set G) = + {(β : G) * (i₂.out : G) * (g : G)} * P.H)] + exact ⟨_, rfl, 1, P.H.one_mem, mul_one _⟩ + obtain ⟨_, ha, k, hk, hkk⟩ := hmem + rw [Set.mem_singleton_iff] at ha + subst ha + have cancel : (i₂.out : G) * (g : G) * k = (i₁.out : G) * (g : G) := by + apply mul_left_cancel (a := (β : G)) + group at hkk ⊢ + exact hkk + apply decompQuot_coset_diff P g i₁ i₂ hne + refine leftCoset_eq_of_not_disjoint (H := P.H) _ _ ?_ + rw [Set.not_disjoint_iff] + exact ⟨(i₁.out : G) * (g : G), ⟨1, P.H.one_mem, mul_one _⟩, ⟨k, hk, cancel⟩⟩ + +private lemma conjAct_inv_mem_of_subgroupOf (g : G) + (n : (ConjAct.toConjAct g • P.H).subgroupOf P.H) : g⁻¹ * (n : G)⁻¹ * g ∈ P.H := by + have hn := n.2 + rw [Subgroup.mem_subgroupOf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, + ConjAct.smul_def] at hn + simp only [map_inv, ConjAct.ofConjAct_toConjAct, inv_inv] at hn + convert P.H.inv_mem hn using 1 + group + +private lemma conjAct_mem_of_subgroupOf (g : G) + (n : (ConjAct.toConjAct g • P.H).subgroupOf P.H) : g⁻¹ * (n : G) * g ∈ P.H := by + have hn := n.2 + rw [Subgroup.mem_subgroupOf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, + ConjAct.smul_def] at hn + simpa using hn + +private lemma mk_out_coe_eq_mul {g : G} {h : P.H} + {n : (ConjAct.toConjAct g • P.H).subgroupOf P.H} + (hn_eq : (⟦h⟧ : P.H ⧸ (ConjAct.toConjAct g • P.H).subgroupOf P.H).out = h * n) : + ((⟦h⟧ : P.H ⧸ (ConjAct.toConjAct g • P.H).subgroupOf P.H).out : G) = + (h : G) * (n : G) := by + simpa using congr_arg (Subtype.val : ↥P.H → G) hn_eq + +private lemma decompQuot_eq_of_conjAct_rel (g : P.Δ) (i₁ i₂ : decompQuot P g) + (h : (i₁.out : ↥P.H)⁻¹ * i₂.out ∈ + (ConjAct.toConjAct (g : G) • P.H).subgroupOf P.H) : + i₁ = i₂ := by + rw [← QuotientGroup.leftRel_apply, ← Quotient.eq''] at h + simpa using h + +/-- Inverse-translation recovery in `decompQuot`: if `b = ⟦s · a.out⟧` with +`s ∈ P.H`, then `⟦s⁻¹ · b.out⟧ = a`. Used twice in the surjectivity +of the forward map (once on each component). -/ +private lemma decompQuot_inv_mul_out_eq {g : P.Δ} (a b : decompQuot P g) + (s : G) (hs : s ∈ P.H) + (hb : b = (⟦⟨s * (a.out : G), P.H.mul_mem hs a.out.2⟩⟧ : decompQuot P g)) : + (⟦⟨s⁻¹ * (b.out : G), + P.H.mul_mem (P.H.inv_mem hs) b.out.2⟩⟧ : decompQuot P g) = a := by + rw [← Quotient.out_eq' a, Quotient.eq'', QuotientGroup.leftRel_apply] + have h := Quotient.out_eq' b + nth_rewrite 2 [hb] at h + rw [Quotient.eq'', QuotientGroup.leftRel_apply] at h + convert h using 1 + ext + simp only [Subgroup.coe_mul, InvMemClass.coe_inv, mul_inv_rev, inv_inv] + group + +private lemma coset_shift_fwd (q a b a' b' g₁ g₂ g_D n₁ n₂ : G) + (hcond : ({a * g₂ * (b * g₁)} : Set G) * ↑P.H = {q * g_D} * ↑P.H) + (ha' : a' = q⁻¹ * a * n₁) (hb' : b' = g₂⁻¹ * n₁⁻¹ * g₂ * b * n₂) + (hn₂_conj : g₁⁻¹ * n₂ * g₁ ∈ P.H) : + ({a' * g₂ * (b' * g₁)} : Set G) * ↑P.H = {g_D} * ↑P.H := by + subst ha' hb' + apply leftCoset_eq_of_not_disjoint + rw [Set.not_disjoint_iff] + refine ⟨q⁻¹ * a * n₁ * g₂ * (g₂⁻¹ * n₁⁻¹ * g₂ * b * n₂ * g₁), + ⟨1, P.H.one_mem, by simp⟩, ?_⟩ + have hmem : a * g₂ * (b * g₁) ∈ ({q * g_D} : Set G) * ↑P.H := by + rw [← hcond] + exact ⟨_, rfl, 1, P.H.one_mem, by group⟩ + obtain ⟨_, h_eq, h₀, hh₀, hprod⟩ := hmem + simp only [Set.mem_singleton_iff] at h_eq + subst h_eq + refine ⟨h₀ * (g₁⁻¹ * n₂ * g₁), P.H.mul_mem hh₀ hn₂_conj, ?_⟩ + simp only [smul_eq_mul] + symm + calc q⁻¹ * a * n₁ * g₂ * (g₂⁻¹ * n₁⁻¹ * g₂ * b * n₂ * g₁) + = q⁻¹ * (a * g₂ * (b * g₁)) * (g₁⁻¹ * n₂ * g₁) := by group + _ = g_D * (h₀ * (g₁⁻¹ * n₂ * g₁)) := by rw [← hprod]; group + +private lemma coset_shift_inv (q a b a' b' g₁ g₂ g_D m₁ m₂ : G) + (hcond : ({a' * g₂ * (b' * g₁)} : Set G) * ↑P.H = {g_D} * ↑P.H) + (ha : a = q * a' * m₁) (hb : b = g₂⁻¹ * m₁⁻¹ * g₂ * b' * m₂) + (hm₂_conj : g₁⁻¹ * m₂ * g₁ ∈ P.H) : + ({a * g₂ * (b * g₁)} : Set G) * ↑P.H = {q * g_D} * ↑P.H := by + apply leftCoset_eq_of_not_disjoint + rw [Set.not_disjoint_iff] + refine ⟨a * g₂ * (b * g₁), ⟨1, P.H.one_mem, by simp⟩, ?_⟩ + have hmem : a' * g₂ * (b' * g₁) ∈ ({g_D} : Set G) * ↑P.H := by + rw [← hcond] + exact ⟨_, rfl, 1, P.H.one_mem, by group⟩ + obtain ⟨_, hd_eq, h₀, hh₀, hprod⟩ := hmem + simp only [Set.mem_singleton_iff] at hd_eq + refine ⟨h₀ * (g₁⁻¹ * m₂ * g₁), P.H.mul_mem hh₀ hm₂_conj, ?_⟩ + simp only [smul_eq_mul] + symm + calc a * g₂ * (b * g₁) + = q * (a' * g₂ * (b' * g₁)) * (g₁⁻¹ * m₂ * g₁) := by subst ha hb; group + _ = q * g_D * (h₀ * (g₁⁻¹ * m₂ * g₁)) := by subst hd_eq; rw [← hprod]; group + +private lemma representative_cancel_eq_inv (a m n : G) (h : a = a * m * n) : n = m⁻¹ := + eq_inv_of_mul_eq_one_right + (mul_left_cancel (a := a) (by rw [mul_one, ← mul_assoc]; exact h.symm)) + +private noncomputable def uniformShiftElt (g₂ : P.Δ) (D : HeckeCoset P) + (q₀ : decompQuot P (HeckeCoset.rep D)) (i : decompQuot P g₂) : + (ConjAct.toConjAct (g₂ : G) • P.H).subgroupOf P.H := + (QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (g₂ : G) • P.H).subgroupOf P.H) + ⟨(q₀.out : G)⁻¹ * i.out, P.H.mul_mem (P.H.inv_mem q₀.out.2) i.out.2⟩).choose + +private noncomputable def heckeMultiplicity_uniform_fwdMap (g₂ g₁ : P.Δ) + (D : HeckeCoset P) (q₀ : decompQuot P (HeckeCoset.rep D)) + (p : {p : decompQuot P g₂ × decompQuot P g₁ | + ({(p.1.out : G) * (g₂ : G)} : Set G) * {(p.2.out : G) * (g₁ : G)} * P.H = + {(q₀.out : G) * (HeckeCoset.rep D : G)} * (P.H : Set G)}) : + {p : decompQuot P g₂ × decompQuot P g₁ | + ({(p.1.out : G) * (g₂ : G)} : Set G) * {(p.2.out : G) * (g₁ : G)} * P.H = + {(HeckeCoset.rep D : G)} * (P.H : Set G)} := + let i := p.1.1 + let j := p.1.2 + let i' : decompQuot P g₂ := + ⟦⟨(q₀.out : G)⁻¹ * i.out, P.H.mul_mem (P.H.inv_mem q₀.out.2) i.out.2⟩⟧ + let n := uniformShiftElt P g₂ D q₀ i + let hn_conj : (g₂ : G)⁻¹ * (n : G)⁻¹ * (g₂ : G) ∈ P.H := + conjAct_inv_mem_of_subgroupOf P (g₂ : G) n + let j' : decompQuot P g₁ := + ⟦⟨(g₂ : G)⁻¹ * (n : G)⁻¹ * (g₂ : G) * j.out, P.H.mul_mem hn_conj j.out.2⟩⟧ + ⟨⟨i', j'⟩, by + change ({(i'.out : G) * (g₂ : G)} : Set G) * {(j'.out : G) * (g₁ : G)} * P.H = + {(HeckeCoset.rep D : G)} * P.H + rw [Set.singleton_mul_singleton] + have hcond' : ({(i.out : G) * (g₂ : G) * ((j.out : G) * (g₁ : G))} : Set G) * ↑P.H = + {(q₀.out : G) * (HeckeCoset.rep D : G)} * ↑P.H := by + rw [← Set.singleton_mul_singleton]; exact p.2 + obtain ⟨n', hn'_eq⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (g₁ : G) • P.H).subgroupOf P.H) + ⟨(g₂ : G)⁻¹ * (n : G)⁻¹ * (g₂ : G) * j.out, P.H.mul_mem hn_conj j.out.2⟩ + exact coset_shift_fwd P (q₀.out : G) (i.out : G) (j.out : G) (i'.out : G) + (j'.out : G) (g₁ : G) (g₂ : G) (HeckeCoset.rep D : G) (n : G) (n' : G) hcond' + (mk_out_coe_eq_mul P (QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (g₂ : G) • P.H).subgroupOf P.H) + ⟨(q₀.out : G)⁻¹ * i.out, + P.H.mul_mem (P.H.inv_mem q₀.out.2) i.out.2⟩).choose_spec) + (mk_out_coe_eq_mul P hn'_eq) (conjAct_mem_of_subgroupOf P (g₁ : G) n')⟩ + +private lemma uniformShiftElt_eq_m_inv (g₂ : P.Δ) (D : HeckeCoset P) + (q₀ : decompQuot P (HeckeCoset.rep D)) (i' i₀ : decompQuot P g₂) + (m_i : (ConjAct.toConjAct (g₂ : G) • P.H).subgroupOf P.H) + (h_quot_eq : (⟦⟨(q₀.out : G)⁻¹ * (i₀.out : G), + P.H.mul_mem (P.H.inv_mem q₀.out.2) i₀.out.2⟩⟧ : decompQuot P g₂) = i') + (hmi_coe : (i₀.out : G) = (q₀.out : G) * (i'.out : G) * (m_i : G)) : + (uniformShiftElt P g₂ D q₀ i₀ : G) = (m_i : G)⁻¹ := by + have hn₀_val : (i'.out : G) = + (q₀.out : G)⁻¹ * (i₀.out : G) * (uniformShiftElt P g₂ D q₀ i₀ : G) := by + have h1 := congr_arg (Subtype.val : ↥P.H → G) (QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (g₂ : G) • P.H).subgroupOf P.H) + ⟨(q₀.out : G)⁻¹ * i₀.out, + P.H.mul_mem (P.H.inv_mem q₀.out.2) i₀.out.2⟩).choose_spec + simp only [Subgroup.coe_mul] at h1 + rwa [show ((⟦⟨(q₀.out : G)⁻¹ * (i₀.out : G), + P.H.mul_mem (P.H.inv_mem q₀.out.2) i₀.out.2⟩⟧ : decompQuot P g₂).out : G) = + (i'.out : G) by congr 1; simp [h_quot_eq]] at h1 + apply representative_cancel_eq_inv (a := (i'.out : G)) (m := (m_i : G)) + conv_lhs => rw [hn₀_val, hmi_coe] + group + +private lemma heckeMultiplicity_uniform_fwdMap_injective (g₂ g₁ : P.Δ) (D : HeckeCoset P) + (q₀ : decompQuot P (HeckeCoset.rep D)) : + Function.Injective (heckeMultiplicity_uniform_fwdMap P g₂ g₁ D q₀) := by + intro ⟨⟨i₁, j₁⟩, h₁⟩ ⟨⟨i₂, j₂⟩, h₂⟩ heq + simp only [heckeMultiplicity_uniform_fwdMap, Subtype.mk.injEq, Prod.mk.injEq] at heq + obtain ⟨hi, hj⟩ := heq + have hi₁₂ : i₁ = i₂ := by + rw [Quotient.eq'', QuotientGroup.leftRel_apply] at hi + refine decompQuot_eq_of_conjAct_rel P g₂ i₁ i₂ ?_ + convert hi using 1 + ext + simp only [Subgroup.coe_mul, InvMemClass.coe_inv, mul_inv_rev, inv_inv] + group + subst hi₁₂ + have hj₁₂ : j₁ = j₂ := by + rw [Quotient.eq'', QuotientGroup.leftRel_apply] at hj + refine decompQuot_eq_of_conjAct_rel P g₁ j₁ j₂ ?_ + convert hj using 1 + ext + simp only [Subgroup.coe_mul, InvMemClass.coe_inv, mul_inv_rev, inv_inv] + group + subst hj₁₂ + rfl + +/-- The j-side recovery in the surjectivity proof: given +`j₀ = ⟦(g₂⁻¹·n₀·g₂) · j'.out⟧` +(where `n₀ := uniformShiftElt P g₂ D q₀ i₀`), +the quotient class `⟦(g₂⁻¹·n₀⁻¹·g₂) · j₀.out⟧` equals `j'`. -/ +private lemma decompQuot_j_recover_via_uniformShift (g₂ g₁ : P.Δ) (D : HeckeCoset P) + (q₀ : decompQuot P (HeckeCoset.rep D)) (i₀ : decompQuot P g₂) + (j' : decompQuot P g₁) : + let n₀ := uniformShiftElt P g₂ D q₀ i₀ + let hn₀_conj : (g₂ : G)⁻¹ * (n₀ : G) * (g₂ : G) ∈ P.H := + conjAct_mem_of_subgroupOf P (g₂ : G) n₀ + let j₀ : decompQuot P g₁ := ⟦⟨(g₂ : G)⁻¹ * (n₀ : G) * (g₂ : G) * j'.out, + P.H.mul_mem hn₀_conj j'.out.2⟩⟧ + (⟦⟨(g₂ : G)⁻¹ * (n₀ : G)⁻¹ * (g₂ : G) * (j₀.out : G), + P.H.mul_mem (conjAct_inv_mem_of_subgroupOf P (g₂ : G) n₀) j₀.out.2⟩⟧ : + decompQuot P g₁) = j' := by + intro n₀ hn₀_conj j₀ + rw [← Quotient.out_eq' j', Quotient.eq'', QuotientGroup.leftRel_apply] + have h_j₀ := Quotient.out_eq' j₀ + rw [Quotient.eq'', QuotientGroup.leftRel_apply] at h_j₀ + convert h_j₀ using 1 + ext + simp only [Subgroup.coe_mul, InvMemClass.coe_inv, mul_inv_rev, inv_inv] + group + +private lemma heckeMultiplicity_uniform_fwdMap_surjective (g₂ g₁ : P.Δ) (D : HeckeCoset P) + (q₀ : decompQuot P (HeckeCoset.rep D)) : + Function.Surjective (heckeMultiplicity_uniform_fwdMap P g₂ g₁ D q₀) := by + intro ⟨⟨i', j'⟩, (hcond'_tgt : _ = _)⟩ + let i₀ : decompQuot P g₂ := + ⟦⟨(q₀.out : G) * i'.out, P.H.mul_mem q₀.out.2 i'.out.2⟩⟧ + let n₀ := uniformShiftElt P g₂ D q₀ i₀ + have hn₀_conj : (g₂ : G)⁻¹ * (n₀ : G) * (g₂ : G) ∈ P.H := + conjAct_mem_of_subgroupOf P (g₂ : G) n₀ + let j₀ : decompQuot P g₁ := ⟦⟨(g₂ : G)⁻¹ * (n₀ : G) * (g₂ : G) * j'.out, + P.H.mul_mem hn₀_conj j'.out.2⟩⟧ + obtain ⟨m_i, hmi_eq⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (g₂ : G) • P.H).subgroupOf P.H) + ⟨(q₀.out : G) * i'.out, P.H.mul_mem q₀.out.2 i'.out.2⟩ + obtain ⟨m_j, hmj_eq⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (g₁ : G) • P.H).subgroupOf P.H) + ⟨(g₂ : G)⁻¹ * (n₀ : G) * (g₂ : G) * j'.out, P.H.mul_mem hn₀_conj j'.out.2⟩ + have hmi_coe : (i₀.out : G) = (q₀.out : G) * (i'.out : G) * (m_i : G) := + mk_out_coe_eq_mul P hmi_eq + have hmj_coe : (j₀.out : G) = + (g₂ : G)⁻¹ * (n₀ : G) * (g₂ : G) * (j'.out : G) * (m_j : G) := + mk_out_coe_eq_mul P hmj_eq + have h_quot_eq : (⟦⟨(q₀.out : G)⁻¹ * (i₀.out : G), + P.H.mul_mem (P.H.inv_mem q₀.out.2) i₀.out.2⟩⟧ : decompQuot P g₂) = i' := + decompQuot_inv_mul_out_eq P i' i₀ (q₀.out : G) q₀.out.2 rfl + have hcond₀ : ({(i₀.out : G) * (g₂ : G)} : Set G) * {(j₀.out : G) * (g₁ : G)} * P.H = + {(q₀.out : G) * (HeckeCoset.rep D : G)} * P.H := by + rw [Set.singleton_mul_singleton] + exact coset_shift_inv P (q₀.out : G) (i₀.out : G) (j₀.out : G) (i'.out : G) + (j'.out : G) (g₁ : G) (g₂ : G) (HeckeCoset.rep D : G) (m_i : G) (m_j : G) + (by rw [← Set.singleton_mul_singleton]; exact hcond'_tgt) + hmi_coe (by rw [hmj_coe, + uniformShiftElt_eq_m_inv P g₂ D q₀ i' i₀ m_i h_quot_eq hmi_coe]) + (conjAct_mem_of_subgroupOf P (g₁ : G) m_j) + refine ⟨⟨⟨i₀, j₀⟩, hcond₀⟩, Subtype.ext ?_⟩ + simp only [heckeMultiplicity_uniform_fwdMap, Prod.mk.injEq] + exact ⟨h_quot_eq, decompQuot_j_recover_via_uniformShift P g₂ g₁ D q₀ i₀ j'⟩ + +/-- Uniform distribution of multiplicities: the count of coset pairs `(i,j)` mapping +to a given left coset `q₀H` within double coset `D` is independent of the choice of `q₀` +(Shimura Proposition 3.4). -/ +lemma heckeMultiplicity_uniform (g₂ g₁ : P.Δ) (D : HeckeCoset P) + (q₀ : decompQuot P (HeckeCoset.rep D)) : + Nat.card {p : decompQuot P g₂ × decompQuot P g₁ | + ({(p.1.out : G) * (g₂ : G)} : Set G) * {(p.2.out : G) * (g₁ : G)} * P.H = + {(q₀.out : G) * (HeckeCoset.rep D : G)} * (P.H : Set G)} = + Nat.card {p : decompQuot P g₂ × decompQuot P g₁ | + ({(p.1.out : G) * (g₂ : G)} : Set G) * {(p.2.out : G) * (g₁ : G)} * P.H = + {(HeckeCoset.rep D : G)} * (P.H : Set G)} := + Nat.card_congr <| Equiv.ofBijective _ + ⟨heckeMultiplicity_uniform_fwdMap_injective P g₂ g₁ D q₀, + heckeMultiplicity_uniform_fwdMap_surjective P g₂ g₁ D q₀⟩ + +/-- Given a double-coset decomposition `i.out·g₂·(j.out·g₁) = h₁·g_D·h₂` and the +cosrep formula `r.out = h₁·n` with `n` in the relevant conjugate subgroup, the two +HeckeLeftCoset classes `⟦β·r.out·g_D⟧` and `⟦β·i.out·g₂·j.out·g₁⟧` agree. -/ +private lemma iter_doubleCoset_class_eq (β g_D g₁' g₂' i_out j_out h₁ h₂ : G) + (hh₂ : h₂ ∈ P.H) (hprod : i_out * g₂' * (j_out * g₁') = h₁ * g_D * h₂) (r_out : G) + (n : (ConjAct.toConjAct g_D • P.H).subgroupOf P.H) + (hn_coe : r_out = h₁ * (n : G)) + (h_mem_l : β * r_out * g_D ∈ P.Δ) + (h_mem_r : β * i_out * g₂' * j_out * g₁' ∈ P.Δ) : + (⟦⟨β * r_out * g_D, h_mem_l⟩⟧ : HeckeLeftCoset P) = + (⟦⟨β * i_out * g₂' * j_out * g₁', h_mem_r⟩⟧ : HeckeLeftCoset P) := by + apply Quotient.sound + change lcRel P _ _ + simp only [lcRel] + apply leftCoset_eq_of_not_disjoint + rw [Set.not_disjoint_iff] + refine ⟨β * h₁ * g_D, ?_, ?_⟩ + · refine ⟨g_D⁻¹ * (n : G)⁻¹ * g_D, conjAct_inv_mem_of_subgroupOf P g_D n, ?_⟩ + simp only [smul_eq_mul, hn_coe] + group + · refine ⟨h₂⁻¹, P.H.inv_mem hh₂, ?_⟩ + simp only [smul_eq_mul] + calc β * i_out * g₂' * j_out * g₁' * h₂⁻¹ + = β * (i_out * g₂' * (j_out * g₁')) * h₂⁻¹ := by group + _ = β * (h₁ * g_D * h₂) * h₂⁻¹ := by rw [hprod] + _ = β * h₁ * g_D := by group + +private lemma iter_mem_smulOrbit_mulMap (g₂ g₁ β : P.Δ) (i : decompQuot P g₂) + (j : decompQuot P g₁) : + (⟦⟨(β : G) * i.out * (g₂ : G) * j.out * (g₁ : G), + Submonoid.mul_mem _ (Submonoid.mul_mem _ (delta_mul_mem P.H P.Δ i.out β g₂ P.h₀) + (P.h₀ j.out.2)) g₁.2⟩⟧ : HeckeLeftCoset P) ∈ + smulOrbit P (HeckeCoset.rep (mulMap P g₂ g₁ (i, j))) β := by + set D := mulMap P g₂ g₁ (i, j) with hD_def + have h_in_doset : (i.out : G) * (g₂ : G) * ((j.out : G) * (g₁ : G)) ∈ + DoubleCoset.doubleCoset (HeckeCoset.rep D : G) P.H P.H := by + rw [← HeckeCoset.toSet_eq_rep D, hD_def] + simpa only [mulMap, HeckeCoset.toSet_mk] using + DoubleCoset.mem_doubleCoset_self P.H P.H _ + rw [DoubleCoset.mem_doubleCoset] at h_in_doset + obtain ⟨h₁, hh₁, h₂, hh₂, hprod⟩ := h_in_doset + set r : decompQuot P (HeckeCoset.rep D) := ⟦⟨h₁, hh₁⟩⟧ + obtain ⟨n, hn_eq⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (HeckeCoset.rep D : G) • P.H).subgroupOf P.H) ⟨h₁, hh₁⟩ + have hsuff := iter_doubleCoset_class_eq P (β : G) (HeckeCoset.rep D : G) (g₁ : G) (g₂ : G) + (i.out : G) (j.out : G) h₁ h₂ hh₂ hprod (r.out : G) n + (mk_out_coe_eq_mul P hn_eq) + (delta_mul_mem P.H P.Δ r.out β (HeckeCoset.rep D) P.h₀) + (Submonoid.mul_mem _ (Submonoid.mul_mem _ + (delta_mul_mem P.H P.Δ i.out β g₂ P.h₀) (P.h₀ j.out.2)) g₁.2) + rw [← hsuff] + show _ ∈ smulOrbit _ _ _ + simp only [smulOrbit, Finset.mem_image] + exact ⟨r, Finset.mem_univ _, rfl⟩ + +private lemma rep_mem_H_of_smulOrbit_eq (g₂ β₀ : P.Δ) (i₀ : decompQuot P g₂) + (j : HeckeLeftCoset P) + (hj_eq : (⟦⟨(β₀ : G) * i₀.out * (g₂ : G), + delta_mul_mem P.H P.Δ i₀.out β₀ g₂ P.h₀⟩⟧ : HeckeLeftCoset P) = j) : + (g₂ : G)⁻¹ * (i₀.out : G)⁻¹ * (β₀ : G)⁻¹ * + (HeckeLeftCoset.rep j : G) ∈ P.H := by + set β := (HeckeLeftCoset.rep j : G) + have h_coset : ({β} : Set G) * ↑P.H = + ({(β₀ : G) * (i₀.out : G) * (g₂ : G)} : Set G) * ↑P.H := by + have h1 : HeckeLeftCoset.toSet j = ({β} : Set G) * ↑P.H := by + rw [← Quotient.out_eq (s := lcSetoid P) j]; rfl + rw [← h1, ← hj_eq]; rfl + have hβ : β ∈ ({(β₀ : G) * (i₀.out : G) * (g₂ : G)} : Set G) * ↑P.H := + h_coset ▸ (⟨_, rfl, 1, P.H.one_mem, mul_one _⟩ : β ∈ ({β} : Set G) * ↑P.H) + simp only [Set.singleton_mul, Set.mem_image] at hβ + obtain ⟨h, hh, hβ_eq⟩ := hβ + have hβ' : (g₂ : G)⁻¹ * (i₀.out : G)⁻¹ * (β₀ : G)⁻¹ * β = h := by + rw [← hβ_eq]; group + exact hβ' ▸ hh + +/-- The HeckeLeftCoset class `⟦β·k₀·g₁'⟧` equals +`⟦α·i₀·g₂'·k'·g₁'⟧` provided +`k' = ⟦g₂'⁻¹·i₀⁻¹·α⁻¹·β·k₀⟧` (i.e. +`k'.out = (g₂'⁻¹·i₀⁻¹·α⁻¹·β·k₀)·n'` for some +`n'` in the conjugate subgroup). -/ +private lemma iter_connector_class_eq (α β g₁' g₂' i₀ k₀ k'_out : G) + (n' : (ConjAct.toConjAct g₁' • P.H).subgroupOf P.H) + (hk'_coe : k'_out = g₂'⁻¹ * i₀⁻¹ * α⁻¹ * β * k₀ * (n' : G)) + (h_mem_l : β * k₀ * g₁' ∈ P.Δ) (h_mem_r : α * i₀ * g₂' * k'_out * g₁' ∈ P.Δ) : + (⟦⟨β * k₀ * g₁', h_mem_l⟩⟧ : HeckeLeftCoset P) = + (⟦⟨α * i₀ * g₂' * k'_out * g₁', h_mem_r⟩⟧ : HeckeLeftCoset P) := by + apply Quotient.sound + change lcRel P _ _ + simp only [lcRel] + apply leftCoset_eq_of_not_disjoint + rw [Set.not_disjoint_iff] + refine ⟨β * k₀ * g₁', ⟨1, P.H.one_mem, by simp⟩, ?_⟩ + refine ⟨g₁'⁻¹ * (n' : G)⁻¹ * g₁', conjAct_inv_mem_of_subgroupOf P g₁' n', ?_⟩ + simp only [smul_eq_mul, hk'_coe] + group + +private lemma iter_smulOrbit_mem_mulSupport_smulOrbit (g₂ g₁ β₀ : P.Δ) + (j x₀ : HeckeLeftCoset P) (hj : j ∈ smulOrbit P g₂ β₀) + (hx₀ : x₀ ∈ smulOrbit P g₁ (HeckeLeftCoset.rep j)) : + ∃ D, D ∈ mulSupport P g₂ g₁ ∧ x₀ ∈ smulOrbit P (HeckeCoset.rep D) β₀ := by + simp only [smulOrbit, Finset.mem_image] at hj hx₀ + obtain ⟨i₀, _, hj_eq⟩ := hj + obtain ⟨k₀, _, hx₀_eq⟩ := hx₀ + set β := (HeckeLeftCoset.rep j : G) + have h_rep_mem : (g₂ : G)⁻¹ * (i₀.out : G)⁻¹ * (β₀ : G)⁻¹ * β ∈ P.H := + rep_mem_H_of_smulOrbit_eq P g₂ β₀ i₀ j hj_eq + set k' : decompQuot P g₁ := + ⟦⟨(g₂ : G)⁻¹ * (i₀.out : G)⁻¹ * (β₀ : G)⁻¹ * β * (k₀.out : G), + P.H.mul_mem h_rep_mem k₀.out.2⟩⟧ + refine ⟨mulMap P g₂ g₁ (i₀, k'), + Finset.mem_image_of_mem _ (Finset.mem_univ _), ?_⟩ + rw [← hx₀_eq] + obtain ⟨n', hn'_eq⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (g₁ : G) • P.H).subgroupOf P.H) + ⟨(g₂ : G)⁻¹ * (i₀.out : G)⁻¹ * (β₀ : G)⁻¹ * β * (k₀.out : G), + P.H.mul_mem h_rep_mem k₀.out.2⟩ + rw [iter_connector_class_eq P (β₀ : G) β (g₁ : G) (g₂ : G) (i₀.out : G) (k₀.out : G) + (k'.out : G) n' (mk_out_coe_eq_mul P hn'_eq) _ + (Submonoid.mul_mem _ (Submonoid.mul_mem _ + (delta_mul_mem P.H P.Δ i₀.out β₀ g₂ P.h₀) (P.h₀ k'.out.2)) g₁.2)] + exact iter_mem_smulOrbit_mulMap P g₂ g₁ β₀ i₀ k' + +private lemma smulOrbit_indicator_eq_sum (g₁ : P.Δ) (x₀ : HeckeLeftCoset P) (β : P.Δ) : + (if x₀ ∈ smulOrbit P g₁ β then (1 : ℤ) else 0) = + ∑ k : decompQuot P g₁, + if (⟦⟨(β : G) * (k.out : G) * (g₁ : G), + delta_mul_mem P.H P.Δ k.out β g₁ P.h₀⟩⟧ : + HeckeLeftCoset P) = x₀ then 1 else 0 := by + classical + by_cases hmem : x₀ ∈ smulOrbit P g₁ β + · rw [if_pos hmem] + simp only [smulOrbit, Finset.mem_image] at hmem + obtain ⟨q₀, _, hq₀⟩ := hmem + rw [Finset.sum_eq_single q₀] + · exact (if_pos hq₀).symm + · intro q _ hne + rw [if_neg] + exact fun heq ↦ hne (smulOrbit_map_injective P g₁ β (heq.trans hq₀.symm)) + · exact fun h ↦ absurd (Finset.mem_univ _) h + · rw [if_neg hmem] + exact (Finset.sum_eq_zero fun q _ ↦ if_neg fun heq ↦ + hmem (Finset.mem_image.mpr ⟨q, Finset.mem_univ _, heq⟩)).symm + +private lemma singleton_coset_factor_iff (a x g₂ y g₁ z₁ z₂ : G) : + ({a * x * g₂ * y * g₁} : Set G) * ↑P.H = {a * z₁ * z₂} * ↑P.H ↔ + ({x * g₂} : Set G) * {y * g₁} * ↑P.H = {z₁ * z₂} * ↑P.H := by + have hl : ({a * x * g₂ * y * g₁} : Set G) = + ({a} : Set G) * {x * g₂ * (y * g₁)} := by + rw [Set.singleton_mul_singleton] + congr 1 + group + have hr : ({a * z₁ * z₂} : Set G) = ({a} : Set G) * {z₁ * z₂} := by + rw [Set.singleton_mul_singleton] + congr 1 + group + constructor + · intro h + have hset' : ({a} : Set G) * ({x * g₂ * (y * g₁)} * ↑P.H) = + {a} * ({z₁ * z₂} * ↑P.H) := by + rwa [← mul_assoc, ← hl, ← mul_assoc, ← hr] + rw [Set.singleton_mul_singleton] + exact set_singleton_mul_left_cancel a hset' + · intro h + rw [Set.singleton_mul_singleton] at h + calc ({a * x * g₂ * y * g₁} : Set G) * ↑P.H + _ = ({a} * {x * g₂ * (y * g₁)}) * ↑P.H := by rw [hl] + _ = {a} * ({x * g₂ * (y * g₁)} * ↑P.H) := mul_assoc _ _ _ + _ = {a} * ({z₁ * z₂} * ↑P.H) := congr_arg _ h + _ = ({a} * {z₁ * z₂}) * ↑P.H := (mul_assoc _ _ _).symm + _ = ({a * z₁ * z₂} : Set G) * ↑P.H := by rw [hr] + +private lemma smulOrbit_count_eq_m' (g₂ g₁ : P.Δ) (D₀ : HeckeCoset P) (β₀ : P.Δ) + (x₀ : HeckeLeftCoset P) (hx₀ : x₀ ∈ smulOrbit P (HeckeCoset.rep D₀) β₀) : + (∑ j ∈ smulOrbit P g₂ β₀, + if x₀ ∈ smulOrbit P g₁ (HeckeLeftCoset.rep j) then (1 : ℤ) else 0) = + (m P g₂ g₁) D₀ := by + simp only [smulOrbit, Finset.mem_image] at hx₀ + obtain ⟨q₀, _, hq₀⟩ := hx₀ + have h_lhs_eq : ∀ q : decompQuot P g₂, + smulOrbit P g₁ (HeckeLeftCoset.rep + (⟦⟨(β₀ : G) * (q.out : G) * (g₂ : G), + delta_mul_mem P.H P.Δ q.out β₀ g₂ P.h₀⟩⟧ : HeckeLeftCoset P)) = + smulOrbit P g₁ ⟨(β₀ : G) * (q.out : G) * (g₂ : G), + delta_mul_mem P.H P.Δ q.out β₀ g₂ P.h₀⟩ := fun q ↦ + smulOrbit_lcRel P g₁ + (Quotient.exact (Quotient.out_eq + (⟦⟨(β₀ : G) * (q.out : G) * (g₂ : G), + delta_mul_mem P.H P.Δ q.out β₀ g₂ P.h₀⟩⟧ : HeckeLeftCoset P))) + set F : HeckeLeftCoset P → ℤ := + fun j ↦ if x₀ ∈ smulOrbit P g₁ (HeckeLeftCoset.rep j) then 1 else 0 with hF_def + conv_lhs => rw [smulOrbit, Finset.top_eq_univ] + rw [Finset.sum_image (f := F) fun a _ b _ hab ↦ smulOrbit_map_injective P g₂ β₀ hab] + simp only [hF_def, h_lhs_eq] + simp_rw [smulOrbit_indicator_eq_sum P g₁ x₀] + simp_rw [← hq₀, fun a b : P.Δ ↦ + (⟨fun h ↦ Quotient.exact h, fun h ↦ Quotient.sound h⟩ : + (⟦a⟧ : HeckeLeftCoset P) = ⟦b⟧ ↔ ({(a : G)} : Set G) * ↑P.H = {(b : G)} * ↑P.H)] + rw [← Fintype.sum_prod_type', Finset.sum_boole, ← Fintype.card_subtype, + ← Nat.card_eq_fintype_card] + simp_rw [fun p : decompQuot P g₂ × decompQuot P g₁ ↦ + propext (singleton_coset_factor_iff P (β₀ : G) p.1.out (g₂ : G) p.2.out (g₁ : G) + (q₀.out : G) (HeckeCoset.rep D₀ : G))] + change _ = (heckeMultiplicity P g₂ g₁ (HeckeCoset.rep D₀) : ℤ) + unfold heckeMultiplicity + norm_cast + exact heckeMultiplicity_uniform P g₂ g₁ D₀ q₀ + +private lemma finsupp_sum_single_orbit (orbit : Finset (HeckeLeftCoset P)) (val : ℤ) + (f : HeckeLeftCoset P → ℤ → ℤ) (hf0 : ∀ a, f a 0 = 0) + (hfadd : ∀ a b₁ b₂, f a (b₁ + b₂) = f a b₁ + f a b₂) : + (∑ j ∈ orbit, Finsupp.single j val).sum f = ∑ j ∈ orbit, f j val := by + rw [← Finsupp.sum_finsetSum_index (h_zero := hf0) (h_add := hfadd)] + exact Finset.sum_congr rfl fun j _ ↦ Finsupp.sum_single_index (hf0 j) + +/-- Positive case of `smul_assoc_key`: if some `D₀ ∈ (m g₂ g₁).support` covers `x₀`, +LHS reduces to `(m g₂ g₁) D₀` and RHS matches by `smulOrbit_count_eq_m'`. -/ +private lemma smul_assoc_key_apply_pos (g₁ g₂ β₀ : P.Δ) (x₀ : HeckeLeftCoset P) + (h_ex : ∃ D₀ ∈ (m P g₂ g₁).support, + x₀ ∈ smulOrbit P (HeckeCoset.rep D₀) β₀) : + ((m P g₂ g₁).sum fun a₁ b ↦ + if x₀ ∈ smulOrbit P (HeckeCoset.rep a₁) β₀ then b else (0 : ℤ)) = + ∑ j ∈ smulOrbit P g₂ β₀, + if x₀ ∈ smulOrbit P g₁ (HeckeLeftCoset.rep j) then 1 else 0 := by + obtain ⟨D₀, hD₀, hx₀⟩ := h_ex + have h_lhs : (m P g₂ g₁).sum (fun a₁ b ↦ + if x₀ ∈ smulOrbit P (HeckeCoset.rep a₁) β₀ then b + else (0 : ℤ)) = (m P g₂ g₁) D₀ := by + rw [Finsupp.sum, Finset.sum_eq_single D₀ + (fun D _ hne ↦ if_neg (Finset.disjoint_left.mp + (smulOrbit_disjoint_of_ne P (HeckeCoset.rep D₀) (HeckeCoset.rep D) β₀ + (by simp only [HeckeCoset.rep, Quotient.out_eq]; exact hne.symm)) hx₀)) + (fun h ↦ absurd hD₀ h)] + exact if_pos hx₀ + rw [h_lhs] + exact (smulOrbit_count_eq_m' P g₂ g₁ D₀ β₀ x₀ hx₀).symm + +/-- Negative case of `smul_assoc_key`: if no `D₀` covers `x₀`, both sides are zero — +LHS by hypothesis, RHS by `iter_smulOrbit_mem_mulSupport_smulOrbit`. -/ +private lemma smul_assoc_key_apply_neg (g₁ g₂ β₀ : P.Δ) (x₀ : HeckeLeftCoset P) + (h_ex : ∀ D₀ ∈ (m P g₂ g₁).support, + x₀ ∉ smulOrbit P (HeckeCoset.rep D₀) β₀) : + ((m P g₂ g₁).sum fun a₁ b ↦ + if x₀ ∈ smulOrbit P (HeckeCoset.rep a₁) β₀ then b else (0 : ℤ)) = + ∑ j ∈ smulOrbit P g₂ β₀, + if x₀ ∈ smulOrbit P g₁ (HeckeLeftCoset.rep j) then 1 else 0 := by + have h_lhs : (m P g₂ g₁).sum (fun a₁ b ↦ + if x₀ ∈ smulOrbit P (HeckeCoset.rep a₁) β₀ then b + else (0 : ℤ)) = 0 := by + rw [Finsupp.sum] + exact Finset.sum_eq_zero fun D hD ↦ if_neg (h_ex D hD) + rw [h_lhs] + exact (Finset.sum_eq_zero fun j hj ↦ by + simp only [ite_eq_right_iff, one_ne_zero] + intro hmem + obtain ⟨D, hD, hD_mem⟩ := + iter_smulOrbit_mem_mulSupport_smulOrbit P g₂ g₁ β₀ j x₀ hj hmem + exact absurd hD_mem (h_ex D hD)).symm + +private lemma smul_assoc_key (g₁ g₂ β₀ : P.Δ) : + ((m P g₂ g₁).sum fun D b₁ ↦ + ∑ i ∈ smulOrbit P (HeckeCoset.rep D) β₀, Finsupp.single i (b₁ * 1)) = + (∑ j ∈ smulOrbit P g₂ β₀, + Finsupp.single j 1).sum + fun m b₂ ↦ ∑ i ∈ smulOrbit P g₁ (HeckeLeftCoset.rep m), + Finsupp.single i (1 * b₂) := by + simp only [mul_one, one_mul] + ext x₀ + simp only [Finsupp.sum_apply, Finsupp.finsetSum_apply, Finsupp.single_apply] + simp_rw [Finset.sum_ite_eq'] + rw [finsupp_sum_single_orbit P _ 1 _ (fun a ↦ by simp) + (fun a b₁ b₂ ↦ by split_ifs <;> simp [*])] + by_cases h_ex : ∃ D₀ ∈ (m P g₂ g₁).support, + x₀ ∈ smulOrbit P (HeckeCoset.rep D₀) β₀ + · exact smul_assoc_key_apply_pos P g₁ g₂ β₀ x₀ h_ex + · push Not at h_ex + exact smul_assoc_key_apply_neg P g₁ g₂ β₀ x₀ h_ex + +private lemma smul_assoc_singles_lhs_apply (D₁ D₂ : HeckeCoset P) (a₁ a₂ : ℤ) + (m₀ x₀ : HeckeLeftCoset P) (c₀ : ℤ) : + ((a₂ • a₁ • m P D₂.rep D₁.rep).sum fun D1 b₁ ↦ + ∑ i ∈ smulOrbit P D1.rep m₀.rep, Finsupp.single i (b₁ * c₀)) x₀ = + a₁ * a₂ * c₀ * + (m P D₂.rep D₁.rep).sum + (fun D b₁ ↦ if x₀ ∈ smulOrbit P D.rep m₀.rep then b₁ else (0 : ℤ)) := by + simp only [Finsupp.sum_apply, Finsupp.finsetSum_apply, Finsupp.single_apply] + simp_rw [Finset.sum_ite_eq'] + have h_lhs : (a₂ • a₁ • m P D₂.rep D₁.rep).sum + (fun D b₁ ↦ if x₀ ∈ smulOrbit P D.rep m₀.rep then b₁ * c₀ else (0 : ℤ)) = + (m P D₂.rep D₁.rep).sum + (fun D b₁ ↦ + if x₀ ∈ smulOrbit P D.rep m₀.rep then a₂ * (a₁ * b₁) * c₀ + else (0 : ℤ)) := by + rw [Finsupp.sum_smul_index (fun i ↦ by split_ifs <;> simp), + Finsupp.sum_smul_index (fun i ↦ by split_ifs <;> simp)] + rw [h_lhs, Finsupp.mul_sum] + refine Finset.sum_congr rfl fun D _ ↦ ?_ + dsimp only + split_ifs <;> ring + +private lemma smul_assoc_singles_rhs_apply (D₁ D₂ : HeckeCoset P) (a₁ a₂ : ℤ) + (m₀ x₀ : HeckeLeftCoset P) (c₀ : ℤ) : + ((∑ i ∈ smulOrbit P D₂.rep m₀.rep, Finsupp.single i (a₂ * c₀)).sum fun m b₂ ↦ + ∑ i ∈ smulOrbit P D₁.rep m.rep, Finsupp.single i (a₁ * b₂)) x₀ = + a₁ * a₂ * c₀ * + ∑ j ∈ smulOrbit P D₂.rep m₀.rep, + if x₀ ∈ smulOrbit P D₁.rep j.rep then (1 : ℤ) else 0 := by + simp only [Finsupp.sum_apply, Finsupp.finsetSum_apply, Finsupp.single_apply] + simp_rw [Finset.sum_ite_eq'] + rw [finsupp_sum_single_orbit P _ (a₂ * c₀) _ (fun a ↦ by simp) + (fun a b₁ b₂ ↦ by split_ifs <;> simp [*, mul_add])] + rw [Finset.mul_sum] + refine Finset.sum_congr rfl fun j _ ↦ ?_ + split_ifs <;> ring + +private lemma smul_assoc_singles_sum_eq (D₁ D₂ : HeckeCoset P) (a₁ a₂ : ℤ) + (m₀ : HeckeLeftCoset P) (c₀ : ℤ) : + ((a₂ • a₁ • m P D₂.rep D₁.rep).sum fun D1 b₁ ↦ + ∑ i ∈ smulOrbit P D1.rep m₀.rep, Finsupp.single i (b₁ * c₀)) = + (∑ i ∈ smulOrbit P D₂.rep m₀.rep, Finsupp.single i (a₂ * c₀)).sum fun m b₂ ↦ + ∑ i ∈ smulOrbit P D₁.rep m.rep, Finsupp.single i (a₁ * b₂) := by + ext x₀ + rw [smul_assoc_singles_lhs_apply P D₁ D₂ a₁ a₂ m₀ x₀ c₀, + smul_assoc_singles_rhs_apply P D₁ D₂ a₁ a₂ m₀ x₀ c₀] + congr 1 + have key := smul_assoc_key P D₁.rep D₂.rep m₀.rep + simp only [mul_one, one_mul] at key + have key_pt := DFunLike.congr_fun key x₀ + simp only [Finsupp.sum_apply, Finsupp.finsetSum_apply, Finsupp.single_apply] at key_pt + simp_rw [Finset.sum_ite_eq'] at key_pt + rw [key_pt] + exact finsupp_sum_single_orbit P _ 1 _ (fun a ↦ by simp) + (fun a b₁ b₂ ↦ by split_ifs <;> simp [*]) + +private lemma smul_assoc_singles (D₁ D₂ : HeckeCoset P) (a₁ a₂ : ℤ) + (m₀ : HeckeLeftCoset P) (c₀ : ℤ) : + (T_single P ℤ D₂ a₂ * T_single P ℤ D₁ a₁) • + (HeckeLeftCoset_single P ℤ m₀ c₀) = + T_single P ℤ D₁ a₁ • + (T_single P ℤ D₂ a₂ • HeckeLeftCoset_single P ℤ m₀ c₀) := by + rw [mul_singleton_𝕋, single_smul_single] + simp only [smul_eq_sum, HeckeLeftCoset_single, T_single] + have hsi : ∀ (D : HeckeCoset P) (b : ℤ), + (Finsupp.single m₀ c₀).sum (fun m b₂ ↦ + ∑ i ∈ smulOrbit P (HeckeCoset.rep D) (HeckeLeftCoset.rep m), + Finsupp.single i (b * b₂)) = + ∑ i ∈ smulOrbit P (HeckeCoset.rep D) (HeckeLeftCoset.rep m₀), + Finsupp.single i (b * c₀) := by + intro D b + rw [Finsupp.sum_single_index (by + simp [mul_zero, Finsupp.single_zero, + Finset.sum_const_zero])] + simp_rw [hsi] + rw [Finsupp.sum_single_index (by simp [zero_mul, Finsupp.single_zero, Finset.sum_const_zero])] + exact smul_assoc_singles_sum_eq P D₁ D₂ a₁ a₂ m₀ c₀ + +/-- The module action satisfies the scalar tower property `(x * y) • z = y • (x • z)`, +which is equivalent to associativity of multiplication (Shimura Proposition 3.4). -/ +noncomputable instance instIsScalarTower : + IsScalarTower (𝕋 P ℤ) (𝕋 P ℤ) (HeckeModule P ℤ) where + smul_assoc x y z := by + show (x • y) • z = x • (y • z) + have hsmul : ∀ a b : 𝕋 P ℤ, a • b = b * a := fun _ _ ↦ rfl + rw [hsmul x y] + -- View Finsupp values as 𝕋 P ℤ via a thin wrapper. + let toT : (HeckeCoset P →₀ ℤ) → 𝕋 P ℤ := fun a ↦ a + let toM : (HeckeLeftCoset P →₀ ℤ) → HeckeModule P ℤ := fun a ↦ a + let motx : (HeckeCoset P →₀ ℤ) → Prop := + fun x' ↦ (y * (toT x')) • z = (toT x') • (y • z) + change motx x + apply Finsupp.induction_linear + · -- x = 0 + show (y * (toT 0)) • z = (toT 0) • y • z + change (y * (0 : 𝕋 P ℤ)) • z = ((0 : 𝕋 P ℤ)) • y • z + rw [mul_zero, zero_smul_HeckeModule, zero_smul_HeckeModule] + · -- x = x₁ + x₂ + intro x₁ x₂ ih₁ ih₂ + show (y * (toT (x₁ + x₂))) • z = (toT (x₁ + x₂)) • y • z + change (y * ((toT x₁) + (toT x₂))) • z = ((toT x₁) + (toT x₂)) • y • z + rw [mul_add, smul_add_left, ih₁, ih₂, ← smul_add_left] + · -- x = single D₁ a₁ + intro D₁ a₁ + show (y * (toT (Finsupp.single D₁ a₁))) • z = + (toT (Finsupp.single D₁ a₁)) • y • z + -- Now induct on y. + let motY : (HeckeCoset P →₀ ℤ) → Prop := + fun Y' ↦ ((toT Y') * (toT (Finsupp.single D₁ a₁))) • z = + (toT (Finsupp.single D₁ a₁)) • (toT Y') • z + change motY y + apply Finsupp.induction_linear + · show ((toT 0) * (toT (Finsupp.single D₁ a₁))) • z = + (toT (Finsupp.single D₁ a₁)) • (toT 0) • z + change (((0 : 𝕋 P ℤ)) * (toT (Finsupp.single D₁ a₁))) • z = + (toT (Finsupp.single D₁ a₁)) • ((0 : 𝕋 P ℤ)) • z + rw [zero_mul, zero_smul_HeckeModule, smul_zero_HeckeModule] + · intro y₁ y₂ ih₁ ih₂ + show ((toT (y₁ + y₂)) * (toT (Finsupp.single D₁ a₁))) • z = + (toT (Finsupp.single D₁ a₁)) • (toT (y₁ + y₂)) • z + change ((toT y₁ + toT y₂) * (toT (Finsupp.single D₁ a₁))) • z = + (toT (Finsupp.single D₁ a₁)) • (toT y₁ + toT y₂) • z + rw [add_mul, smul_add_left, ih₁, ih₂, smul_add_left, smul_add_right] + · intro D₂ a₂ + show ((toT (Finsupp.single D₂ a₂)) * (toT (Finsupp.single D₁ a₁))) • z = + (toT (Finsupp.single D₁ a₁)) • (toT (Finsupp.single D₂ a₂)) • z + -- Now induct on z. + let motZ : (HeckeLeftCoset P →₀ ℤ) → Prop := + fun z' ↦ ((toT (Finsupp.single D₂ a₂)) * + (toT (Finsupp.single D₁ a₁))) • (toM z') = + (toT (Finsupp.single D₁ a₁)) • + (toT (Finsupp.single D₂ a₂)) • (toM z') + change motZ z + apply Finsupp.induction_linear + · show ((toT (Finsupp.single D₂ a₂)) * (toT (Finsupp.single D₁ a₁))) • (toM 0) = + (toT (Finsupp.single D₁ a₁)) • (toT (Finsupp.single D₂ a₂)) • (toM 0) + change ((toT (Finsupp.single D₂ a₂)) * + (toT (Finsupp.single D₁ a₁))) • (0 : HeckeModule P ℤ) = + (toT (Finsupp.single D₁ a₁)) • + (toT (Finsupp.single D₂ a₂)) • (0 : HeckeModule P ℤ) + rw [smul_zero_HeckeModule, smul_zero_HeckeModule, smul_zero_HeckeModule] + · intro z₁ z₂ ih₁ ih₂ + show ((toT (Finsupp.single D₂ a₂)) * (toT (Finsupp.single D₁ a₁))) • + (toM (z₁ + z₂)) = + (toT (Finsupp.single D₁ a₁)) • + (toT (Finsupp.single D₂ a₂)) • (toM (z₁ + z₂)) + change ((toT (Finsupp.single D₂ a₂)) * (toT (Finsupp.single D₁ a₁))) • + ((toM z₁ + toM z₂) : HeckeModule P ℤ) = + (toT (Finsupp.single D₁ a₁)) • + (toT (Finsupp.single D₂ a₂)) • + ((toM z₁ + toM z₂) : HeckeModule P ℤ) + rw [smul_add_right, smul_add_right, ih₁, ih₂, smul_add_right] + · intro m₀ c₀ + show ((toT (Finsupp.single D₂ a₂)) * (toT (Finsupp.single D₁ a₁))) • + (toM (Finsupp.single m₀ c₀)) = + (toT (Finsupp.single D₁ a₁)) • + (toT (Finsupp.single D₂ a₂)) • (toM (Finsupp.single m₀ c₀)) + exact smul_assoc_singles P D₁ D₂ a₁ a₂ m₀ c₀ diff --git a/LeanBridge/ForMathlib/AbstractHeckeRing/Basic.lean b/LeanBridge/ForMathlib/AbstractHeckeRing/Basic.lean new file mode 100644 index 00000000..397676f1 --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing/Basic.lean @@ -0,0 +1,345 @@ +/- +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.Algebra.Lie.OfAssociative +import Mathlib.Analysis.Normed.Lp.WithLp +import Mathlib.Analysis.Normed.Ring.Lemmas +import Mathlib.Data.Finsupp.Pointwise +import Mathlib.Data.Int.Star +import Mathlib.GroupTheory.Commensurable +import Mathlib.GroupTheory.DoubleCoset +import Mathlib.Order.CompletePartialOrder +import Mathlib.Tactic.Group + +/-! +# Hecke Rings: Basic Definitions + +Basic definitions for Hecke rings following Shimura Ch. 3: `HeckePair`, double coset +spaces `HeckeCoset` and `HeckeLeftCoset`, the Hecke ring type `𝕋` and module type `HeckeModule`, +and foundational double coset lemmas. +-/ + +open Set DoubleCoset Subgroup Subgroup.Commensurable + +open scoped Pointwise + +namespace HeckeRing + +variable {G : Type*} [Group G] (H : Subgroup G) (Δ : Submonoid G) + +/-- The conjugation action on `H` as a set product: `gHg⁻¹ = {g} * H * {g⁻¹}`. -/ +lemma conjAct_smul_coe_eq (g : G) : + ((ConjAct.toConjAct g • H) : Set G) = {g} * H * {g⁻¹} := by + ext x + refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ + · obtain ⟨a, ha⟩ := Set.mem_smul_set.mp h + rw [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct] at ha + rw [← ha.2] + simp only [singleton_mul, image_mul_left, mul_singleton, image_mul_right, + inv_inv, mem_preimage, inv_mul_cancel_right, inv_mul_cancel_left, ha.1] + · refine Set.mem_smul_set.mpr ⟨g⁻¹ * x * g, ?_, + by rw [ConjAct.smul_def, ConjAct.ofConjAct_toConjAct]; group⟩ + simp only [singleton_mul, image_mul_left, mul_singleton, image_mul_right, + inv_inv, mem_preimage, SetLike.mem_coe] at * + rwa [← mul_assoc] at h + +/-- Conjugation by an element of `H` fixes `H`. -/ +lemma conjAct_smul_elt_eq (h : H) : ConjAct.toConjAct (h : G) • H = H := by + have : ConjAct.toConjAct (h : G) • (H : Set G) = H := by + rw [conjAct_smul_coe_eq, Subgroup.singleton_mul_subgroup h.2, + Subgroup.subgroup_mul_singleton (by simp)] + rw [← Subgroup.coe_pointwise_smul] at this; exact_mod_cast this + +/-- 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 _ + +/-- Two elements of `Δ` define the same left coset `gH = hH`. -/ +def lcRel (P : HeckePair G) (g h : P.Δ) : Prop := + ({(g : G)} : Set G) * (P.H : Set G) = {(h : G)} * P.H + +/-- The setoid on `Δ` identifying elements with the same left coset. -/ +instance lcSetoid (P : HeckePair G) : Setoid P.Δ where + r := lcRel P + iseqv := ⟨fun _ ↦ rfl, Eq.symm, Eq.trans⟩ + +/-- A Hecke left coset: an equivalence class of `Δ`-elements under `gH = hH`. -/ +def HeckeLeftCoset (P : HeckePair G) := Quotient (lcSetoid P) + +namespace HeckeCoset + +variable {P : HeckePair G} + +/-- The underlying set `HgH`, well-defined on the quotient. -/ +noncomputable def toSet (D : HeckeCoset P) : Set G := + Quotient.lift (fun (g : P.Δ) ↦ DoubleCoset.doubleCoset (g : G) P.H P.H) + (fun a b (h : @Setoid.r _ (dcSetoid P) a b) ↦ h) D + +/-- A representative `g : Δ` (via `Quotient.out`). -/ +noncomputable def rep (D : HeckeCoset P) : P.Δ := Quotient.out D + +/-- The representative of a `HeckeCoset` maps back to the coset under `⟦·⟧`. -/ +lemma mk_rep (D : HeckeCoset P) : (⟦HeckeCoset.rep D⟧ : HeckeCoset P) = D := + Quotient.out_eq D + +/-- `⟦g⟧ = ⟦h⟧ ↔ HgH = HhH`. -/ +lemma eq_iff (g h : P.Δ) : (⟦g⟧ : HeckeCoset P) = ⟦h⟧ ↔ + DoubleCoset.doubleCoset (g : G) P.H P.H = DoubleCoset.doubleCoset (h : G) P.H P.H := + Quotient.eq (r := dcSetoid P) + +/-- The carrier set of `⟦g⟧` is definitionally `HgH`. -/ +@[simp] lemma toSet_mk (g : P.Δ) : + HeckeCoset.toSet (⟦g⟧ : HeckeCoset P) = DoubleCoset.doubleCoset (g : G) P.H P.H := rfl + +/-- The carrier set equals the double coset of the representative. -/ +lemma toSet_eq_rep (D : HeckeCoset P) : + HeckeCoset.toSet D = DoubleCoset.doubleCoset (HeckeCoset.rep D : G) P.H P.H := by + refine Quotient.inductionOn D fun g ↦ ?_ + simpa only [toSet_mk, HeckeCoset.rep] using + (Quotient.exact (Quotient.out_eq (⟦g⟧ : HeckeCoset P))).symm + +/-- The representative lies in its double coset. -/ +lemma rep_mem (D : HeckeCoset P) : (HeckeCoset.rep D : G) ∈ HeckeCoset.toSet D := + toSet_eq_rep D ▸ DoubleCoset.mem_doubleCoset_self P.H P.H _ + +/-- If `x ∈ HgH`, then `HxH = HgH`. The fundamental double coset absorption lemma. -/ +lemma doubleCoset_eq_of_mem {g : P.Δ} {x : G} + (hx : x ∈ DoubleCoset.doubleCoset (g : G) P.H P.H) : + DoubleCoset.doubleCoset x P.H P.H = DoubleCoset.doubleCoset (g : G) P.H P.H := by + obtain ⟨_, ⟨l, hl, _, rfl, rfl⟩, r, hr, rfl⟩ := hx + simp only [DoubleCoset.doubleCoset] + ext y; simp only [Set.mem_mul, Set.mem_singleton_iff, SetLike.mem_coe] + constructor + · rintro ⟨_, ⟨a, ha, _, rfl, rfl⟩, b, hb, rfl⟩ + exact ⟨_, ⟨a * l, P.H.mul_mem ha hl, _, rfl, rfl⟩, r * b, P.H.mul_mem hr hb, by group⟩ + · rintro ⟨_, ⟨a, ha, _, rfl, rfl⟩, b, hb, rfl⟩ + exact ⟨_, ⟨a * l⁻¹, P.H.mul_mem ha (P.H.inv_mem hl), _, rfl, rfl⟩, + r⁻¹ * b, P.H.mul_mem (P.H.inv_mem hr) hb, by group⟩ + +/-- `⟦g₁⟧ = ⟦g₂⟧` when `g₁` is in the double coset of `g₂`. -/ +lemma eq_mk_of_mem {g₁ g₂ : P.Δ} + (h : (g₁ : G) ∈ DoubleCoset.doubleCoset (g₂ : G) P.H P.H) : + (⟦g₁⟧ : HeckeCoset P) = ⟦g₂⟧ := + (eq_iff g₁ g₂).mpr (doubleCoset_eq_of_mem h) + +/-- The identity double coset `H1H = H`. -/ +def one (P : HeckePair G) : HeckeCoset P := ⟦⟨1, P.Δ.one_mem⟩⟧ + +/-- Induction: to prove something for all double cosets, prove it for `⟦g⟧`. -/ +protected lemma ind {motive : HeckeCoset P → Prop} + (h : ∀ g : P.Δ, motive ⟦g⟧) : ∀ D, motive D := Quotient.ind h + +/-- Two-argument induction. -/ +protected lemma ind₂ {motive : HeckeCoset P → HeckeCoset P → Prop} + (h : ∀ g₁ g₂ : P.Δ, motive ⟦g₁⟧ ⟦g₂⟧) : + ∀ D₁ D₂, motive D₁ D₂ := Quotient.ind₂ h + +/-- The representative of `HeckeCoset.one` belongs to `H`. -/ +lemma one_rep_mem_H (P : HeckePair G) : ((one P).rep : G) ∈ P.H := by + have hm := rep_mem (one P) + rw [toSet_eq_rep, + show DoubleCoset.doubleCoset ((rep (one P)) : G) P.H P.H = + DoubleCoset.doubleCoset (1 : G) P.H P.H from + Quotient.exact (Quotient.out_eq (⟦⟨(1 : G), P.Δ.one_mem⟩⟧ : HeckeCoset P)), + mem_doubleCoset] at hm + obtain ⟨a, ha, b, hb, hab⟩ := hm + rw [mul_one] at hab + exact hab ▸ P.H.mul_mem ha hb + +end HeckeCoset + +namespace HeckeLeftCoset + +variable {P : HeckePair G} + +/-- The underlying set `gH`, well-defined on the quotient. -/ +noncomputable def toSet (D : HeckeLeftCoset P) : Set G := + Quotient.lift (fun (g : P.Δ) ↦ ({(g : G)} : Set G) * (P.H : Set G)) + (fun _ _ (h : lcRel P _ _) ↦ h) D + +/-- A representative `g : Δ`. -/ +noncomputable def rep (D : HeckeLeftCoset P) : P.Δ := Quotient.out D + +/-- The identity left coset `1H = H`. -/ +def one (P : HeckePair G) : HeckeLeftCoset P := ⟦⟨1, P.Δ.one_mem⟩⟧ + +/-- Induction for left cosets. -/ +protected lemma ind {motive : HeckeLeftCoset P → Prop} + (h : ∀ g : P.Δ, motive ⟦g⟧) : ∀ D, motive D := Quotient.ind h + +end HeckeLeftCoset + +/-- Left-multiplying the representative by an element of `H` does not change the double coset. -/ +lemma doset_mul_left_eq_self (P : HeckePair G) (h : P.H) (g : G) : + DoubleCoset.doubleCoset ((h : G) * g) P.H P.H = + DoubleCoset.doubleCoset g P.H P.H := by + simp_rw [DoubleCoset.doubleCoset, ← Set.singleton_mul_singleton, ← mul_assoc] + conv => enter [1, 1, 1]; rw [Subgroup.subgroup_mul_singleton h.2] + +/-- Right-multiplying the representative by an element of `H` does not change the double coset. -/ +lemma DoubleCoset.doubleCoset_mul_right_eq_self (P : HeckePair G) + (h : P.H) (g : G) : DoubleCoset.doubleCoset (g * h) P.H P.H = + DoubleCoset.doubleCoset g P.H P.H := by + simp_rw [DoubleCoset.doubleCoset, ← Set.singleton_mul_singleton, ← mul_assoc] + conv => enter [1]; rw [mul_assoc, Subgroup.singleton_mul_subgroup h.2] + +/-- Scalar multiplication by a group element is the same as singleton set multiplication. -/ +lemma smul_eq_singleton_mul (s : Set G) (g : G) : g • s = {g} * s := + Set.singleton_smul.symm + +/-- A subgroup `H` is the union of left cosets of any sub-subgroup `K ≤ H`. -/ +lemma set_eq_iUnion_leftCosets (K : Subgroup G) (hK : K ≤ H) : + (H : Set G) = ⋃ (i : H ⧸ K.subgroupOf H), (i.out : G) • (K : Set G) := by + ext a + refine ⟨fun ha ↦ ?_, fun ha ↦ ?_⟩ + · simp only [Set.mem_iUnion] + refine ⟨(⟨a, ha⟩ : H), ?_⟩ + obtain ⟨h, hh⟩ := QuotientGroup.mk_out_eq_mul (K.subgroupOf H) (⟨a, ha⟩ : H) + rw [hh] + simp only [coe_mul] + refine Set.mem_smul_set.mpr ⟨h⁻¹, ?_, ?_⟩ + · simpa using Subgroup.mem_subgroupOf.mp (SetLike.coe_mem h) + · simp + · simp only [Set.mem_iUnion] at ha + obtain ⟨i, h, hh, rfl⟩ := ha + show ((Quotient.out i : H) : G) * h ∈ H + exact mul_mem (by simp) (hK hh) + +/-- The conjugate subgroup `gHg⁻¹` is closed under multiplication. -/ +lemma conjAct_mul_self_eq_self (g : G) : + ((ConjAct.toConjAct g • H) : Set G) * (ConjAct.toConjAct g • H) = + (ConjAct.toConjAct g • H) := by + rw [conjAct_smul_coe_eq, + show {g} * (H : Set G) * {g⁻¹} * ({g} * ↑H * {g⁻¹}) = + {g} * ↑H * (({g⁻¹} * {g}) * ↑H) * {g⁻¹} by simp_rw [← mul_assoc], + Set.singleton_mul_singleton] + conv => enter [1, 1, 2]; simp only [inv_mul_cancel, Set.singleton_one, one_mul] + conv => enter [1, 1]; rw [mul_assoc, coe_mul_coe H] + +/-- The intersection `H ∩ gHg⁻¹` acts trivially on `gHg⁻¹` by left multiplication. -/ +lemma inter_mul_conjAct_eq_conjAct (g : G) : + ((H : Set G) ∩ (ConjAct.toConjAct g • H)) * (ConjAct.toConjAct g • H) = + (ConjAct.toConjAct g • H) := + Subset.antisymm + (le_trans (Set.inter_mul_subset (s₁ := (H : Set G)) + (s₂ := (ConjAct.toConjAct g • H)) (t := (ConjAct.toConjAct g • H))) + (by simp [conjAct_mul_self_eq_self])) + (subset_mul_right _ ⟨Subgroup.one_mem H, Subgroup.one_mem (ConjAct.toConjAct g • H)⟩) + +/-- Right multiplication by a singleton is cancellative. -/ +lemma mul_singleton_right_cancel (g : G) (K L : Set G) (h : K * {g} = L * {g}) : K = L := by + have h2 := congrFun (congrArg HMul.hMul h) {g⁻¹} + simp_rw [mul_assoc, Set.singleton_mul_singleton] at h2; simpa using h2 + +/-- A double coset `HgH` decomposes as a disjoint union of left cosets of `H`. -/ +lemma DoubleCoset.doubleCoset_eq_iUnion_leftCosets (g : G) : + DoubleCoset.doubleCoset g H H = + ⋃ (i : H ⧸ (ConjAct.toConjAct g • H).subgroupOf H), + (i.out * g) • (H : Set G) := by + rw [DoubleCoset.doubleCoset] + have := set_eq_iUnion_leftCosets H + (((ConjAct.toConjAct g • H).subgroupOf H).map H.subtype) + simp only [Subgroup.subgroupOf_map_subtype, inf_le_right, Subgroup.coe_inf, + Subgroup.coe_pointwise_smul, true_implies] at this + have h2 := congrFun (congrArg HMul.hMul this) + ((ConjAct.toConjAct g • H) : Set G) + rw [Set.iUnion_mul, inter_comm] at h2 + apply mul_singleton_right_cancel g⁻¹ + rw [conjAct_smul_coe_eq] at * + simp_rw [← mul_assoc] at h2 + rw [h2, show (Subgroup.map H.subtype + ((ConjAct.toConjAct g • H).subgroupOf H)).subgroupOf H = + (ConjAct.toConjAct g • H).subgroupOf H by simp] + have h1 : ∀ (i : H ⧸ (ConjAct.toConjAct g • H).subgroupOf H), + ((i.out) : G) • ((H : Set G) ∩ ({g} * ↑H * {g⁻¹})) * + {g} * ↑H * {g⁻¹} = + (↑(Quotient.out i) * g) • ↑H * {g⁻¹} := by + intro i + have := inter_mul_conjAct_eq_conjAct H g + rw [conjAct_smul_coe_eq] at this + simp_rw [smul_mul_assoc] + simp_rw [← mul_assoc] at this + conv => enter [1, 2]; rw [this] + simp_rw [smul_eq_singleton_mul, ← Set.singleton_mul_singleton, ← mul_assoc] + convert Set.iUnion_congr h1 + rw [Set.iUnion_mul] + +/-- The Hecke ring type: formal `Z`-linear combinations of double cosets `HeckeCoset P`. -/ +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*) [Zero Z] : + FunLike (𝕋 P Z) (HeckeCoset P) Z := + inferInstanceAs (FunLike (HeckeCoset P →₀ Z) (HeckeCoset P) Z) + +/-- The Hecke module type: formal `Z`-linear combinations of left cosets `HeckeLeftCoset P`. -/ +def HeckeModule (P : HeckePair G) (Z : Type*) [Zero Z] := Finsupp (HeckeLeftCoset P) Z + +/-- `FunLike` instance for `HeckeModule P Z`: treat as functions `HeckeLeftCoset P → Z`. -/ +instance instFunLikeHeckeModule (P : HeckePair G) (Z : Type*) [Zero Z] : + FunLike (HeckeModule P Z) (HeckeLeftCoset P) Z := + inferInstanceAs (FunLike (HeckeLeftCoset P →₀ Z) (HeckeLeftCoset P) Z) + +variable (P : HeckePair G) (Z : Type*) [CommRing Z] + +/-- The decomposition quotient `H / (H ∩ gHg⁻¹)` for a concrete `g : Δ`. + Indexes the left cosets in the decomposition of `HgH`. -/ +abbrev decompQuot (P : HeckePair G) (g : P.Δ) := + P.H ⧸ (ConjAct.toConjAct (g : G) • P.H).subgroupOf P.H + +/-- The decomposition quotient is finite because `Δ ≤ commensurator(H)`. -/ +noncomputable instance instFintypeDecompQuot (P : HeckePair G) (g : P.Δ) : + Fintype (decompQuot P g) := + Subgroup.fintypeOfIndexNeZero (P.h₁ g.2).1 + +/-- Products of the form `a · h · b` with `h ∈ H`, `a, b ∈ Δ` remain in `Δ`. -/ +lemma delta_mul_mem (i : H) (a b : Δ) (h₀ : H.toSubmonoid ≤ Δ) : + a * (i : G) * b ∈ Δ := by + rw [mul_assoc]; exact Submonoid.mul_mem _ a.2 (Submonoid.mul_mem _ (h₀ i.2) b.2) + +/-- 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)) + +/-- The additive commutative monoid structure on the Hecke module, for any `AddCommMonoid` of +coefficients. -/ +noncomputable instance instAddCommMonoidHeckeModule (P : HeckePair G) (Z : Type*) + [AddCommMonoid Z] : AddCommMonoid (HeckeModule P Z) := + inferInstanceAs (AddCommMonoid ((HeckeLeftCoset P) →₀ Z)) + +/-- The additive commutative group structure on the Hecke module, when the coefficients form an +`AddCommGroup`. -/ +noncomputable instance instAddCommGroupHeckeModule (P : HeckePair G) (Z : Type*) [AddCommGroup Z] : + AddCommGroup (HeckeModule P Z) := + inferInstanceAs (AddCommGroup ((HeckeLeftCoset P) →₀ Z)) diff --git a/LeanBridge/ForMathlib/AbstractHeckeRing/Module.lean b/LeanBridge/ForMathlib/AbstractHeckeRing/Module.lean new file mode 100644 index 00000000..2e880538 --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing/Module.lean @@ -0,0 +1,268 @@ +/- +Copyright (c) 2024 Chris Birkbeck. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Birkbeck +-/ +import LeanBridge.ForMathlib.AbstractHeckeRing.Multiplication + +/-! +# Hecke Rings: Module Action + +The module action of `𝕋 P ℤ` on `HeckeModule P ℤ` (formal sums of left cosets) and the +faithfulness theorem `eq_of_smul_eq_smul_𝕋`. +-/ + +open Classical + +open scoped Pointwise + +namespace HeckeRing + +variable {G : Type*} [Group G] + +variable (P : HeckePair G) (Z : Type*) [CommRing Z] + +/-- The scalar multiplication on `𝕋` by itself, defined as reverse multiplication. -/ +noncomputable instance (priority := 1200) instSMul𝕋 : SMul (𝕋 P ℤ) (𝕋 P ℤ) where + smul x y := y * x + +/-- The orbit of a left coset representative `β` under double coset representative `g`: +the set of left cosets `{β · σ_i · g | σ_i ∈ H/(H ∩ gHg⁻¹)}`. -/ +noncomputable def smulOrbit (g : P.Δ) (β : P.Δ) : + Finset (HeckeLeftCoset P) := + Finset.image (fun i : decompQuot P g ↦ + (⟦⟨(β : G) * (i.out : G) * (g : G), + delta_mul_mem P.H P.Δ i.out β g P.h₀⟩⟧ : HeckeLeftCoset P)) ⊤ + +/-- The smul orbit of any left coset under any double coset is nonempty. -/ +lemma smulOrbit_nonempty (g : P.Δ) (β : P.Δ) : + (smulOrbit P g β).Nonempty := by simp [smulOrbit] + +/-- The orbit is invariant under left coset equivalence: if `β₁H = β₂H`, then + `smulOrbit g β₁ = smulOrbit g β₂`. This is the key API lemma that lets us + replace `HeckeLeftCoset.rep j` with any representative of `j`. -/ +lemma smulOrbit_lcRel (g : P.Δ) {β₁ β₂ : P.Δ} (h : lcRel P β₁ β₂) : + smulOrbit P g β₁ = smulOrbit P g β₂ := by + ext x + simp only [smulOrbit, Finset.top_eq_univ, Finset.mem_image, Finset.mem_univ, true_and] + suffices hsuff : ∀ (β β' : P.Δ), lcRel P β β' → ∀ i : decompQuot P g, + ∃ j : decompQuot P g, + (⟦⟨(β : G) * (i.out : G) * (g : G), + delta_mul_mem P.H P.Δ i.out β g P.h₀⟩⟧ : HeckeLeftCoset P) = + ⟦⟨(β' : G) * (j.out : G) * (g : G), + delta_mul_mem P.H P.Δ j.out β' g P.h₀⟩⟧ by + refine ⟨fun ⟨i, hi⟩ ↦ ?_, fun ⟨i, hi⟩ ↦ ?_⟩ + · obtain ⟨j, hj⟩ := hsuff β₁ β₂ h i; exact ⟨j, hi ▸ hj.symm⟩ + · obtain ⟨j, hj⟩ := hsuff β₂ β₁ h.symm i; exact ⟨j, hi ▸ hj.symm⟩ + intro β β' hlc i + have hβ'_mem : (β' : G) ∈ ({(β : G)} : Set G) * (P.H : Set G) := + hlc ▸ ⟨β', rfl, 1, P.H.one_mem, mul_one _⟩ + obtain ⟨_, hβ_eq, k, hk, hβ'_eq⟩ := hβ'_mem + rw [Set.mem_singleton_iff] at hβ_eq + subst hβ_eq + set j : decompQuot P g := + ⟦⟨k⁻¹ * i.out, P.H.mul_mem (P.H.inv_mem hk) (SetLike.coe_mem i.out)⟩⟧ + refine ⟨j, Quotient.sound ?_⟩ + show ({(β : G) * (i.out : G) * (g : G)} : Set G) * (P.H : Set G) = + {(β' : G) * (j.out : G) * (g : G)} * P.H + obtain ⟨n, hn_eq⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (g : G) • P.H).subgroupOf P.H) + ⟨k⁻¹ * i.out, P.H.mul_mem (P.H.inv_mem hk) i.out.2⟩ + have hj_coe : (j.out : G) = k⁻¹ * (i.out : G) * (n : G) := by + simpa [Subgroup.coe_mul] using congr_arg (Subtype.val : P.H → G) hn_eq + have hn_conj : (g : G)⁻¹ * (n : G) * g ∈ P.H := by + have := n.2 + rw [Subgroup.mem_subgroupOf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, + ConjAct.smul_def] at this + simpa [ConjAct.ofConjAct_toConjAct] using this + rw [hj_coe, ← hβ'_eq] + conv_rhs => + rw [show (β : G) * k * (k⁻¹ * (i.out : G) * ↑n) * (g : G) = + (β : G) * (i.out : G) * (g : G) * ((g : G)⁻¹ * ↑n * (g : G)) by group, + ← Set.singleton_mul_singleton, mul_assoc] + rw [Subgroup.singleton_mul_subgroup hn_conj] + +/-- The module action of the Hecke ring on formal sums of left cosets. -/ +noncomputable instance instSMulHeckeModule : SMul (𝕋 P Z) (HeckeModule P Z) where + smul t mm := Finsupp.sum t fun D1 b₁ ↦ mm.sum fun m b₂ ↦ + (∑ i ∈ smulOrbit P (HeckeCoset.rep D1) (HeckeLeftCoset.rep m), + Finsupp.single i (b₁ * b₂ : Z) : (HeckeLeftCoset P) →₀ Z) + +/-- The scalar multiplication on `HeckeModule` unfolds as a double sum over orbits. -/ +lemma smul_eq_sum (T : 𝕋 P Z) (m : HeckeModule P Z) : + T • m = Finsupp.sum T (fun D1 b₁ ↦ m.sum fun m b₂ ↦ + (∑ i ∈ smulOrbit P (HeckeCoset.rep D1) (HeckeLeftCoset.rep m), + Finsupp.single i (b₁ * b₂ : Z) : (HeckeLeftCoset P) →₀ Z)) := rfl + +/-- The heterogeneous scalar multiplication instance for the module action. -/ +noncomputable instance instHSMulHeckeModule : + HSMul (𝕋 P Z) (HeckeModule P Z) (HeckeModule P Z) := + inferInstance + +/-- The action of a basis Hecke element on a basis module element. -/ +lemma single_smul_single (t : HeckeCoset P) (m : HeckeLeftCoset P) (a b : Z) : + (instHSMulHeckeModule P Z).hSMul ((Finsupp.single t a) : 𝕋 P Z) + ((Finsupp.single m b) : HeckeModule P Z) = + (∑ i ∈ smulOrbit P (HeckeCoset.rep t) (HeckeLeftCoset.rep m), + Finsupp.single i (a * b : Z) : (HeckeLeftCoset P) →₀ Z) := by + rw [smul_eq_sum] + simp + +/-- The one element of `HeckeModule`: the basis element for the identity left coset. -/ +noncomputable instance instOneHeckeModule : One (HeckeModule P Z) := + ⟨Finsupp.single (HeckeLeftCoset.one P) 1⟩ + +/-- The one element of `HeckeModule` is the basis element corresponding to the identity +left coset. -/ +lemma one_eq_HeckeLeftCoset_single : + (1 : HeckeModule P Z) = Finsupp.single (HeckeLeftCoset.one P) 1 := rfl + +/-- The module action is additive in the Hecke ring argument. -/ +lemma smul_add_left (T₁ T₂ : 𝕋 P Z) (m : HeckeModule P Z) : + (T₁ + T₂) • m = T₁ • m + T₂ • m := by + simp only [smul_eq_sum] + refine Eq.trans (Finsupp.sum_add_index (f := T₁) (g := T₂) ?_ ?_) ?_ + · intro D1 _ + simp only [zero_mul, Finsupp.single_zero, Finset.sum_const_zero, Finsupp.sum_fun_zero] + rfl + · intro D1 _ y b₂ + simp only [Finsupp.sum] + show (∑ x ∈ m.support, ∑ i ∈ smulOrbit P D1.rep x.rep, + Finsupp.single i ((y + b₂) * m x) : HeckeLeftCoset P →₀ Z) = + (∑ x ∈ m.support, ∑ i ∈ smulOrbit P D1.rep x.rep, + Finsupp.single i (y * m x) : HeckeLeftCoset P →₀ Z) + + (∑ x ∈ m.support, ∑ i ∈ smulOrbit P D1.rep x.rep, + Finsupp.single i (b₂ * m x) : HeckeLeftCoset P →₀ Z) + rw [← Finset.sum_add_distrib] + refine Finset.sum_congr rfl fun m _ ↦ ?_ + rw [← Finset.sum_add_distrib] + refine Finset.sum_congr rfl fun i _ ↦ ?_ + rw [add_mul, Finsupp.single_add] + · rfl + +/-- The zero element of the Hecke ring acts as zero on the module. -/ +lemma zero_smul_HeckeModule (z : HeckeModule P Z) : (0 : 𝕋 P Z) • z = 0 := by + simp only [smul_eq_sum]; exact Finsupp.sum_zero_index + +/-- Any Hecke ring element acts as zero on the zero module element. -/ +lemma smul_zero_HeckeModule (T : 𝕋 P Z) : T • (0 : HeckeModule P Z) = 0 := by + simp only [smul_eq_sum] + show Finsupp.sum T (fun D1 b₁ ↦ Finsupp.sum 0 fun m b₂ ↦ + ∑ i ∈ smulOrbit P (HeckeCoset.rep D1) (HeckeLeftCoset.rep m), + Finsupp.single i (b₁ * b₂)) = 0 + simp_rw [Finsupp.sum_zero_index] + exact Finsupp.sum_fun_zero _ + +/-- The module action is additive in the module argument. -/ +lemma smul_add_right (T : 𝕋 P Z) (m₁ m₂ : HeckeModule P Z) : + T • (m₁ + m₂) = T • m₁ + T • m₂ := by + simp only [smul_eq_sum] + have inner_split : ∀ D (b : Z), + (m₁ + m₂).sum (fun m c ↦ + ∑ i ∈ smulOrbit P (HeckeCoset.rep D) (HeckeLeftCoset.rep m), + Finsupp.single i (b * c)) = + m₁.sum (fun m c ↦ + ∑ i ∈ smulOrbit P (HeckeCoset.rep D) (HeckeLeftCoset.rep m), + Finsupp.single i (b * c)) + + m₂.sum (fun m c ↦ + ∑ i ∈ smulOrbit P (HeckeCoset.rep D) (HeckeLeftCoset.rep m), + Finsupp.single i (b * c)) := by + intro D b + refine Eq.trans (Finsupp.sum_add_index' + (f := (m₁ : HeckeLeftCoset P →₀ Z)) (g := m₂) ?_ ?_) ?_ + · intro m + simp + · intro m c₁ c₂ + simp only [← Finset.sum_add_distrib, mul_add, Finsupp.single_add] + · rfl + simp_rw [inner_split] + show Finsupp.sum T (fun D1 b₁ ↦ + Finsupp.sum m₁ (fun m c ↦ ∑ i ∈ smulOrbit P (HeckeCoset.rep D1) (HeckeLeftCoset.rep m), + Finsupp.single i (b₁ * c)) + + Finsupp.sum m₂ (fun m c ↦ ∑ i ∈ smulOrbit P (HeckeCoset.rep D1) (HeckeLeftCoset.rep m), + Finsupp.single i (b₁ * c))) = _ + exact Finsupp.sum_add + +/-- The smul orbits of distinct double cosets acting on the same left coset are disjoint. -/ +lemma smulOrbit_disjoint_of_ne (g₁ g₂ : P.Δ) (β : P.Δ) + (hne : (⟦g₁⟧ : HeckeCoset P) ≠ ⟦g₂⟧) : + Disjoint (smulOrbit P g₁ β) (smulOrbit P g₂ β) := by + rw [Finset.disjoint_left] + intro x hx₁ hx₂ + refine hne <| Quotient.sound (show dcRel P _ _ from ?_) + simp only [smulOrbit, Finset.mem_image] at hx₁ hx₂ + obtain ⟨i₁, _, hi₁⟩ := hx₁ + obtain ⟨i₂, _, hi₂⟩ := hx₂ + rw [← hi₂] at hi₁ + have hset : ({(β : G) * (i₁.out : G) * (g₁ : G)} : Set G) * (P.H : Set G) = + {(β : G) * (i₂.out : G) * (g₂ : G)} * P.H := Quotient.exact hi₁ + have hmem : (β : G) * ↑i₁.out * (g₁ : G) ∈ + ({(β : G) * ↑i₂.out * (g₂ : G)} : Set G) * (↑P.H : Set G) := by + rw [← hset]; exact ⟨_, rfl, 1, P.H.one_mem, mul_one _⟩ + obtain ⟨_, ha, k, hk, hkk⟩ := hmem + rw [Set.mem_singleton_iff] at ha + subst ha + have hstep : ↑i₂.out * (g₂ : G) * k = ↑i₁.out * (g₁ : G) := by + refine mul_left_cancel (a := (β : G)) ?_ + dsimp at hkk + group at hkk ⊢ + exact hkk + have hg : (g₁ : G) = ↑(i₁.out⁻¹ * i₂.out) * (g₂ : G) * k := by + refine mul_left_cancel (a := (↑i₁.out : G)) ?_ + have : ↑i₁.out * (↑(i₁.out⁻¹ * i₂.out) * (g₂ : G) * k) = + ↑i₂.out * (g₂ : G) * k := by + simp only [Subgroup.coe_mul, Subgroup.coe_inv]; group + rw [this]; exact hstep.symm + show DoubleCoset.doubleCoset (g₁ : G) P.H P.H = DoubleCoset.doubleCoset (g₂ : G) P.H P.H + rw [hg] + exact (DoubleCoset.doubleCoset_mul_right_eq_self P ⟨k, hk⟩ _).trans + (doset_mul_left_eq_self P (i₁.out⁻¹ * i₂.out) _) + +private lemma smul_one_eval (T : 𝕋 P Z) (D : HeckeCoset P) (m : HeckeLeftCoset P) + (hm : m ∈ smulOrbit P (HeckeCoset.rep D) (HeckeLeftCoset.rep (HeckeLeftCoset.one P))) : + (T • (1 : HeckeModule P Z)).toFun m = T.toFun D := by + rw [smul_eq_sum, one_eq_HeckeLeftCoset_single] + have hsimp : ∀ D1 (b₁ : Z), + Finsupp.sum (Finsupp.single (HeckeLeftCoset.one P) (1 : Z)) + (fun m' b₂ ↦ ∑ i ∈ smulOrbit P (HeckeCoset.rep D1) (HeckeLeftCoset.rep m'), + Finsupp.single i (b₁ * b₂)) = + ∑ i ∈ smulOrbit P (HeckeCoset.rep D1) (HeckeLeftCoset.rep (HeckeLeftCoset.one P)), + Finsupp.single i b₁ := by + intro D1 b1 + rw [Finsupp.sum_single_index + (by simp [mul_zero, Finsupp.single_zero, Finset.sum_const_zero]), mul_one] + simp_rw [hsimp]; unfold Finsupp.sum + show (∑ x ∈ T.support, + ∑ i ∈ smulOrbit P (HeckeCoset.rep x) (HeckeLeftCoset.rep (HeckeLeftCoset.one P)), + Finsupp.single i (T.toFun x)) m = T.toFun D + simp_rw [Finsupp.finsetSum_apply, Finsupp.single_apply] + rw [Finset.sum_eq_single D] + · rw [Finset.sum_eq_single_of_mem m hm (fun b _ hb ↦ if_neg hb), if_pos rfl] + · intro D' _ hne + exact Finset.sum_eq_zero fun i hi ↦ + if_neg fun heq ↦ absurd (heq ▸ hi) + (Finset.disjoint_left.mp + (smulOrbit_disjoint_of_ne P (HeckeCoset.rep D) (HeckeCoset.rep D') + (HeckeLeftCoset.rep (HeckeLeftCoset.one P)) + (by simp only [HeckeCoset.rep, Quotient.out_eq]; exact hne.symm)) hm) + · intro hns + have h0 : T.toFun D = 0 := Finsupp.notMem_support_iff.mp hns + exact Finset.sum_eq_zero fun x _ ↦ by simp [h0] + +/-- Faithfulness of the module action: if two Hecke ring elements act identically on all +module elements, they are equal. -/ +lemma eq_of_smul_eq_smul_𝕋 (T1 T2 : (𝕋 P Z)) + (h : ∀ (a : HeckeModule P Z), T1 • a = T2 • a) : T1 = T2 := by + refine Finsupp.ext fun D ↦ ?_ + obtain ⟨m, hm⟩ := smulOrbit_nonempty P (HeckeCoset.rep D) + (HeckeLeftCoset.rep (HeckeLeftCoset.one P)) + have h1 := congrFun (congrArg Finsupp.toFun (h 1)) m + rwa [smul_one_eval P Z T1 D m hm, smul_one_eval P Z T2 D m hm] at h1 + +/-- The module action of `𝕋 P ℤ` on `HeckeModule P ℤ` is faithful. -/ +noncomputable instance instFaithfulSMulHeckeModule : + FaithfulSMul (𝕋 P ℤ) (HeckeModule P ℤ) where + eq_of_smul_eq_smul := eq_of_smul_eq_smul_𝕋 P ℤ _ _ + +/-- The scalar multiplication on `𝕋` is defined as reverse multiplication. -/ +lemma smul_def (f g : 𝕋 P ℤ) : f • g = g * f := rfl diff --git a/LeanBridge/ForMathlib/AbstractHeckeRing/Multiplication.lean b/LeanBridge/ForMathlib/AbstractHeckeRing/Multiplication.lean new file mode 100644 index 00000000..ef2223d9 --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing/Multiplication.lean @@ -0,0 +1,688 @@ +/- +Copyright (c) 2024 Chris Birkbeck. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Birkbeck +-/ +import LeanBridge.ForMathlib.AbstractHeckeRing.Basic + +/-! +# Hecke Rings: Multiplication + +Shimura's multiplicity `heckeMultiplicity`, the multiplication finsupp `m`, the `Mul` instance +on `𝕋 P ℤ`, +and the `NonUnitalNonAssocSemiring` instance. Proves that `HeckeCoset.one` is the identity element. +-/ + +open Classical MulOpposite Set DoubleCoset Subgroup + +open scoped Pointwise + +namespace HeckeRing + +variable {G α : Type*} [Group G] (H : Subgroup G) (Δ : Submonoid G) + +variable (P : HeckePair G) (Z : Type*) [CommRing Z] + +/-- Two `HeckeCoset` elements are equal iff their `toSet`s are equal. -/ +lemma HeckeCoset_ext_toSet {D₁ D₂ : HeckeCoset P} + (h : HeckeCoset.toSet D₁ = HeckeCoset.toSet D₂) : D₁ = D₂ := by + revert h + refine Quotient.ind₂ (motive := fun D₁ D₂ ↦ + HeckeCoset.toSet D₁ = HeckeCoset.toSet D₂ → D₁ = D₂) + (fun g₁ g₂ h ↦ ?_) D₁ D₂ + simp only [HeckeCoset.toSet_mk] at h + exact Quotient.sound h + +/-- The stabilizer quotient for the identity double coset is trivial. -/ +lemma decompQuot_T_one_eq_top : + (ConjAct.toConjAct ((HeckeCoset.one P).rep : G) • P.H).subgroupOf P.H = ⊤ := by + have h := HeckeCoset.one_rep_mem_H P + rw [Subgroup.subgroupOf_eq_top] + intro x hx + rw [← @SetLike.mem_coe] + simp only [Subgroup.coe_pointwise_smul] + rw [conjAct_smul_coe_eq, Subgroup.singleton_mul_subgroup h, + Subgroup.subgroup_mul_singleton (by simp [h])] + exact hx + +/-- The decomposition quotient for `HeckeCoset.one` is nonempty. -/ +lemma one_in_decompQuot_T_one : + Nonempty (decompQuot P (HeckeCoset.one P).rep) := + ⟨(1 : P.H)⟩ + +/-- The decomposition quotient for `HeckeCoset.one` is a subsingleton. -/ +lemma subsingleton_decompQuot_T_one : + Subsingleton (decompQuot P (HeckeCoset.one P).rep) := by + unfold decompQuot + rw [decompQuot_T_one_eq_top] + exact QuotientGroup.subsingleton_quotient_top + +private lemma conjAct_mem_of_leftCoset_eq (d : Δ) (h h' : H) + (hyp : {(h : G)} * {(d : G)} * (H : Set G) = + {(h' : G)} * {(d : G)} * (H : Set G)) : + (h')⁻¹ * h ∈ (ConjAct.toConjAct (d : G) • H).subgroupOf H := by + have h_mem_lhs : (h : G) * (d : G) ∈ {(h : G)} * {(d : G)} * (H : Set G) := by + rw [Set.singleton_mul_singleton] + exact ⟨(h : G) * (d : G), Set.mem_singleton _, 1, H.one_mem, by simp⟩ + rw [hyp, Set.singleton_mul_singleton] at h_mem_lhs + obtain ⟨_, rfl, k, hk, hkk⟩ := h_mem_lhs + have hkk' : ↑h' * ↑d * k = ↑h * ↑d := hkk + have key : (h' : G)⁻¹ * (h : G) = (d : G) * k * (d : G)⁻¹ := by + apply mul_right_cancel (b := (d : G)) + rw [mul_assoc, mul_assoc, inv_mul_cancel, mul_one] + apply mul_left_cancel (a := (h' : G)) + rw [mul_inv_cancel_left, ← mul_assoc] + exact hkk'.symm + rw [Subgroup.mem_subgroupOf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, + ConjAct.smul_def] + simp only [map_inv, ConjAct.ofConjAct_toConjAct, Subgroup.coe_mul, + Subgroup.coe_inv] + rw [inv_inv, key] + simp only [mul_assoc, inv_mul_cancel, mul_one, inv_mul_cancel_left] + exact hk + +/-- Distinct elements of `decompQuot` give distinct left cosets. -/ +lemma decompQuot_coset_diff (g : P.Δ) (i j : decompQuot P g) (hij : i ≠ j) : + {((i.out : G) * (g : G))} * (P.H : Set G) ≠ {((j.out : G) * (g : G))} * (P.H : Set G) := by + intro h + simp_rw [← Set.singleton_mul_singleton] at h + have := conjAct_mem_of_leftCoset_eq P.H P.Δ g i.out j.out h + rw [← @QuotientGroup.leftRel_apply, ← @Quotient.eq''] at this + simp only [Quotient.out_eq'] at this + exact hij this.symm + +/-- Two left cosets that are not disjoint must be equal. -/ +lemma leftCoset_eq_of_not_disjoint (f g : G) + (h : ¬ Disjoint (g • (H : Set G)) (f • H)) : + {g} * (H : Set G) = {f} * H := by + simp_rw [← Set.singleton_smul] at * + rw [not_disjoint_iff] at h + obtain ⟨a, ha, ha2⟩ := h + simp only [smul_eq_mul, singleton_mul, image_mul_left, mem_preimage, + SetLike.mem_coe] at ha ha2 + ext Y + simp only [singleton_mul, image_mul_left, mem_preimage, SetLike.mem_coe] + simp_rw [← QuotientGroup.eq] at * + rw [← ha] at ha2 + rw [ha2] + +private lemma mul_mem_delta (a : H) (g : Δ) (h₀ : H.toSubmonoid ≤ Δ) : + (a : G) * (g : G) ∈ Δ := + Submonoid.mul_mem _ (h₀ a.2) g.2 + +/-- Membership in `(ConjAct.toConjAct a • H).subgroupOf H` unfolds to conjugation by `a` +landing back in `H`. -/ +private lemma inv_mul_mul_mem_of_mem_subgroupOf {a : G} + (x : (ConjAct.toConjAct a • H).subgroupOf H) : a⁻¹ * (x.val : G) * a ∈ H := by + have := x.2 + rw [Subgroup.mem_subgroupOf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, + ConjAct.smul_def] at this + simpa [ConjAct.ofConjAct_toConjAct] using this + +/-- The map sending a pair of coset representatives `(σ_i, τ_j)` to the double coset +of their product `H(σ_i τ_j)H`. -/ +noncomputable def mulMap (g₁ g₂ : P.Δ) (i : decompQuot P g₁ × decompQuot P g₂) : + HeckeCoset P := + ⟦⟨i.1.out * g₁ * (i.2.out * g₂), + Submonoid.mul_mem _ (mul_mem_delta P.H P.Δ i.1.out g₁ P.h₀) + (mul_mem_delta P.H P.Δ i.2.out g₂ P.h₀)⟩⟧ + +/-- Shimura's multiplicity (Proposition 3.2): `heckeMultiplicity(g₁, g₂, d)` counts pairs +`(i,j)` such that `σᵢ τⱼ H = ξ H`. -/ +noncomputable def heckeMultiplicity (g₁ g₂ d : P.Δ) : ℤ := + Nat.card {⟨i, j⟩ : decompQuot P g₁ × decompQuot P g₂ | + ({(i.out : G) * (g₁ : G)} : Set G) * {(j.out : G) * (g₂ : G)} * P.H = + {(d : G)} * (P.H : Set G)} + +/-- The finite set of double cosets appearing in the product `D1 * D2`. -/ +noncomputable def mulSupport (g₁ g₂ : P.Δ) : Finset (HeckeCoset P) := + Finset.image (mulMap P g₁ g₂) ⊤ + +/-- If `σ_i τ_j H = ξ H` then the double coset of `σ_i τ_j` equals +that of `ξ`. -/ +lemma doubleCoset_eq_of_rightCoset_eq (g₁ g₂ d : P.Δ) + (p : decompQuot P g₁ × decompQuot P g₂) + (heq : ({(p.1.out : G) * (g₁ : G)} : Set G) * {(p.2.out : G) * (g₂ : G)} * P.H = + {(d : G)} * (P.H : Set G)) : + mulMap P g₁ g₂ p = (⟦d⟧ : HeckeCoset P) := by + unfold mulMap + show (⟦_⟧ : HeckeCoset P) = ⟦_⟧ + rw [HeckeCoset.eq_iff] + have h_mem : (p.1.out : G) * (g₁ : G) * ((p.2.out : G) * (g₂ : G)) ∈ + ({(d : G)} : Set G) * (P.H : Set G) := by + rw [← heq, Set.singleton_mul_singleton] + exact ⟨_, rfl, 1, P.H.one_mem, by simp⟩ + obtain ⟨_, hd_eq, h, hh, hprod⟩ := h_mem + simp only [Set.mem_singleton_iff] at hd_eq + subst hd_eq + dsimp only at hprod ⊢ + rw [← hprod] + exact DoubleCoset.doubleCoset_mul_right_eq_self P ⟨h, hh⟩ _ + +private lemma mulMap_T_one_eq (g₁ : P.Δ) (i : decompQuot P g₁) + (j : decompQuot P (HeckeCoset.one P).rep) : + mulMap P g₁ (HeckeCoset.one P).rep (i, j) = (⟦g₁⟧ : HeckeCoset P) := by + unfold mulMap + show (⟦_⟧ : HeckeCoset P) = ⟦_⟧ + rw [HeckeCoset.eq_iff] + dsimp only + rw [mul_assoc, doset_mul_left_eq_self] + apply DoubleCoset.doubleCoset_mul_right_eq_self P + ⟨j.out * (HeckeCoset.one P).rep, + Subgroup.mul_mem _ (by simp) (HeckeCoset.one_rep_mem_H P)⟩ + +/-- Left multiplication by a singleton set is cancellative. -/ +lemma set_singleton_mul_left_cancel (a : G) {S T : Set G} + (h : ({a} : Set G) * S = ({a} : Set G) * T) : S = T := by + rw [Set.singleton_mul, Set.singleton_mul] at h + exact Set.image_injective.mpr (mul_right_injective a) h + +/-- When the first-component representatives agree, the second-component +representatives must also agree (by left-cancellation on the common prefix). -/ +lemma decompQuot_snd_eq_of_fst_eq (g₁ g₂ d : P.Δ) (i : decompQuot P g₁) + (j₁ j₂ : decompQuot P g₂) + (h₁ : ({(i.out : G) * (g₁ : G)} : Set G) * {(j₁.out : G) * (g₂ : G)} * P.H = + {(d : G)} * (P.H : Set G)) + (h₂ : ({(i.out : G) * (g₁ : G)} : Set G) * {(j₂.out : G) * (g₂ : G)} * P.H = + {(d : G)} * (P.H : Set G)) : + j₁ = j₂ := by + by_contra hne + refine decompQuot_coset_diff P g₂ j₁ j₂ hne + (set_singleton_mul_left_cancel ((i.out : G) * (g₁ : G)) ?_) + have := h₁.trans h₂.symm + rwa [mul_assoc, mul_assoc] at this + +/-- When `j.out * g₂ ∈ H`, the second factor collapses and +first-component injectivity follows from coset disjointness. -/ +lemma decompQuot_fst_eq_of_snd_mem_H (g₁ g₂ d : P.Δ) (i₁ i₂ : decompQuot P g₁) + (j : decompQuot P g₂) (hj : (j.out : G) * (g₂ : G) ∈ P.H) + (h₁ : ({(i₁.out : G) * (g₁ : G)} : Set G) * {(j.out : G) * (g₂ : G)} * P.H = + {(d : G)} * (P.H : Set G)) + (h₂ : ({(i₂.out : G) * (g₁ : G)} : Set G) * {(j.out : G) * (g₂ : G)} * P.H = + {(d : G)} * (P.H : Set G)) : + i₁ = i₂ := by + by_contra hne + refine decompQuot_coset_diff P g₁ i₁ i₂ hne ?_ + simp only [mul_assoc, Subgroup.singleton_mul_subgroup hj] at h₁ h₂ + exact h₁.trans h₂.symm + +private lemma nonempty_mul_one_witness_of_dcRel (g₁ d : P.Δ) (hg₁d : dcRel P g₁ d) : + Nonempty ↑{x : decompQuot P g₁ × decompQuot P (HeckeCoset.one P).rep | + ({(↑x.1.out : G) * (↑g₁ : G)} : Set G) * + {(↑x.2.out : G) * (↑(HeckeCoset.one P).rep : G)} * P.H = + {(↑d : G)} * (P.H : Set G)} := by + have hd_in_g₁ : (↑d : G) ∈ doubleCoset (↑g₁ : G) P.H P.H := + hg₁d ▸ DoubleCoset.mem_doubleCoset_self P.H P.H _ + rw [DoubleCoset.doubleCoset_eq_iUnion_leftCosets] at hd_in_g₁ + simp only [Set.mem_iUnion] at hd_in_g₁ + obtain ⟨k, hk⟩ := hd_in_g₁ + rw [smul_eq_singleton_mul] at hk + obtain ⟨j₀⟩ := one_in_decompQuot_T_one P + refine ⟨⟨(k, j₀), ?_⟩⟩ + simp only [Set.mem_setOf_eq] + have hmem : (j₀.out : G) * ((HeckeCoset.one P).rep : G) ∈ P.H := + Subgroup.mul_mem _ (SetLike.coe_mem j₀.out) (HeckeCoset.one_rep_mem_H P) + rw [mul_assoc, Subgroup.singleton_mul_subgroup hmem] + apply (leftCoset_eq_of_not_disjoint (H := P.H) _ _ _).symm + rw [not_disjoint_iff] + refine ⟨↑d, Set.mem_smul_set.mpr ⟨1, P.H.one_mem, by simp⟩, ?_⟩ + rw [Set.mem_smul_set] + rw [singleton_mul] at hk + simp only [image_mul_left, mem_preimage, SetLike.mem_coe] at hk + exact ⟨(↑k.out * (↑g₁ : G))⁻¹ * ↑d, hk, + show (↑k.out * (↑g₁ : G)) * ((↑k.out * ↑g₁)⁻¹ * ↑d) = ↑d by group⟩ + +/-- Right multiplication by `HeckeCoset.one` has multiplicity `1` on the diagonal +and `0` elsewhere. -/ +lemma heckeMultiplicity_mul_one (g₁ d : P.Δ) : + (⟦g₁⟧ : HeckeCoset P) = ⟦d⟧ ↔ + heckeMultiplicity P g₁ (HeckeCoset.one P).rep d = 1 := by + constructor + · intro h + have hg₁d : dcRel P g₁ d := (HeckeCoset.eq_iff g₁ d).mp h + simp only [heckeMultiplicity] + norm_cast + rw [Nat.card_eq_one_iff_unique] + have : Subsingleton (decompQuot P (HeckeCoset.one P).rep) := + subsingleton_decompQuot_T_one P + refine ⟨⟨?_⟩, nonempty_mul_one_witness_of_dcRel P g₁ d hg₁d⟩ + intro ⟨⟨i₁, j₁⟩, h₁⟩ ⟨⟨i₂, j₂⟩, h₂⟩ + have hj : j₁ = j₂ := Subsingleton.elim j₁ j₂ + subst hj + simp only [Set.mem_setOf_eq] at h₁ h₂ + exact Subtype.ext (Prod.ext + (decompQuot_fst_eq_of_snd_mem_H P g₁ (HeckeCoset.one P).rep d i₁ i₂ j₁ + (Subgroup.mul_mem _ (SetLike.coe_mem j₁.out) (HeckeCoset.one_rep_mem_H P)) h₁ h₂) + rfl) + · intro hm + by_contra hne + have : heckeMultiplicity P g₁ (HeckeCoset.one P).rep d = 0 := by + simp only [heckeMultiplicity, Nat.cast_eq_zero, Nat.card_eq_zero, isEmpty_subtype] + left + intro ⟨i, j⟩ heq + exact hne ((mulMap_T_one_eq P g₁ i j).symm.trans + (doubleCoset_eq_of_rightCoset_eq P g₁ (HeckeCoset.one P).rep d (i, j) heq)) + omega + +private lemma mulMap_one_T_eq (g₁ : P.Δ) (i : decompQuot P (HeckeCoset.one P).rep) + (j : decompQuot P g₁) : + mulMap P (HeckeCoset.one P).rep g₁ (i, j) = (⟦g₁⟧ : HeckeCoset P) := by + unfold mulMap + show (⟦_⟧ : HeckeCoset P) = ⟦_⟧ + rw [HeckeCoset.eq_iff] + dsimp only + rw [mul_assoc] + simp_rw [doset_mul_left_eq_self, + doset_mul_left_eq_self P ⟨(HeckeCoset.one P).rep, HeckeCoset.one_rep_mem_H P⟩, + doset_mul_left_eq_self] + +private lemma nonempty_witness_of_doubleCoset_eq (g₁ g₂ : P.Δ) (c : G) + (i₀ : decompQuot P g₁) (j₀ : decompQuot P g₂) + (hset_eq : DoubleCoset.doubleCoset + ((↑i₀.out : G) * (↑g₁ : G) * ((↑j₀.out : G) * (↑g₂ : G))) + (P.H : Set G) (P.H : Set G) = + DoubleCoset.doubleCoset c P.H P.H) : + Nonempty ↑{x : decompQuot P g₁ × decompQuot P g₂ | + ({(↑x.1.out : G) * (↑g₁ : G)} : Set G) * + {(↑x.2.out : G) * (↑g₂ : G)} * P.H = {c} * (P.H : Set G)} := by + obtain ⟨h₁, hh₁, h₂, hh₂, hprod⟩ := (DoubleCoset.eq P.H P.H _ _).mp + (DoubleCoset.mk_eq_of_doubleCoset_eq hset_eq) + set α := (↑g₁ : G) + set β := (↑g₂ : G) + set K₁ := (ConjAct.toConjAct α • P.H).subgroupOf P.H + set i' : decompQuot P g₁ := ⟦⟨h₁ * ↑i₀.out, P.H.mul_mem hh₁ i₀.out.2⟩⟧ + obtain ⟨κ₁, hκ₁_eq⟩ := QuotientGroup.mk_out_eq_mul K₁ + ⟨h₁ * ↑i₀.out, P.H.mul_mem hh₁ i₀.out.2⟩ + have hκ₁_conj : α⁻¹ * (κ₁.val : G) * α ∈ P.H := + inv_mul_mul_mem_of_mem_subgroupOf (H := P.H) κ₁ + set K₂ := (ConjAct.toConjAct β • P.H).subgroupOf P.H + set j' : decompQuot P g₂ := ⟦⟨(α⁻¹ * (κ₁.val : G) * α)⁻¹ * ↑j₀.out, + P.H.mul_mem (P.H.inv_mem hκ₁_conj) j₀.out.2⟩⟧ + obtain ⟨κ₂, hκ₂_eq⟩ := QuotientGroup.mk_out_eq_mul K₂ + ⟨(α⁻¹ * (κ₁.val : G) * α)⁻¹ * ↑j₀.out, + P.H.mul_mem (P.H.inv_mem hκ₁_conj) j₀.out.2⟩ + have hκ₂_conj : β⁻¹ * (κ₂.val : G) * β ∈ P.H := + inv_mul_mul_mem_of_mem_subgroupOf (H := P.H) κ₂ + have hi'_coe : (↑i'.out : G) = h₁ * ↑i₀.out * (κ₁.val : G) := by + have := congr_arg (Subtype.val : P.H → G) hκ₁_eq + simpa [Subgroup.coe_mul] using this + have hj'_coe : (↑j'.out : G) = + (α⁻¹ * (κ₁.val : G) * α)⁻¹ * ↑j₀.out * (κ₂.val : G) := by + have h := hκ₂_eq + apply_fun (↑· : ↥P.H → G) at h + simp only [Subgroup.coe_mul] at h + exact h + refine ⟨⟨(i', j'), ?_⟩⟩ + simp only [Set.mem_setOf_eq] + have hprod_main : (↑i'.out : G) * α * ((↑j'.out : G) * β) = + c * (h₂⁻¹ * (β⁻¹ * (κ₂.val : G) * β)) := by + rw [hi'_coe, hj'_coe] + have hprod' : c = h₁ * (↑i₀.out * α * (↑j₀.out * β)) * h₂ := hprod + rw [hprod'] + group + rw [Set.singleton_mul_singleton, hprod_main, ← Set.singleton_mul_singleton, mul_assoc, + Subgroup.singleton_mul_subgroup (P.H.mul_mem (P.H.inv_mem hh₂) hκ₂_conj)] + +/-- The multiplicity `heckeMultiplicity` is nonzero for double cosets in the +multiplication support. -/ +lemma heckeMultiplicity_pos_of_mem_mulSupport (g₁ g₂ : P.Δ) (d : HeckeCoset P) + (hd : d ∈ mulSupport P g₁ g₂) : + heckeMultiplicity P g₁ g₂ (HeckeCoset.rep d) ≠ 0 := by + rw [heckeMultiplicity] + simp only [ne_eq, Nat.cast_eq_zero] + rw [Nat.card_eq_zero, not_or, not_isEmpty_iff] + refine ⟨?_, not_infinite_iff_finite.mpr inferInstance⟩ + rw [mulSupport] at hd + simp only [Finset.top_eq_univ, Finset.mem_image, Finset.mem_univ, true_and, + Prod.exists] at hd + obtain ⟨i₀, j₀, hmap⟩ := hd + exact nonempty_witness_of_doubleCoset_eq P g₁ g₂ (HeckeCoset.rep d) i₀ j₀ + ((HeckeCoset.eq_iff _ _).mp (hmap.trans (Quotient.out_eq d).symm)) + +/-- The multiplicity `heckeMultiplicity` is zero for double cosets outside the +multiplication support. -/ +lemma heckeMultiplicity_eq_zero_of_nmem_mulSupport (g₁ g₂ : P.Δ) (d : HeckeCoset P) + (hd : d ∉ mulSupport P g₁ g₂) : + heckeMultiplicity P g₁ g₂ (HeckeCoset.rep d) = 0 := by + simp only [heckeMultiplicity, Nat.cast_eq_zero, Nat.card_eq_zero, isEmpty_subtype] + left + rintro ⟨i, j⟩ hij + refine hd ?_ + rw [mulSupport] + simp only [Finset.top_eq_univ, Finset.mem_image, Finset.mem_univ, true_and, Prod.exists] + exact ⟨i, j, (doubleCoset_eq_of_rightCoset_eq P g₁ g₂ (HeckeCoset.rep d) (i, j) hij).trans + (Quotient.out_eq d)⟩ + +/-- A multiplicity that is both at most one and positive must equal one. -/ +lemma heckeMultiplicity_eq_one_of_le_one_and_pos (g₁ g₂ d : P.Δ) + (h_le : heckeMultiplicity P g₁ g₂ d ≤ 1) + (h_pos : 0 < heckeMultiplicity P g₁ g₂ d) : + heckeMultiplicity P g₁ g₂ d = 1 := by omega + +/-- The multiplicity `heckeMultiplicity` is positive for double cosets in the +multiplication support. -/ +lemma heckeMultiplicity_pos_of_mem (g₁ g₂ : P.Δ) (d : HeckeCoset P) + (hd : d ∈ mulSupport P g₁ g₂) : + 0 < heckeMultiplicity P g₁ g₂ (HeckeCoset.rep d) := by + have h_ne := heckeMultiplicity_pos_of_mem_mulSupport P g₁ g₂ d hd + have : (0 : ℤ) ≤ heckeMultiplicity P g₁ g₂ (HeckeCoset.rep d) := by + simp only [heckeMultiplicity] + exact Nat.cast_nonneg _ + omega + +/-- If `h₁ * g₁ * (h₂ * g₂) ∈ HdH` (with `h₁, h₂ ∈ H`), +then `⟦d⟧ ∈ mulSupport g₁ g₂`. +Avoids manual construction of decomposition quotient elements. -/ +lemma mem_mulSupport_of_product_mem (g₁ g₂ d : P.Δ) (h₁ h₂ : P.H) + (hmem : (h₁ : G) * g₁ * ((h₂ : G) * g₂) ∈ + DoubleCoset.doubleCoset (d : G) P.H P.H) : + (⟦d⟧ : HeckeCoset P) ∈ mulSupport P g₁ g₂ := by + have key : mulMap P g₁ g₂ (⟦⟨h₁, h₁.2⟩⟧, ⟦⟨h₂, h₂.2⟩⟧) = + (⟦d⟧ : HeckeCoset P) := by + unfold mulMap + show (⟦_⟧ : HeckeCoset P) = ⟦_⟧ + rw [HeckeCoset.eq_iff] + dsimp only + obtain ⟨n₁, hn₁⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (g₁ : G) • P.H).subgroupOf P.H) ⟨(h₁ : G), h₁.2⟩ + obtain ⟨n₂, hn₂⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (g₂ : G) • P.H).subgroupOf P.H) ⟨(h₂ : G), h₂.2⟩ + have hi : ((⟦⟨(h₁ : G), h₁.2⟩⟧ : decompQuot P g₁).out : G) = h₁ * n₁ := by + have := congr_arg (Subtype.val : P.H → G) hn₁ + simpa [Subgroup.coe_mul] + have hj : ((⟦⟨(h₂ : G), h₂.2⟩⟧ : decompQuot P g₂).out : G) = h₂ * n₂ := by + have := congr_arg (Subtype.val : P.H → G) hn₂ + simpa [Subgroup.coe_mul] + have hn₂c : (g₂ : G)⁻¹ * ↑n₂ * g₂ ∈ P.H := + inv_mul_mul_mem_of_mem_subgroupOf (H := P.H) n₂ + rw [hi, hj] + apply HeckeCoset.doubleCoset_eq_of_mem + rw [DoubleCoset.mem_doubleCoset] at hmem + obtain ⟨a, ha, b, hb, hab⟩ := hmem + rw [DoubleCoset.mem_doubleCoset] + refine ⟨(h₁ : G) * ↑↑n₁ * (h₁ : G)⁻¹ * a, + P.H.mul_mem (P.H.mul_mem (P.H.mul_mem h₁.2 (SetLike.coe_mem n₁.val)) + (P.H.inv_mem h₁.2)) ha, + b * ((g₂ : G)⁻¹ * ↑↑n₂ * g₂), P.H.mul_mem hb hn₂c, ?_⟩ + have key : (↑h₁ * ↑↑n₁ * (↑h₁ : G)⁻¹ * a) * ↑d * + (b * ((↑g₂ : G)⁻¹ * ↑↑n₂ * ↑g₂)) = + (↑h₁ * ↑↑n₁) * (↑g₁ : G) * ((↑h₂ * ↑↑n₂) * ↑g₂) := + calc (↑h₁ * ↑↑n₁ * (↑h₁ : G)⁻¹ * a) * ↑d + * (b * ((↑g₂ : G)⁻¹ * ↑↑n₂ * ↑g₂)) + = ↑h₁ * ↑↑n₁ * (↑h₁)⁻¹ * (a * ↑d * b) * + ((↑g₂)⁻¹ * ↑↑n₂ * ↑g₂) := by group + _ = ↑h₁ * ↑↑n₁ * (↑h₁)⁻¹ * (↑h₁ * ↑g₁ * (↑h₂ * ↑g₂)) * + ((↑g₂)⁻¹ * ↑↑n₂ * ↑g₂) := by rw [hab] + _ = (↑h₁ * ↑↑n₁) * ↑g₁ * ((↑h₂ * ↑↑n₂) * ↑g₂) := by group + exact key.symm + unfold mulSupport + exact key ▸ Finset.mem_image_of_mem (mulMap P g₁ g₂) (Finset.mem_univ _) + +private lemma nonempty_one_mul_witness_of_dcRel (g₁ d : P.Δ) (hg₁d : dcRel P g₁ d) : + Nonempty ↑{x : decompQuot P (HeckeCoset.one P).rep × decompQuot P g₁ | + ({(↑x.1.out : G) * (↑(HeckeCoset.one P).rep : G)} : Set G) * + {(↑x.2.out : G) * (↑g₁ : G)} * P.H = {(↑d : G)} * (P.H : Set G)} := by + have hd_in : (↑d : G) ∈ doubleCoset (↑g₁ : G) P.H P.H := + hg₁d ▸ DoubleCoset.mem_doubleCoset_self P.H P.H _ + rw [DoubleCoset.doubleCoset_eq_iUnion_leftCosets] at hd_in + simp only [Set.mem_iUnion] at hd_in + obtain ⟨j', hj'⟩ := hd_in + rw [smul_eq_singleton_mul, singleton_mul] at hj' + simp only [image_mul_left, mem_preimage, SetLike.mem_coe] at hj' + obtain ⟨i₀⟩ := one_in_decompQuot_T_one P + have h₀_mem : (↑i₀.out : G) * ((HeckeCoset.one P).rep : G) ∈ P.H := + Subgroup.mul_mem _ (SetLike.coe_mem i₀.out) (HeckeCoset.one_rep_mem_H P) + set h₀ := ↑i₀.out * ((HeckeCoset.one P).rep : G) with hh₀_def + set j₀ : decompQuot P g₁ := + ⟦⟨h₀⁻¹ * ↑j'.out, P.H.mul_mem (P.H.inv_mem h₀_mem) j'.out.2⟩⟧ + obtain ⟨n, hn_eq⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (↑g₁ : G) • P.H).subgroupOf P.H) + ⟨h₀⁻¹ * ↑j'.out, P.H.mul_mem (P.H.inv_mem h₀_mem) j'.out.2⟩ + have hn_coe : (j₀.out : G) = h₀⁻¹ * ↑j'.out * (n : G) := by + have := congr_arg (Subtype.val : ↥P.H → G) hn_eq + simpa [Subgroup.coe_mul] using this + have hn_conj : (↑g₁ : G)⁻¹ * (n : G) * ↑g₁ ∈ P.H := + inv_mul_mul_mem_of_mem_subgroupOf (H := P.H) n + refine ⟨⟨(i₀, j₀), ?_⟩⟩ + simp only [Set.mem_setOf_eq, Set.singleton_mul_singleton] + apply (leftCoset_eq_of_not_disjoint (H := P.H) _ _ _).symm + rw [not_disjoint_iff] + refine ⟨↑d, Set.mem_smul_set.mpr ⟨1, P.H.one_mem, by simp⟩, ?_⟩ + rw [Set.mem_smul_set] + refine ⟨(h₀ * ↑j₀.out * (↑g₁ : G))⁻¹ * ↑d, ?_, by + show (↑i₀.out * (HeckeCoset.one P).rep * (↑j₀.out * (↑g₁ : G))) * + ((h₀ * ↑j₀.out * ↑g₁)⁻¹ * ↑d) = ↑d + simp only [hh₀_def] + group⟩ + show (h₀ * ↑j₀.out * (↑g₁ : G))⁻¹ * ↑d ∈ P.H + have key : (h₀ * ↑j₀.out * (↑g₁ : G))⁻¹ * ↑d = + ((↑g₁ : G)⁻¹ * (↑n : G)⁻¹ * ↑g₁) * + ((↑j'.out * (↑g₁ : G))⁻¹ * ↑d) := by + rw [hn_coe] + group + rw [key] + exact P.H.mul_mem (by convert P.H.inv_mem hn_conj using 1; group) hj' + +/-- Left multiplication by `HeckeCoset.one` has multiplicity `1` on the diagonal +and `0` elsewhere. -/ +lemma heckeMultiplicity_one_mul (g₁ d : P.Δ) : + (⟦g₁⟧ : HeckeCoset P) = ⟦d⟧ ↔ + heckeMultiplicity P (HeckeCoset.one P).rep g₁ d = 1 := by + constructor + · intro h + have hg₁d : dcRel P g₁ d := (HeckeCoset.eq_iff g₁ d).mp h + simp only [heckeMultiplicity] + norm_cast + rw [Nat.card_eq_one_iff_unique] + have : Subsingleton (decompQuot P (HeckeCoset.one P).rep) := + subsingleton_decompQuot_T_one P + refine ⟨⟨?_⟩, nonempty_one_mul_witness_of_dcRel P g₁ d hg₁d⟩ + intro ⟨⟨i₁, j₁⟩, h₁⟩ ⟨⟨i₂, j₂⟩, h₂⟩ + have hi : i₁ = i₂ := Subsingleton.elim i₁ i₂ + subst hi + simp only [Set.mem_setOf_eq] at h₁ h₂ + exact Subtype.ext (Prod.ext rfl + (decompQuot_snd_eq_of_fst_eq P (HeckeCoset.one P).rep g₁ d i₁ j₁ j₂ h₁ h₂)) + · intro hm + by_contra hne + have : heckeMultiplicity P (HeckeCoset.one P).rep g₁ d = 0 := by + simp only [heckeMultiplicity, Nat.cast_eq_zero, Nat.card_eq_zero, isEmpty_subtype] + left + intro ⟨i, j⟩ heq + exact hne ((mulMap_one_T_eq P g₁ i j).symm.trans + (doubleCoset_eq_of_rightCoset_eq P (HeckeCoset.one P).rep g₁ d (i, j) heq)) + omega + +/-- Scalar multiplication on finitely supported functions by ring elements. -/ +noncomputable instance instSMulZeroClass : SMulZeroClass Z (α →₀ Z) where + smul a v := v.mapRange (a • ·) (smul_zero _) + smul_zero a := by ext; exact smul_zero _ + +/-- The multiplication finsupp: `m(g₁, g₂)` is the formal sum +`Σ_d heckeMultiplicity(g₁, g₂, d) · d` +encoding the product of two double cosets. -/ +noncomputable def m (g₁ g₂ : P.Δ) : (HeckeCoset P) →₀ ℤ := + ⟨mulSupport P g₁ g₂, + fun d ↦ heckeMultiplicity P g₁ g₂ (HeckeCoset.rep d), + fun a ↦ + ⟨heckeMultiplicity_pos_of_mem_mulSupport P g₁ g₂ a, + fun hm ↦ by + by_contra hemp + exact hm (heckeMultiplicity_eq_zero_of_nmem_mulSupport P g₁ g₂ a hemp)⟩⟩ + +/-- The multiplication on the Hecke ring, defined via the multiplicity function `m`. -/ +noncomputable instance (P : HeckePair G) : Mul (𝕋 P ℤ) where + mul f g := Finsupp.sum f fun D1 b₁ ↦ + g.sum fun D2 b₂ ↦ + b₁ • b₂ • m P (HeckeCoset.rep D1) (HeckeCoset.rep D2) + +/-- Multiplication in the Hecke ring unfolds as a double Finsupp sum over multiplicities. -/ +lemma mul_def (f g : 𝕋 P ℤ) : f * g = Finsupp.sum f + (fun D1 b₁ ↦ g.sum fun D2 b₂ ↦ + b₁ • b₂ • m P (HeckeCoset.rep D1) (HeckeCoset.rep D2)) := rfl + +/-- A basis element of the Hecke ring: `T_single D b` is the formal sum `b · [D]`. -/ +noncomputable abbrev T_single (a : HeckeCoset P) (b : Z) : 𝕋 P Z := + Finsupp.single a b + +/-- A basis element of the Hecke module: `HeckeLeftCoset_single m b` is the formal sum +`b · [m]`. -/ +noncomputable abbrev HeckeLeftCoset_single (a : HeckeLeftCoset P) (b : Z) : + HeckeModule P Z := + Finsupp.single a b + +/-- Shimura's notation: `T⦃D⦄` is the basis element `[HgH]` in the Hecke ring, + corresponding to the double coset `D` with coefficient 1. -/ +scoped notation:max "T⦃" D "⦄" => T_single _ ℤ D (1 : ℤ) + +/-- Shimura's notation: `T⦃D, a⦄` is the element `a · [HgH]` in the Hecke ring. -/ +scoped notation:max "T⦃" D ", " a "⦄" => T_single _ ℤ D a + +/-- Multiplication of two basis elements in the Hecke ring. -/ +lemma mul_singleton_𝕋 (D1 D2 : HeckeCoset P) (a b : ℤ) : + T_single P ℤ D1 a * T_single P ℤ D2 b = + a • b • m P (HeckeCoset.rep D1) (HeckeCoset.rep D2) := by + simp_rw [T_single, mul_def] + rw [Finsupp.sum_single_index, Finsupp.sum_single_index, m] + · simp only [zero_smul, smul_zero] + · ext a + simp only [m, zero_smul, Finsupp.sum_fun_zero, Finsupp.coe_zero, Pi.zero_apply] + +open Finsupp + +/-- If all pairs under `mulMap` land on a single double coset `D_out`, then +`heckeMultiplicity` vanishes on every other coset. -/ +lemma heckeMultiplicity_eq_zero_of_mulMap_unique (g₁ g₂ : P.Δ) (D_out A : HeckeCoset P) + (hA : A ≠ D_out) + (h : ∀ p : decompQuot P g₁ × decompQuot P g₂, mulMap P g₁ g₂ p = D_out) : + heckeMultiplicity P g₁ g₂ (HeckeCoset.rep A) = 0 := + heckeMultiplicity_eq_zero_of_nmem_mulSupport P g₁ g₂ A (by + rw [mulSupport] + simp only [Finset.top_eq_univ, Finset.mem_image, Finset.mem_univ, true_and, + Prod.exists, not_exists] + intro i j heq + exact hA (heq ▸ h (i, j))) + +/-- When `heckeMultiplicity` equals one on a single output coset and vanishes elsewhere, +the multiplication finsupp is a singleton. -/ +lemma m_eq_single (g₁ g₂ : P.Δ) (D_out : HeckeCoset P) + (h_one : heckeMultiplicity P g₁ g₂ (HeckeCoset.rep D_out) = 1) + (h_zero : ∀ A, A ≠ D_out → heckeMultiplicity P g₁ g₂ (HeckeCoset.rep A) = 0) : + m P g₁ g₂ = Finsupp.single D_out 1 := by + ext A + simp only [m, Finsupp.coe_mk, Finsupp.single_apply] + split_ifs with h1 + · exact h1 ▸ h_one + · exact h_zero A (ne_comm.mp h1) + +/-- The off-diagonal multiplicity for right multiplication by `HeckeCoset.one` is zero. -/ +lemma heckeMultiplicity_mul_one_eq_zero (g₁ : P.Δ) (A : HeckeCoset P) + (h : A ≠ (⟦g₁⟧ : HeckeCoset P)) : + heckeMultiplicity P g₁ (HeckeCoset.one P).rep (HeckeCoset.rep A) = 0 := by + simp only [heckeMultiplicity, Nat.cast_eq_zero, Nat.card_eq_zero, isEmpty_subtype] + left + intro ⟨i, j⟩ heq + refine h ?_ + rw [show A = ⟦HeckeCoset.rep A⟧ from (Quotient.out_eq A).symm] + exact ((mulMap_T_one_eq P g₁ i j).symm.trans + (doubleCoset_eq_of_rightCoset_eq P g₁ (HeckeCoset.one P).rep (HeckeCoset.rep A) + (i, j) heq)).symm + +/-- Right multiplication by `HeckeCoset.one` acts as the identity: +`m(g₁, one.rep) = δ_{⟦g₁⟧}`. -/ +lemma m_mul_one_eq_single (g₁ : P.Δ) : + m P g₁ (HeckeCoset.one P).rep = Finsupp.single (⟦g₁⟧ : HeckeCoset P) 1 := + m_eq_single P g₁ (HeckeCoset.one P).rep (⟦g₁⟧ : HeckeCoset P) + ((heckeMultiplicity_mul_one P g₁ (HeckeCoset.rep (⟦g₁⟧ : HeckeCoset P))).mp + (Quotient.out_eq (⟦g₁⟧ : HeckeCoset P)).symm) + (heckeMultiplicity_mul_one_eq_zero P g₁) + +/-- `T_single D b * T_single (HeckeCoset.one P) 1 = T_single D b`. -/ +lemma singleton_one_mul_𝕋 (D2 : HeckeCoset P) (b : ℤ) : + T_single P ℤ D2 b * T_single P ℤ (HeckeCoset.one P) 1 = + T_single P ℤ D2 b := by + revert D2 + exact HeckeCoset.ind fun g ↦ by + rw [mul_singleton_𝕋, m_mul_one_eq_single] + simp only [T_single] + rw [show (⟦HeckeCoset.rep ⟦g⟧⟧ : HeckeCoset P) = ⟦g⟧ from Quotient.out_eq _] + show Finsupp.mapRange (b • ·) _ (Finsupp.mapRange ((1 : ℤ) • ·) _ + (Finsupp.single ⟦g⟧ (1 : ℤ))) = _ + rw [Finsupp.mapRange_single (hf := smul_zero (1 : ℤ))] + rw [Finsupp.mapRange_single (hf := smul_zero b)] + show Finsupp.single ⟦g⟧ (b • (1 : ℤ) • (1 : ℤ)) = Finsupp.single ⟦g⟧ b + rw [one_smul, smul_eq_mul, mul_one] + +/-- The off-diagonal multiplicity for left multiplication by `HeckeCoset.one` is zero. -/ +lemma heckeMultiplicity_one_mul_eq_zero (g₁ : P.Δ) (A : HeckeCoset P) + (h : A ≠ (⟦g₁⟧ : HeckeCoset P)) : + heckeMultiplicity P (HeckeCoset.one P).rep g₁ (HeckeCoset.rep A) = 0 := by + simp only [heckeMultiplicity, Nat.cast_eq_zero, Nat.card_eq_zero, isEmpty_subtype] + left + intro ⟨i, j⟩ heq + refine h ?_ + rw [show A = ⟦HeckeCoset.rep A⟧ from (Quotient.out_eq A).symm] + exact ((mulMap_one_T_eq P g₁ i j).symm.trans + (doubleCoset_eq_of_rightCoset_eq P (HeckeCoset.one P).rep g₁ (HeckeCoset.rep A) + (i, j) heq)).symm + +/-- Left multiplication by `HeckeCoset.one` acts as the identity: +`m(one.rep, g₁) = δ_{⟦g₁⟧}`. -/ +lemma m_one_mul_eq_single (g₁ : P.Δ) : + m P (HeckeCoset.one P).rep g₁ = Finsupp.single (⟦g₁⟧ : HeckeCoset P) 1 := + m_eq_single P (HeckeCoset.one P).rep g₁ (⟦g₁⟧ : HeckeCoset P) + ((heckeMultiplicity_one_mul P g₁ (HeckeCoset.rep (⟦g₁⟧ : HeckeCoset P))).mp + (Quotient.out_eq (⟦g₁⟧ : HeckeCoset P)).symm) + (heckeMultiplicity_one_mul_eq_zero P g₁) + +/-- `T_single (HeckeCoset.one P) 1 * T_single D b = T_single D b`. -/ +lemma one_mul_singleton_𝕋 (D2 : HeckeCoset P) (b : ℤ) : + T_single P ℤ (HeckeCoset.one P) 1 * T_single P ℤ D2 b = + T_single P ℤ D2 b := by + revert D2 + exact HeckeCoset.ind fun g ↦ by + rw [mul_singleton_𝕋, m_one_mul_eq_single] + simp only [T_single] + rw [show (⟦HeckeCoset.rep ⟦g⟧⟧ : HeckeCoset P) = ⟦g⟧ from Quotient.out_eq _] + show Finsupp.mapRange ((1 : ℤ) • ·) _ (Finsupp.mapRange (b • ·) _ + (Finsupp.single ⟦g⟧ (1 : ℤ))) = _ + rw [Finsupp.mapRange_single (hf := smul_zero b)] + rw [Finsupp.mapRange_single (hf := smul_zero (1 : ℤ))] + show Finsupp.single ⟦g⟧ ((1 : ℤ) • b • (1 : ℤ)) = Finsupp.single ⟦g⟧ b + rw [one_smul, smul_eq_mul, mul_one] + +/-- The Hecke ring is a non-unital non-associative semiring (distributivity and zero laws). -/ +noncomputable instance instNonUnitalNonAssocSemiring : + NonUnitalNonAssocSemiring (𝕋 P ℤ) := + { (instAddCommGroup𝕋 P ℤ) with + left_distrib := fun f g h ↦ by + simp only [mul_def] + refine Eq.trans (congr_arg (Finsupp.sum f) + (funext₂ fun a₁ b₁ ↦ Finsupp.sum_add_index ?_ ?_)) ?_ + · intros; simp + · intro D1 _ a b + simp_rw [← smul_assoc, smul_eq_mul] + ring_nf + rw [@add_smul] + · exact Finsupp.sum_add + right_distrib := fun f g h ↦ by + simp only [mul_def] + refine Eq.trans (Finsupp.sum_add_index ?_ ?_) ?_ + · intros + simp only [zero_smul, Finsupp.sum_fun_zero] + rfl + · intro D1 _ a b + refine Finsupp.ext fun t ↦ ?_ + change (Finsupp.sum h fun D2 b₂ ↦ (a + b) • b₂ • m P D1.rep D2.rep) t = + ((Finsupp.sum h fun D2 b₂ ↦ a • b₂ • m P D1.rep D2.rep) + + Finsupp.sum h fun D2 b₂ ↦ b • b₂ • m P D1.rep D2.rep) t + rw [Finsupp.add_apply] + simp only [Finsupp.sum, Finset.sum_apply', Finsupp.coe_smul, Pi.smul_apply, + smul_eq_mul] + simp_rw [add_mul] + rw [Finset.sum_add_distrib] + · rfl + zero_mul := fun _ ↦ by simp only [mul_def]; exact Finsupp.sum_zero_index + mul_zero := fun f ↦ by + simp only [mul_def] + exact Eq.trans (congr_arg (sum f) (funext₂ fun _ _ ↦ sum_zero_index)) (sum_fun_zero f) } diff --git a/LeanBridge/ForMathlib/AbstractHeckeRing/Ring.lean b/LeanBridge/ForMathlib/AbstractHeckeRing/Ring.lean new file mode 100644 index 00000000..10cc771c --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing/Ring.lean @@ -0,0 +1,189 @@ +/- +Copyright (c) 2024 Chris Birkbeck. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Chris Birkbeck +-/ +import LeanBridge.ForMathlib.AbstractHeckeRing.Associativity + +/-! +# Hecke Rings: Ring Instance and API + +The `Ring (𝕋 P ℤ)` instance and user-facing API lemmas for working with Hecke rings. +-/ + +open Classical MulOpposite Set DoubleCoset Subgroup + +open scoped Pointwise + +namespace HeckeRing + +variable {G : Type*} [Group G] + +variable (P : HeckePair G) (Z : Type*) [CommRing Z] + +open Finsupp + +/-- Associativity of multiplication in the Hecke ring, deduced from `IsScalarTower` +and faithfulness of the module action. -/ +lemma mul_assoc_𝕋 (f g h : 𝕋 P ℤ) : (f * g) * h = f * (g * h) := by + refine (instFaithfulSMulHeckeModule P).eq_of_smul_eq_smul (M := 𝕋 P ℤ) fun a ↦ ?_ + have e1 := (instIsScalarTower P).smul_assoc g f a + have e2 := (instIsScalarTower P).smul_assoc h g (f • a) + have e4 := (instIsScalarTower P).smul_assoc h (f * g) a + simp only [smul_def] at e1 e2 e4 + rw [e1, ← e2, ← (instIsScalarTower P).smul_assoc (g * h) f a, smul_def] at e4 + exact e4 + +/-- The Hecke ring is a non-unital semiring (associativity + distributivity). -/ +noncomputable instance instNonUnitalSemiring : NonUnitalSemiring (𝕋 P ℤ) := + { instNonUnitalNonAssocSemiring P with mul_assoc := mul_assoc_𝕋 P } + +/-- The multiplicative identity of the Hecke ring is `T_single (HeckeCoset.one P) 1`. -/ +noncomputable instance instOne𝕋 : One (𝕋 P Z) := + ⟨T_single P Z (HeckeCoset.one P) 1⟩ + +/-- The one element of the Hecke ring unfolds to `T_single (HeckeCoset.one P) 1`. -/ +theorem one_def : (1 : 𝕋 P Z) = T_single P Z (HeckeCoset.one P) 1 := rfl + +/-- The Hecke ring is a non-associative semiring (one is a two-sided identity). -/ +noncomputable instance instNonAssocSemiring : NonAssocSemiring (𝕋 P ℤ) := + { instNonUnitalNonAssocSemiring P with + natCast := fun n ↦ T_single P ℤ (HeckeCoset.one P) n + natCast_zero := by simp only [Nat.cast_zero, single_zero]; rfl + natCast_succ := fun _ ↦ by + simp only [Nat.cast_add, Nat.cast_one, single_add]; rfl + one_mul := fun f ↦ by + simp only [one_def, mul_def, T_single] + simp + nth_rw 2 [← Finsupp.sum_single f] + congr + ext D z v + have := one_mul_singleton_𝕋 P D z + simp_rw [T_single] at * + rw [← this, mul_singleton_𝕋, one_smul] + mul_one := fun f ↦ by + simp only [one_def, mul_def, zero_smul, smul_zero, sum_single_index, one_smul] + nth_rw 2 [← Finsupp.sum_single f] + congr + ext D z v + have := singleton_one_mul_𝕋 P D z + simp_rw [T_single] at this + rw [← this, mul_singleton_𝕋, one_smul] } + +/-- The Hecke ring is a semiring. -/ +noncomputable instance instSemiring : Semiring (𝕋 P ℤ) := + { HeckeRing.instNonUnitalSemiring P, + HeckeRing.instNonAssocSemiring P with } + +/-- The Hecke ring is a non-associative ring (semiring + additive inverses). -/ +noncomputable instance instNonAssocRing : NonAssocRing (𝕋 P ℤ) := + { HeckeRing.instAddCommGroup𝕋 P ℤ, + HeckeRing.instNonAssocSemiring P with + intCast := fun n ↦ T_single P ℤ (HeckeCoset.one P) n + intCast_ofNat := fun _ ↦ rfl + intCast_negSucc := fun _ ↦ by + simp only [T_single, Int.negSucc_eq, Finsupp.single_neg]; congr 1 } + +/-- The Hecke ring `𝕋 P ℤ` is a ring. -/ +noncomputable instance instRing : Ring (𝕋 P ℤ) := + { HeckeRing.instNonAssocRing P, HeckeRing.instSemiring P with } + +section API + +/-- A basis element with coefficient zero is zero. -/ +@[simp] lemma T_single_zero (D : HeckeCoset P) : + T_single P ℤ D 0 = 0 := Finsupp.single_zero _ + +/-- Addition of two basis elements with the same double coset. -/ +@[simp] lemma T_single_add (D : HeckeCoset P) (a b : ℤ) : + T_single P ℤ D a + T_single P ℤ D b = T_single P ℤ D (a + b) := + (Finsupp.single_add D a b).symm + +/-- Negation of a basis element. -/ +@[simp] lemma T_single_neg (D : HeckeCoset P) (a : ℤ) : + -T_single P ℤ D a = T_single P ℤ D (-a) := (Finsupp.single_neg D a).symm + +/-- Scalar multiplication on a basis element. -/ +lemma T_single_smul (D : HeckeCoset P) (n a : ℤ) : + n • T_single P ℤ D a = T_single P ℤ D (n * a) := Finsupp.smul_single' n D a + +/-- The integer cast into the Hecke ring lands on the identity double coset. -/ +@[simp] lemma intCast_eq (n : ℤ) : (n : 𝕋 P ℤ) = T_single P ℤ (HeckeCoset.one P) n := + rfl + +/-- The product of two basis elements equals the scaled multiplication finsupp. -/ +lemma T_single_mul_T_single (D₁ D₂ : HeckeCoset P) (a b : ℤ) : + T_single P ℤ D₁ a * T_single P ℤ D₂ b = + a • b • m P (HeckeCoset.rep D₁) (HeckeCoset.rep D₂) := + mul_singleton_𝕋 P D₁ D₂ a b + +/-- The product of two unit-coefficient basis elements is the multiplication finsupp. -/ +@[simp] lemma T_single_one_mul_T_single_one (D₁ D₂ : HeckeCoset P) : + T_single P ℤ D₁ 1 * T_single P ℤ D₂ 1 = + m P (HeckeCoset.rep D₁) (HeckeCoset.rep D₂) := by + simp [T_single_mul_T_single] + +/-- Right multiplication by 1 is the identity. -/ +@[simp] lemma T_single_mul_one (D : HeckeCoset P) (a : ℤ) : + T_single P ℤ D a * 1 = T_single P ℤ D a := singleton_one_mul_𝕋 P D a + +/-- Left multiplication by 1 is the identity. -/ +@[simp] lemma one_mul_T_single (D : HeckeCoset P) (a : ℤ) : + 1 * T_single P ℤ D a = T_single P ℤ D a := one_mul_singleton_𝕋 P D a + +/-- When `heckeMultiplicity` is one on a single output and zero elsewhere, multiplication of +unit-coefficient basis elements produces a single basis element. -/ +lemma T_single_one_mul_eq_single (D₁ D₂ D_out : HeckeCoset P) + (h_one : heckeMultiplicity P (HeckeCoset.rep D₁) (HeckeCoset.rep D₂) + (HeckeCoset.rep D_out) = 1) + (h_zero : ∀ A, A ≠ D_out → heckeMultiplicity P (HeckeCoset.rep D₁) + (HeckeCoset.rep D₂) (HeckeCoset.rep A) = 0) : + T_single P ℤ D₁ 1 * T_single P ℤ D₂ 1 = T_single P ℤ D_out 1 := by + rw [T_single_one_mul_T_single_one, + m_eq_single P (HeckeCoset.rep D₁) (HeckeCoset.rep D₂) D_out h_one h_zero] + +/-- Evaluating the multiplication finsupp at a double coset gives `heckeMultiplicity`. -/ +@[simp] lemma m_apply (g₁ g₂ : P.Δ) (D : HeckeCoset P) : + (m P g₁ g₂) D = heckeMultiplicity P g₁ g₂ (HeckeCoset.rep D) := rfl + +/-- Right multiplication by `HeckeCoset.one` is the identity on `m`. -/ +@[simp] lemma m_mul_T_one (D : HeckeCoset P) : + m P (HeckeCoset.rep D) (HeckeCoset.one P).rep = + Finsupp.single (⟦HeckeCoset.rep D⟧ : HeckeCoset P) 1 := + m_mul_one_eq_single P (HeckeCoset.rep D) + +/-- Left multiplication by `HeckeCoset.one` is the identity on `m`. -/ +@[simp] lemma m_T_one_mul (D : HeckeCoset P) : + m P (HeckeCoset.one P).rep (HeckeCoset.rep D) = + Finsupp.single (⟦HeckeCoset.rep D⟧ : HeckeCoset P) 1 := + m_one_mul_eq_single P (HeckeCoset.rep D) + +/-- The support of the multiplication finsupp equals `mulSupport`. -/ +lemma m_support (g₁ g₂ : P.Δ) : + (m P g₁ g₂).support = mulSupport P g₁ g₂ := rfl + +/-- The multiplicity `heckeMultiplicity` is nonneg since it is a natural number cast to `ℤ`. -/ +lemma heckeMultiplicity_nonneg (g₁ g₂ d : P.Δ) : + 0 ≤ heckeMultiplicity P g₁ g₂ d := by + simp [heckeMultiplicity] + +/-- Extensionality for Hecke ring elements. -/ +@[ext] lemma ext_𝕋 {f g : 𝕋 P ℤ} + (h : ∀ D : HeckeCoset P, f.toFun D = g.toFun D) : f = g := Finsupp.ext h + +/-- Linear induction principle: reduce to zero, single basis elements, and sums. -/ +lemma induction_linear_𝕋 {C : 𝕋 P ℤ → Prop} (f : 𝕋 P ℤ) (h_zero : C 0) + (h_single : ∀ (D : HeckeCoset P) (a : ℤ), C (T_single P ℤ D a)) + (h_add : ∀ f g : 𝕋 P ℤ, C f → C g → C (f + g)) : C f := + Finsupp.induction_linear f h_zero h_add h_single + +/-- The action of a basis Hecke element on a basis module element as a sum over orbits. -/ +lemma T_single_smul_HeckeLeftCoset_single (D : HeckeCoset P) (m₀ : HeckeLeftCoset P) (a b : Z) : + T_single P Z D a • HeckeLeftCoset_single P Z m₀ b = + ∑ i ∈ smulOrbit P (HeckeCoset.rep D) (HeckeLeftCoset.rep m₀), + HeckeLeftCoset_single P Z i (a * b) := + single_smul_single P Z D m₀ a b + +end API + +end HeckeRing