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..0c8768b0 --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing.lean @@ -0,0 +1,32 @@ +/- +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 +import LeanBridge.ForMathlib.AbstractHeckeRing.Multiplication +import LeanBridge.ForMathlib.AbstractHeckeRing.Associativity +import LeanBridge.ForMathlib.AbstractHeckeRing.Ring +import LeanBridge.ForMathlib.AbstractHeckeRing.Module +import LeanBridge.ForMathlib.AbstractHeckeRing.Commutativity +import LeanBridge.ForMathlib.AbstractHeckeRing.Degree +import LeanBridge.ForMathlib.AbstractHeckeRing.StabConjugation + +/-! +# Abstract Hecke ring + +The full construction of the abstract Hecke ring, following Shimura, *Introduction to the +Arithmetic Theory of Automorphic Functions*, Ch. 3. For an arithmetic pair `(H, Δ)` +(`H ≤ Δ ≤ commensurator(H)`), this assembles: + +* `HeckeRing.HeckePair`, the double-coset quotient `HeckeRing.HeckeCoset`, and the Hecke ring + type `HeckeRing.𝕋` (`Basic`); +* the convolution product (`Multiplication`, `Associativity`) and the resulting `Ring` + structure (`Ring`); +* the Hecke module over the left cosets (`Module`); +* commutativity from an anti-involution (`Commutativity`), the degree map (`Degree`), and + stabilizer/conjugation lemmas (`StabConjugation`). + +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/Commutativity.lean b/LeanBridge/ForMathlib/AbstractHeckeRing/Commutativity.lean new file mode 100644 index 00000000..cda26cf3 --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing/Commutativity.lean @@ -0,0 +1,478 @@ +/- +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 + +/-! +# Hecke Rings: Commutativity via Anti-Involution + +Shimura Proposition 3.8: if an arithmetic group pair admits an anti-automorphism +`ι : G →* Gᵐᵒᵖ` that preserves H and Δ and fixes every double coset, then the +Hecke ring `𝕋 P ℤ` is commutative. +-/ + +open Classical MulOpposite Set DoubleCoset Subgroup Finsupp + +open scoped Pointwise + +namespace HeckeRing + +variable {G : Type*} [Group G] (P : HeckePair G) + +/-- An anti-involution of a HeckePair: `ι : G →* Gᵐᵒᵖ`, +involutive and preserving both `H` and `Δ`. -/ +@[ext] +structure AntiInvolution where + /-- The underlying homomorphism to the opposite group. -/ + toFun : G →* MulOpposite G + /-- The induced map on `G` is involutive. -/ + involutive : ∀ g, (toFun (toFun g).unop).unop = g + /-- The induced map preserves membership in `H`. -/ + map_H : ∀ g, g ∈ P.H → (toFun g).unop ∈ P.H + /-- The induced map preserves membership in `Δ`. -/ + map_Δ : ∀ g, g ∈ P.Δ → (toFun g).unop ∈ P.Δ + +variable {P} + +namespace AntiInvolution + +variable (ι : AntiInvolution P) + +/-- The underlying function of the anti-involution, mapping `g` to `ι(g)` viewed in `G`. -/ +def bar (g : G) : G := (ι.toFun g).unop + +/-- The anti-involution is an involution: `bar(bar(g)) = g`. -/ +@[simp] lemma bar_bar (g : G) : ι.bar (ι.bar g) = g := ι.involutive g + +/-- The anti-involution reverses multiplication: `bar(ab) = bar(b) * bar(a)`. -/ +lemma bar_mul (a b : G) : ι.bar (a * b) = ι.bar b * ι.bar a := by simp [bar] + +/-- The anti-involution commutes with inversion. -/ +lemma bar_inv (g : G) : ι.bar g⁻¹ = (ι.bar g)⁻¹ := by simp [bar] + +/-- The anti-involution preserves membership in `H`. -/ +lemma bar_mem_H {g : G} (hg : g ∈ P.H) : ι.bar g ∈ P.H := + ι.map_H g hg + +/-- The anti-involution preserves membership in `Δ`. -/ +lemma bar_mem_Δ {g : G} (hg : g ∈ P.Δ) : ι.bar g ∈ P.Δ := + ι.map_Δ g hg + +/-- The anti-involution preserves double coset equality. -/ +lemma bar_doubleCoset_eq (g₁ g₂ : G) + (h : DoubleCoset.doubleCoset g₁ P.H P.H = + DoubleCoset.doubleCoset g₂ P.H P.H) : + DoubleCoset.doubleCoset (ι.bar g₁) P.H P.H = + DoubleCoset.doubleCoset (ι.bar g₂) P.H P.H := by + obtain ⟨h₁, hh₁, h₂, hh₂, hprod⟩ := (DoubleCoset.eq P.H P.H _ _).mp + (DoubleCoset.mk_eq_of_doubleCoset_eq h) + rw [show ι.bar g₂ = ι.bar h₂ * ι.bar g₁ * ι.bar h₁ by + rw [hprod, bar_mul, bar_mul, mul_assoc]] + symm + rw [mul_assoc] + trans DoubleCoset.doubleCoset (ι.bar g₁ * ι.bar h₁) (P.H : Set G) P.H + · exact doset_mul_left_eq_self P ⟨ι.bar h₂, ι.bar_mem_H hh₂⟩ _ + · exact DoubleCoset.doubleCoset_mul_right_eq_self P ⟨ι.bar h₁, ι.bar_mem_H hh₁⟩ _ + +/-- The induced action of the anti-involution on double cosets, defined via `Quotient.lift`. -/ +noncomputable def onHeckeCoset (D : HeckeCoset P) : HeckeCoset P := + Quotient.lift (fun (g : P.Δ) ↦ + (⟦⟨ι.bar (g : G), ι.bar_mem_Δ g.2⟩⟧ : HeckeCoset P)) + (fun _ _ (h : @Setoid.r _ (dcSetoid P) _ _) ↦ by + show (⟦_⟧ : HeckeCoset P) = ⟦_⟧ + rw [HeckeCoset.eq_iff] + exact ι.bar_doubleCoset_eq _ _ h) D + +/-- `onHeckeCoset ⟦g⟧` equals `⟦bar(g)⟧`. -/ +lemma onHeckeCoset_mk (g : P.Δ) : + ι.onHeckeCoset (⟦g⟧ : HeckeCoset P) = + (⟦⟨ι.bar (g : G), ι.bar_mem_Δ g.2⟩⟧ : HeckeCoset P) := rfl + +/-- The set underlying `onHeckeCoset D` is the double coset of the barred representative. -/ +lemma onHeckeCoset_toSet (D : HeckeCoset P) : + HeckeCoset.toSet (ι.onHeckeCoset D) = + DoubleCoset.doubleCoset (ι.bar (HeckeCoset.rep D : G)) P.H P.H := by + conv_lhs => rw [show D = ⟦HeckeCoset.rep D⟧ from (Quotient.out_eq D).symm] + simp [onHeckeCoset_mk] + +private lemma bar_mem_doubleCoset (h_fix : ∀ D : HeckeCoset P, ι.onHeckeCoset D = D) + (D₀ : HeckeCoset P) (x : G) (hx : x ∈ HeckeCoset.toSet D₀) : + ι.bar x ∈ HeckeCoset.toSet D₀ := by + rw [← congr_arg HeckeCoset.toSet (h_fix D₀), onHeckeCoset_toSet] + rw [HeckeCoset.toSet_eq_rep, DoubleCoset.mem_doubleCoset] at hx + obtain ⟨h₁, hh₁, h₂, hh₂, hprod⟩ := hx + rw [hprod, DoubleCoset.mem_doubleCoset] + exact ⟨ι.bar h₂, ι.bar_mem_H hh₂, ι.bar h₁, ι.bar_mem_H hh₁, by + simp [bar_mul, mul_assoc]⟩ + +private lemma bar_rep_mem_doubleCoset (h_fix : ∀ D : HeckeCoset P, ι.onHeckeCoset D = D) + (D : HeckeCoset P) : ∃ h₁ h₂ : P.H, + ι.bar (HeckeCoset.rep D : G) = h₁ * (HeckeCoset.rep D : G) * h₂ := by + have hbar := bar_mem_doubleCoset ι h_fix D _ (HeckeCoset.rep_mem D) + rw [HeckeCoset.toSet_eq_rep, DoubleCoset.mem_doubleCoset] at hbar + obtain ⟨h₁, hh₁, h₂, hh₂, heq⟩ := hbar + exact ⟨⟨h₁, hh₁⟩, ⟨h₂, hh₂⟩, heq⟩ + +private lemma inverse_product_mem_doubleCoset + (g₁ g₂ g_D : G) (D₂ : HeckeCoset P) + (hg₂ : g₂ = (HeckeCoset.rep D₂ : G)) + (rep : P.H) (j_rep : P.H) + (hcond : ({(rep : G) * g₁} : Set G) * {(j_rep : G) * g₂} * P.H = + {g_D} * (P.H : Set G)) : + g₁⁻¹ * (rep : G)⁻¹ * g_D ∈ HeckeCoset.toSet D₂ := by + rw [HeckeCoset.toSet_eq_rep, DoubleCoset.mem_doubleCoset] + rw [hg₂] at hcond + have hmem : (rep : G) * g₁ * ((j_rep : G) * (HeckeCoset.rep D₂ : G)) ∈ + ({g_D} : Set G) * ↑P.H := by + have h1 : (rep : G) * g₁ * ((j_rep : G) * (HeckeCoset.rep D₂ : G)) ∈ + ({(rep : G) * g₁} : Set G) * {(j_rep : G) * (HeckeCoset.rep D₂ : G)} * ↑P.H := + ⟨_, ⟨_, rfl, _, rfl, rfl⟩, 1, P.H.one_mem, mul_one _⟩ + rwa [hcond] at h1 + obtain ⟨w, hw, k, hk, hprod⟩ := hmem + rw [Set.mem_singleton_iff] at hw + refine ⟨(j_rep : G), j_rep.2, k⁻¹, P.H.inv_mem hk, ?_⟩ + have hprod' : g_D * k = + (rep : G) * g₁ * ((j_rep : G) * (HeckeCoset.rep D₂ : G)) := hw ▸ hprod + calc g₁⁻¹ * (rep : G)⁻¹ * g_D + = g₁⁻¹ * (rep : G)⁻¹ * (g_D * k * k⁻¹) := by group + _ = g₁⁻¹ * (rep : G)⁻¹ * + ((rep : G) * g₁ * ((j_rep : G) * (HeckeCoset.rep D₂ : G)) * k⁻¹) := by + rw [hprod'] + _ = (j_rep : G) * (HeckeCoset.rep D₂ : G) * k⁻¹ := by group + +private lemma conj_mem_of_stabilizer (g : G) + (n : ((ConjAct.toConjAct g • P.H).subgroupOf P.H)) : + 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 + +private lemma bar_quotient_diff_mem_H + (x₁ x₂ : G) (g₂ a₁ b₁ a₂ b₂ : G) + (_ : a₁ ∈ (P.H : Set G)) (hb₁ : b₁ ∈ (P.H : Set G)) + (_ : a₂ ∈ (P.H : Set G)) (hb₂ : b₂ ∈ (P.H : Set G)) + (hbarx₁ : ι.bar x₁ = a₁ * g₂ * b₁) + (hbarx₂ : ι.bar x₂ = a₂ * g₂ * b₂) + (hconj : g₂⁻¹ * a₁⁻¹ * a₂ * g₂ ∈ P.H) : + x₂ * x₁⁻¹ ∈ P.H := by + rw [← ι.bar_bar (x₂ * x₁⁻¹)] + refine ι.bar_mem_H ?_ + rw [show ι.bar (x₂ * x₁⁻¹) = (ι.bar x₁)⁻¹ * ι.bar x₂ by + rw [← ι.bar_inv, ← ι.bar_mul], + show (ι.bar x₁)⁻¹ * ι.bar x₂ = + b₁⁻¹ * (g₂⁻¹ * a₁⁻¹ * a₂ * g₂) * b₂ by + rw [hbarx₁, hbarx₂] + group] + exact P.H.mul_mem (P.H.mul_mem (P.H.inv_mem hb₁) hconj) hb₂ + +private lemma decompQuot_eq_of_conj_mem (g₁ : P.Δ) + (i₁ i₂ : decompQuot P g₁) (g_D : G) + (hxx_H : (((g₁ : G))⁻¹ * (i₂.out : G)⁻¹ * g_D) * + (((g₁ : G))⁻¹ * (i₁.out : G)⁻¹ * g_D)⁻¹ ∈ P.H) : + i₁ = i₂ := by + have hconj_H : + ((g₁ : G))⁻¹ * (i₂.out : G)⁻¹ * (i₁.out : G) * ((g₁ : G)) ∈ P.H := by + convert hxx_H using 1 + group + have hconj_H' : + ((g₁ : G))⁻¹ * (i₁.out : G)⁻¹ * (i₂.out : G) * ((g₁ : G)) ∈ P.H := by + convert P.H.inv_mem hconj_H using 1 + group + rw [show i₁ = ⟦i₁.out⟧ from (Quotient.out_eq' i₁).symm, + show i₂ = ⟦i₂.out⟧ from (Quotient.out_eq' i₂).symm, + @Quotient.eq'', QuotientGroup.leftRel_apply, + Subgroup.mem_subgroupOf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ConjAct.smul_def] + simp only [map_inv, ConjAct.ofConjAct_toConjAct, inv_inv] + convert hconj_H' using 1 + simp [Subgroup.coe_mul] + group + +private lemma conj_kernel_mem_of_stabilizer_mem + (a₁ a₂ : P.H) (g₂ : G) + (hrel : (a₁ : P.H)⁻¹ * a₂ ∈ (ConjAct.toConjAct g₂ • P.H).subgroupOf P.H) : + g₂⁻¹ * (a₁ : G)⁻¹ * (a₂ : G) * g₂ ∈ P.H := by + rw [Subgroup.mem_subgroupOf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, + ConjAct.smul_def] at hrel + simp only [map_inv, ConjAct.ofConjAct_toConjAct, inv_inv, Subgroup.coe_mul, + Subgroup.coe_inv] at hrel + convert hrel using 1 + group + +private lemma fwd_inj_i (g₁ g₂ : P.Δ) (g_D : G) + (i₁ i₂ : decompQuot P g₁) + (a₁ : P.H) (b₁ : G) (hb₁ : b₁ ∈ (P.H : Set G)) + (hbarx₁_eq : ι.bar (((g₁ : G))⁻¹ * (i₁.out : G)⁻¹ * g_D) = + (a₁ : G) * ((g₂ : G)) * b₁) + (a₂ : P.H) (b₂ : G) (hb₂ : b₂ ∈ (P.H : Set G)) + (hbarx₂_eq : ι.bar (((g₁ : G))⁻¹ * (i₂.out : G)⁻¹ * g_D) = + (a₂ : G) * ((g₂ : G)) * b₂) + (hj'_eq : (⟦a₁⟧ : decompQuot P g₂) = ⟦a₂⟧) : i₁ = i₂ := by + rw [@Quotient.eq'', QuotientGroup.leftRel_apply] at hj'_eq + exact decompQuot_eq_of_conj_mem g₁ i₁ i₂ g_D + (bar_quotient_diff_mem_H ι + (((g₁ : G))⁻¹ * (i₁.out : G)⁻¹ * g_D) + (((g₁ : G))⁻¹ * (i₂.out : G)⁻¹ * g_D) + ((g₂ : G)) + (a₁ : G) b₁ (a₂ : G) b₂ + a₁.2 hb₁ a₂.2 hb₂ hbarx₁_eq hbarx₂_eq + (conj_kernel_mem_of_stabilizer_mem a₁ a₂ ((g₂ : G)) hj'_eq)) + +private lemma fwd_y_mem (g₁ g₂ g_D : G) + (i_val : G) (hi : i_val ∈ (P.H : Set G)) + (a_val : G) (b_val : G) (hb : b_val ∈ (P.H : Set G)) + (hbarx_eq : ι.bar (g₁⁻¹ * i_val⁻¹ * g_D) = a_val * g₂ * b_val) + (h1₁ h2₁ : P.H) + (hbar₁' : ι.bar g₁ = (h1₁ : G) * g₁ * (h2₁ : G)) + (j'_val q₀_val h'_val : G) + (hq₀_eq : q₀_val * g_D = ι.bar g_D * h'_val) + (h'_mem : h'_val ∈ (P.H : Set G)) + (hn₂_val : G) (hn₂_mem : g₂⁻¹ * hn₂_val * g₂ ∈ P.H) + (hj'_coe : j'_val = a_val * hn₂_val) : + ∃ h₁ ∈ (P.H : Set G), ∃ h₂ ∈ (P.H : Set G), + g₂⁻¹ * j'_val⁻¹ * q₀_val * g_D = h₁ * g₁ * h₂ := by + have hab_eq : a_val * g₂ * b_val = + ι.bar g_D * (ι.bar i_val)⁻¹ * (ι.bar g₁)⁻¹ := by + rw [← hbarx_eq, ι.bar_mul, ι.bar_mul, ι.bar_inv, ι.bar_inv] + group + have key1 : g₂⁻¹ * a_val⁻¹ * ι.bar g_D = + b_val * ι.bar g₁ * ι.bar i_val := by + calc g₂⁻¹ * a_val⁻¹ * ι.bar g_D + = g₂⁻¹ * a_val⁻¹ * (a_val * g₂ * b_val * + (ι.bar g₁ * ι.bar i_val)) := by + rw [hab_eq] + group + _ = _ := by group + rw [show g₂⁻¹ * j'_val⁻¹ * q₀_val * g_D = + (g₂⁻¹ * hn₂_val⁻¹ * g₂) * (b_val * ι.bar g₁ * ι.bar i_val) * h'_val by + rw [hj'_coe, show g₂⁻¹ * (a_val * hn₂_val)⁻¹ * q₀_val * g_D = + g₂⁻¹ * (a_val * hn₂_val)⁻¹ * (q₀_val * g_D) by group, + hq₀_eq, ← key1] + group, hbar₁'] + have hn₂_inv_mem : g₂⁻¹ * hn₂_val⁻¹ * g₂ ∈ P.H := by + convert P.H.inv_mem hn₂_mem using 1 + group + exact ⟨(g₂⁻¹ * hn₂_val⁻¹ * g₂) * b_val * h1₁, + P.H.mul_mem (P.H.mul_mem hn₂_inv_mem hb) h1₁.2, + h2₁ * ι.bar i_val * h'_val, + P.H.mul_mem (P.H.mul_mem h2₁.2 (ι.bar_mem_H hi)) h'_mem, by group⟩ + +private lemma fwd_pair_mem (g₁ : P.Δ) (g₂ g_D q₀_val : G) + (j'_val : G) (c : P.H) (d_val : G) (hd : d_val ∈ (P.H : Set G)) + (hy_eq : g₂⁻¹ * j'_val⁻¹ * q₀_val * g_D = (c : G) * (g₁ : G) * d_val) : + ({j'_val * g₂} : Set G) * {((⟦c⟧ : decompQuot P g₁).out : G) * (g₁ : G)} * + ↑P.H = {q₀_val * g_D} * ↑P.H := by + rw [Set.singleton_mul_singleton] + obtain ⟨n₁, hn₁_eq⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct ((g₁ : G)) • P.H).subgroupOf P.H) c + have hn₁_coe : ((⟦c⟧ : decompQuot P g₁).out : G) = (c : G) * (n₁ : G) := by + simpa [Subgroup.coe_mul] using congr_arg (Subtype.val : ↥P.H → G) hn₁_eq + apply leftCoset_eq_of_not_disjoint + rw [@Set.not_disjoint_iff] + refine ⟨j'_val * g₂ * (((⟦c⟧ : decompQuot P g₁).out : G) * ((g₁ : G))), + ⟨1, P.H.one_mem, by simp [smul_eq_mul]⟩, ?_⟩ + refine ⟨d_val⁻¹ * (((g₁ : G))⁻¹ * (n₁ : G) * ((g₁ : G))), + P.H.mul_mem (P.H.inv_mem hd) (conj_mem_of_stabilizer ((g₁ : G)) n₁), ?_⟩ + simp only [smul_eq_mul] + rw [hn₁_coe] + have h_prod_eq : j'_val * g₂ * ((c : G) * ((g₁ : G)) * d_val) = + q₀_val * g_D := by + rw [← hy_eq] + group + calc q₀_val * g_D * (d_val⁻¹ * (((g₁ : G))⁻¹ * (n₁ : G) * ((g₁ : G)))) + = (q₀_val * g_D * d_val⁻¹) * + (((g₁ : G))⁻¹ * (n₁ : G) * ((g₁ : G))) := by group + _ = j'_val * g₂ * ((c : G) * ((g₁ : G))) * + (((g₁ : G))⁻¹ * (n₁ : G) * ((g₁ : G))) := by + rw [← h_prod_eq] + group + _ = j'_val * g₂ * ((c : G) * (n₁ : G) * ((g₁ : G))) := by group + +private lemma q₀_out_mul_eq_bar_mul (D : HeckeCoset P) (h1D h2D : P.H) + (hbarD : ι.bar (HeckeCoset.rep D : G) = + (h1D : G) * (HeckeCoset.rep D : G) * (h2D : G)) + (q₀ : decompQuot P (HeckeCoset.rep D)) (hq₀ : q₀ = ⟦⟨(h1D : G), h1D.2⟩⟧) : + ∃ h' : P.H, (q₀.out : G) * (HeckeCoset.rep D : G) = + ι.bar (HeckeCoset.rep D : G) * (h' : G) := by + subst hq₀ + obtain ⟨n, hn_eq⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (HeckeCoset.rep D : G) • P.H).subgroupOf P.H) ⟨(h1D : G), h1D.2⟩ + have hn_coe : + ((⟦⟨(h1D : G), h1D.2⟩⟧ : decompQuot P (HeckeCoset.rep D)).out : G) = + (h1D : G) * (n : G) := by + simpa [Subgroup.coe_mul] using congr_arg (Subtype.val : ↥P.H → G) hn_eq + exact ⟨⟨(h2D : G)⁻¹ * ((HeckeCoset.rep D : G)⁻¹ * (n : G) * (HeckeCoset.rep D : G)), + P.H.mul_mem (P.H.inv_mem h2D.2) (conj_mem_of_stabilizer (HeckeCoset.rep D : G) n)⟩, + by + rw [hn_coe, hbarD] + group⟩ + +private noncomputable def heckeMultiplicity_le_comm_fwdMap + (h_fix : ∀ D : HeckeCoset P, ι.onHeckeCoset D = D) (D₁ D₂ D : HeckeCoset P) + (h1D h2D : P.H) + (hbarD : ι.bar (HeckeCoset.rep D : G) = + (h1D : G) * (HeckeCoset.rep D : G) * (h2D : G)) + (h1₁ h2₁ : P.H) + (hbar₁ : ι.bar (HeckeCoset.rep D₁ : G) = + (h1₁ : G) * (HeckeCoset.rep D₁ : G) * (h2₁ : G)) + (q₀ : decompQuot P (HeckeCoset.rep D)) (hq₀ : q₀ = ⟦⟨(h1D : G), h1D.2⟩⟧) + (p : {⟨i, j⟩ : decompQuot P (HeckeCoset.rep D₁) × decompQuot P (HeckeCoset.rep D₂) | + ({(i.out : G) * (HeckeCoset.rep D₁ : G)} : Set G) * + {(j.out : G) * (HeckeCoset.rep D₂ : G)} * P.H = + {(HeckeCoset.rep D : G)} * (P.H : Set G)}) : + {p : decompQuot P (HeckeCoset.rep D₂) × decompQuot P (HeckeCoset.rep D₁) | + ({(p.1.out : G) * (HeckeCoset.rep D₂ : G)} : Set G) * + {(p.2.out : G) * (HeckeCoset.rep D₁ : G)} * P.H = + {(q₀.out : G) * (HeckeCoset.rep D : G)} * (P.H : Set G)} := + let i := p.1.1 + let j := p.1.2 + let hcond : ({(i.out : G) * (HeckeCoset.rep D₁ : G)} : Set G) * + {(j.out : G) * (HeckeCoset.rep D₂ : G)} * P.H = + {(HeckeCoset.rep D : G)} * (P.H : Set G) := p.2 + let x : G := (HeckeCoset.rep D₁ : G)⁻¹ * (i.out : G)⁻¹ * (HeckeCoset.rep D : G) + have hbarx_dc : ∃ h₁ ∈ (P.H : Set G), ∃ h₂ ∈ (P.H : Set G), + ι.bar x = h₁ * (HeckeCoset.rep D₂ : G) * h₂ := by + have := bar_mem_doubleCoset ι h_fix D₂ x + (inverse_product_mem_doubleCoset (HeckeCoset.rep D₁ : G) (HeckeCoset.rep D₂ : G) + (HeckeCoset.rep D : G) D₂ rfl i.out j.out hcond) + rwa [HeckeCoset.toSet_eq_rep, DoubleCoset.mem_doubleCoset] at this + let a : P.H := ⟨hbarx_dc.choose, hbarx_dc.choose_spec.1⟩ + let j' : decompQuot P (HeckeCoset.rep D₂) := ⟦a⟧ + have hy_mem_D₁ : (HeckeCoset.rep D₂ : G)⁻¹ * (j'.out : G)⁻¹ * (q₀.out : G) * + (HeckeCoset.rep D : G) ∈ HeckeCoset.toSet D₁ := by + rw [HeckeCoset.toSet_eq_rep, DoubleCoset.mem_doubleCoset] + obtain ⟨h', hq₀_eq⟩ := q₀_out_mul_eq_bar_mul ι D h1D h2D hbarD q₀ hq₀ + obtain ⟨n₂, hn₂_eq⟩ := QuotientGroup.mk_out_eq_mul + ((ConjAct.toConjAct (HeckeCoset.rep D₂ : G) • P.H).subgroupOf P.H) a + exact fwd_y_mem ι (HeckeCoset.rep D₁ : G) (HeckeCoset.rep D₂ : G) + (HeckeCoset.rep D : G) (i.out : G) i.out.2 (a : G) + hbarx_dc.choose_spec.2.choose hbarx_dc.choose_spec.2.choose_spec.1 + hbarx_dc.choose_spec.2.choose_spec.2 h1₁ h2₁ hbar₁ + (j'.out : G) (q₀.out : G) (h' : G) hq₀_eq h'.2 (n₂ : G) + (conj_mem_of_stabilizer (HeckeCoset.rep D₂ : G) n₂) + (by simpa [Subgroup.coe_mul] using congr_arg (Subtype.val : ↥P.H → G) hn₂_eq) + have hy_dc : ∃ h₁ ∈ (P.H : Set G), ∃ h₂ ∈ (P.H : Set G), + (HeckeCoset.rep D₂ : G)⁻¹ * (j'.out : G)⁻¹ * (q₀.out : G) * (HeckeCoset.rep D : G) = + h₁ * (HeckeCoset.rep D₁ : G) * h₂ := by + rwa [HeckeCoset.toSet_eq_rep, DoubleCoset.mem_doubleCoset] at hy_mem_D₁ + let c : P.H := ⟨hy_dc.choose, hy_dc.choose_spec.1⟩ + ⟨⟨j', ⟦c⟧⟩, fwd_pair_mem (HeckeCoset.rep D₁) (HeckeCoset.rep D₂ : G) + (HeckeCoset.rep D : G) (q₀.out : G) (j'.out : G) c + hy_dc.choose_spec.2.choose hy_dc.choose_spec.2.choose_spec.1 + (hy_dc.choose_spec.2.choose_spec.2 ▸ rfl)⟩ + +private lemma heckeMultiplicity_le_comm_fwdMap_injective + (h_fix : ∀ D : HeckeCoset P, ι.onHeckeCoset D = D) (D₁ D₂ D : HeckeCoset P) + (h1D h2D : P.H) + (hbarD : ι.bar (HeckeCoset.rep D : G) = + (h1D : G) * (HeckeCoset.rep D : G) * (h2D : G)) + (h1₁ h2₁ : P.H) + (hbar₁ : ι.bar (HeckeCoset.rep D₁ : G) = + (h1₁ : G) * (HeckeCoset.rep D₁ : G) * (h2₁ : G)) + (q₀ : decompQuot P (HeckeCoset.rep D)) (hq₀ : q₀ = ⟦⟨(h1D : G), h1D.2⟩⟧) : + Function.Injective + (heckeMultiplicity_le_comm_fwdMap ι h_fix D₁ D₂ D h1D h2D hbarD h1₁ h2₁ hbar₁ + q₀ hq₀) := by + set g₁ := (HeckeCoset.rep D₁ : G) + set g₂ := (HeckeCoset.rep D₂ : G) + set g_D := (HeckeCoset.rep D : G) + intro ⟨⟨i₁, j₁⟩, h₁⟩ ⟨⟨i₂, j₂⟩, h₂⟩ heq + have hj'_eq := congr_arg Prod.fst (congr_arg Subtype.val heq) + have bar_dc (i' : decompQuot P (HeckeCoset.rep D₁)) + (j' : decompQuot P (HeckeCoset.rep D₂)) + (hc : ({(i'.out : G) * g₁} : Set G) * {(j'.out : G) * g₂} * ↑P.H = + {g_D} * ↑P.H) : ∃ h₁ ∈ (P.H : Set G), ∃ h₂ ∈ (P.H : Set G), + ι.bar (g₁⁻¹ * (i'.out : G)⁻¹ * g_D) = h₁ * g₂ * h₂ := by + have := bar_mem_doubleCoset ι h_fix D₂ _ + (inverse_product_mem_doubleCoset g₁ g₂ g_D D₂ rfl i'.out j'.out hc) + rwa [HeckeCoset.toSet_eq_rep, DoubleCoset.mem_doubleCoset] at this + have hbarx₁_dc := bar_dc i₁ j₁ h₁ + have hbarx₂_dc := bar_dc i₂ j₂ h₂ + change (⟦⟨hbarx₁_dc.choose, hbarx₁_dc.choose_spec.1⟩⟧ : + decompQuot P (HeckeCoset.rep D₂)) = + ⟦⟨hbarx₂_dc.choose, hbarx₂_dc.choose_spec.1⟩⟧ at hj'_eq + have hi₁₂ : i₁ = i₂ := fwd_inj_i ι (HeckeCoset.rep D₁) (HeckeCoset.rep D₂) + g_D i₁ i₂ + ⟨hbarx₁_dc.choose, hbarx₁_dc.choose_spec.1⟩ + hbarx₁_dc.choose_spec.2.choose hbarx₁_dc.choose_spec.2.choose_spec.1 + hbarx₁_dc.choose_spec.2.choose_spec.2 + ⟨hbarx₂_dc.choose, hbarx₂_dc.choose_spec.1⟩ + hbarx₂_dc.choose_spec.2.choose hbarx₂_dc.choose_spec.2.choose_spec.1 + hbarx₂_dc.choose_spec.2.choose_spec.2 hj'_eq + subst hi₁₂ + have hj₁₂ : j₁ = j₂ := by + by_contra hne + apply decompQuot_coset_diff P (HeckeCoset.rep D₂) j₁ j₂ hne + exact set_singleton_mul_left_cancel ((i₁.out : G) * g₁) + (by + have := h₁.trans h₂.symm + rwa [mul_assoc, mul_assoc] at this) + subst hj₁₂ + rfl + +private lemma heckeMultiplicity_le_comm (h_fix : ∀ D : HeckeCoset P, ι.onHeckeCoset D = D) + (D₁ D₂ D : HeckeCoset P) : + heckeMultiplicity P (HeckeCoset.rep D₁) (HeckeCoset.rep D₂) (HeckeCoset.rep D) ≤ + heckeMultiplicity P (HeckeCoset.rep D₂) (HeckeCoset.rep D₁) (HeckeCoset.rep D) := by + obtain ⟨h1D, h2D, hbarD⟩ := bar_rep_mem_doubleCoset ι h_fix D + obtain ⟨h1₁, h2₁, hbar₁⟩ := bar_rep_mem_doubleCoset ι h_fix D₁ + set q₀ : decompQuot P (HeckeCoset.rep D) := ⟦⟨(h1D : G), h1D.2⟩⟧ with hq₀ + unfold heckeMultiplicity + rw [← heckeMultiplicity_uniform P (HeckeCoset.rep D₂) (HeckeCoset.rep D₁) D q₀] + exact_mod_cast Nat.card_le_card_of_injective + (heckeMultiplicity_le_comm_fwdMap ι h_fix D₁ D₂ D h1D h2D hbarD h1₁ h2₁ hbar₁ + q₀ hq₀) + (heckeMultiplicity_le_comm_fwdMap_injective ι h_fix D₁ D₂ D h1D h2D hbarD + h1₁ h2₁ hbar₁ q₀ hq₀) + +/-- When the anti-involution fixes all double cosets, +the multiplicity is symmetric: +`heckeMultiplicity(D₁, D₂, D) = heckeMultiplicity(D₂, D₁, D)` +(Shimura Proposition 3.8). -/ +lemma heckeMultiplicity_comm_of_onHeckeCoset_eq + (h_fix : ∀ D : HeckeCoset P, ι.onHeckeCoset D = D) + (D₁ D₂ D : HeckeCoset P) : + heckeMultiplicity P (HeckeCoset.rep D₁) (HeckeCoset.rep D₂) (HeckeCoset.rep D) = + heckeMultiplicity P (HeckeCoset.rep D₂) (HeckeCoset.rep D₁) (HeckeCoset.rep D) := + le_antisymm (ι.heckeMultiplicity_le_comm h_fix D₁ D₂ D) + (ι.heckeMultiplicity_le_comm h_fix D₂ D₁ D) + +/-- When the anti-involution fixes all double cosets, +the multiplication finsupp is symmetric: `m(D₁, D₂) = m(D₂, D₁)`. -/ +lemma m_comm_of_onHeckeCoset_eq (h_fix : ∀ D : HeckeCoset P, ι.onHeckeCoset D = D) + (D₁ D₂ : HeckeCoset P) : + m P (HeckeCoset.rep D₁) (HeckeCoset.rep D₂) = + m P (HeckeCoset.rep D₂) (HeckeCoset.rep D₁) := by + ext D + simpa only [m, Finsupp.coe_mk] using + heckeMultiplicity_comm_of_onHeckeCoset_eq ι h_fix D₁ D₂ D + +/-- Shimura Proposition 3.8: the Hecke ring is commutative when the anti-involution +fixes every double coset. -/ +theorem mul_comm_of_antiInvolution (h_fix : ∀ D : HeckeCoset P, ι.onHeckeCoset D = D) + (f g : 𝕋 P ℤ) : f * g = g * f := by + apply induction_linear_𝕋 P f + · simp + · intro D₁ a + apply induction_linear_𝕋 P g + · simp + · intro D₂ b + rw [T_single_mul_T_single, T_single_mul_T_single, + m_comm_of_onHeckeCoset_eq ι h_fix D₁ D₂, smul_comm] + · intro g₁ g₂ hg₁ hg₂ + rw [mul_add, add_mul, hg₁, hg₂] + · intro f₁ f₂ hf₁ hf₂ + rw [add_mul, mul_add, hf₁, hf₂] + +end AntiInvolution + +/-- Shimura Proposition 3.8: `CommRing (𝕋 P ℤ)` from an anti-involution +fixing every double coset. -/ +@[reducible] +noncomputable def instCommRing_of_antiInvolution (ι : AntiInvolution P) + (h_fix : ∀ D : HeckeCoset P, ι.onHeckeCoset D = D) : CommRing (𝕋 P ℤ) := + { HeckeRing.instRing P with mul_comm := ι.mul_comm_of_antiInvolution h_fix } + +end HeckeRing diff --git a/LeanBridge/ForMathlib/AbstractHeckeRing/Degree.lean b/LeanBridge/ForMathlib/AbstractHeckeRing/Degree.lean new file mode 100644 index 00000000..4ed7ee79 --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing/Degree.lean @@ -0,0 +1,284 @@ +/- +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 + +/-! +# Hecke Rings: Degree Map + +The degree ring homomorphism `deg : 𝕋 P ℤ →+* ℤ`, which sends each +double coset `HgH` to the number of left cosets it contains: +`deg(HgH) = [H : H ∩ gHg⁻¹]`. + +This is Shimura §3.1, Proposition 3.3. + +## Main definitions + +* `HeckeCoset_deg P D` : the degree of a single double coset +* `deg P` : the degree ring homomorphism `𝕋 P ℤ →+* ℤ` + +## Main results + +* `deg_T_single` : `deg(T_single D a) = a * HeckeCoset_deg D` +* `HeckeCoset_deg_pos` : `0 < HeckeCoset_deg D` +* `deg_mul` : `deg(f * g) = deg f * deg g` (the degree map is multiplicative) + +## Proof strategy + +Multiplicativity `deg(f * g) = deg(f) * deg(g)` is proved using the module action +on `HeckeModule P ℤ`. +We show `deg(f) = coeffSum(f • 1)` where `coeffSum` sums all coefficients, and then use +`IsScalarTower` (Shimura Prop 3.4) to get `(f * g) • 1 = g • (f • 1)`. The key intermediate +result is `coeffSum(f • m) = deg(f) * coeffSum(m)`, which follows from the orbit cardinality +lemma `smulOrbit_card`. +-/ + +open Classical MulOpposite Set DoubleCoset Subgroup + +open scoped Pointwise + +namespace HeckeRing + +variable {G : Type*} [Group G] +variable (P : HeckePair G) + +open Finsupp + +/-- The degree of a double coset: `deg(HgH) = [H : H ∩ gHg⁻¹]`, the number of left cosets +in the decomposition of `HgH`. -/ +noncomputable def HeckeCoset_deg (D : HeckeCoset P) : ℤ := + Fintype.card (decompQuot P (HeckeCoset.rep D)) + +/-- The degree of the identity double coset is 1. -/ +@[simp] lemma HeckeCoset_deg_T_one : HeckeCoset_deg P (HeckeCoset.one P) = 1 := by + haveI := subsingleton_decompQuot_T_one P + haveI : Unique (decompQuot P (HeckeCoset.one P).rep) := + uniqueOfSubsingleton (one_in_decompQuot_T_one P).some + simp [HeckeCoset_deg, Fintype.card_unique] + +/-- Every double coset has positive degree. -/ +lemma HeckeCoset_deg_pos (D : HeckeCoset P) : 0 < HeckeCoset_deg P D := by + unfold HeckeCoset_deg; exact_mod_cast Fintype.card_pos + +section SmulOrbitCard + +private lemma smulOrbit_map_inj (g : P.Δ) (β : 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 hset : ({(β : G) * (i₁.out : G) * (g : G)} : Set G) * (P.H : Set G) = + {(β : G) * (i₂.out : G) * (g : G)} * P.H := Quotient.exact heq + have hmem : (β : G) * (i₁.out : G) * (g : G) ∈ + ({(β : G) * (i₂.out : G) * (g : G)} : Set G) * (P.H : Set G) := + hset ▸ ⟨_, 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 + refine mul_left_cancel (a := (β : G)) ?_ + have := hkk; group at this ⊢; exact this + refine decompQuot_coset_diff P g i₁ i₂ hne + (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⟩⟩ + +/-- The cardinality of a smul orbit equals the degree of the acting double coset. -/ +lemma smulOrbit_card (g : P.Δ) (β : P.Δ) : + (smulOrbit P g β).card = Fintype.card (decompQuot P g) := by + show (Finset.image _ ⊤).card = _ + rw [Finset.top_eq_univ] + convert (Finset.card_image_of_injective Finset.univ + (smulOrbit_map_inj P g β)).trans Finset.card_univ + rfl + +/-- The cardinality of a smul orbit cast to `ℤ` equals `HeckeCoset_deg`. -/ +lemma smulOrbit_card_intCast (D : HeckeCoset P) (β : P.Δ) : + ((smulOrbit P (HeckeCoset.rep D) β).card : ℤ) = HeckeCoset_deg P D := by + simp [smulOrbit_card, HeckeCoset_deg] + +end SmulOrbitCard + +section CoeffSum + +/-- The coefficient sum homomorphism: sums all coefficients of a formal linear combination +of left cosets. -/ +noncomputable def coeffSum : HeckeModule P ℤ →+ ℤ := + Finsupp.liftAddHom (fun _ : HeckeLeftCoset P ↦ AddMonoidHom.id ℤ) + +/-- The coefficient sum of a single basis element is its coefficient. -/ +@[simp] lemma coeffSum_single (m₀ : HeckeLeftCoset P) (b : ℤ) : + coeffSum P (HeckeLeftCoset_single P ℤ m₀ b) = b := Finsupp.liftAddHom_apply_single _ _ _ + +/-- The coefficient sum is additive. -/ +lemma coeffSum_add (m₁ m₂ : HeckeModule P ℤ) : + coeffSum P (m₁ + m₂) = coeffSum P m₁ + coeffSum P m₂ := map_add _ _ _ + +/-- The coefficient sum distributes over finite sums. -/ +lemma coeffSum_finset_sum {ι : Type*} (s : Finset ι) (f : ι → HeckeModule P ℤ) : + coeffSum P (∑ i ∈ s, f i) = ∑ i ∈ s, coeffSum P (f i) := map_sum _ _ _ + +/-- The coefficient sum of a single-single smul product equals `a * deg(D) * b`. -/ +lemma coeffSum_single_smul_single (D : HeckeCoset P) (m₀ : HeckeLeftCoset P) (a b : ℤ) : + coeffSum P (T_single P ℤ D a • HeckeLeftCoset_single P ℤ m₀ b) = + a * HeckeCoset_deg P D * b := by + rw [T_single_smul_HeckeLeftCoset_single, coeffSum_finset_sum] + simp only [coeffSum_single, Finset.sum_const, Int.nsmul_eq_mul, + smulOrbit_card_intCast P D (HeckeLeftCoset.rep m₀)] + ring + +end CoeffSum + +section DegreeMap + +/-- The underlying function of the degree map: `Σ_D a_D * deg(D)`. -/ +noncomputable def deg_fun (f : 𝕋 P ℤ) : ℤ := f.sum fun D a ↦ a * HeckeCoset_deg P D + +/-- The degree function of zero is zero. -/ +@[simp] lemma deg_fun_zero : deg_fun P (0 : 𝕋 P ℤ) = 0 := Finsupp.sum_zero_index + +/-- The degree function of a basis element is `a * deg(D)`. -/ +@[simp] lemma deg_fun_T_single (D : HeckeCoset P) (a : ℤ) : + deg_fun P (T_single P ℤ D a) = a * HeckeCoset_deg P D := + Finsupp.sum_single_index (by simp) + +/-- The degree function is additive. -/ +lemma deg_fun_add (f g : 𝕋 P ℤ) : + deg_fun P (f + g) = deg_fun P f + deg_fun P g := + Finsupp.sum_add_index' (fun _ ↦ by simp) (fun _ _ _ ↦ by ring) + +/-- The degree function of the identity is 1. -/ +@[simp] lemma deg_fun_one : deg_fun P (1 : 𝕋 P ℤ) = 1 := by + simp [one_def] + +/-- The degree equals the coefficient sum of the action on the identity module element. -/ +lemma deg_fun_eq_coeffSum_smul_one (f : 𝕋 P ℤ) : + deg_fun P f = coeffSum P (f • (1 : HeckeModule P ℤ)) := by + let toT : (HeckeCoset P →₀ ℤ) → 𝕋 P ℤ := fun a ↦ a + let mot : (HeckeCoset P →₀ ℤ) → Prop := + fun f' ↦ deg_fun P (toT f') = coeffSum P ((toT f') • (1 : HeckeModule P ℤ)) + change mot f + apply Finsupp.induction_linear + · show deg_fun P (toT 0) = coeffSum P ((toT 0) • (1 : HeckeModule P ℤ)) + change deg_fun P (0 : 𝕋 P ℤ) = coeffSum P (((0 : 𝕋 P ℤ)) • (1 : HeckeModule P ℤ)) + simp [zero_smul_HeckeModule] + · intro f g ihf ihg + show deg_fun P (toT (f + g)) = + coeffSum P ((toT (f + g)) • (1 : HeckeModule P ℤ)) + change deg_fun P ((toT f + toT g) : 𝕋 P ℤ) = + coeffSum P (((toT f + toT g) : 𝕋 P ℤ) • (1 : HeckeModule P ℤ)) + rw [deg_fun_add, ihf, ihg, smul_add_left, coeffSum_add] + · intro D a + show deg_fun P (toT (Finsupp.single D a)) = + coeffSum P ((toT (Finsupp.single D a)) • (1 : HeckeModule P ℤ)) + rw [deg_fun_T_single, one_eq_HeckeLeftCoset_single, + coeffSum_single_smul_single, mul_one] + +/-- The coefficient sum of a smul product factors as `deg(f) * coeffSum(m)`. -/ +lemma coeffSum_smul_eq (f : 𝕋 P ℤ) (m : HeckeModule P ℤ) : + coeffSum P (f • m) = deg_fun P f * coeffSum P m := by + let toT : (HeckeCoset P →₀ ℤ) → 𝕋 P ℤ := fun a ↦ a + let toM : (HeckeLeftCoset P →₀ ℤ) → HeckeModule P ℤ := fun a ↦ a + let motf : (HeckeCoset P →₀ ℤ) → Prop := + fun f' ↦ coeffSum P ((toT f') • m) = deg_fun P (toT f') * coeffSum P m + change motf f + apply Finsupp.induction_linear + · show coeffSum P ((toT 0) • m) = deg_fun P (toT 0) * coeffSum P m + change coeffSum P (((0 : 𝕋 P ℤ)) • m) = deg_fun P (0 : 𝕋 P ℤ) * coeffSum P m + simp [zero_smul_HeckeModule] + · intro f₁ f₂ ih₁ ih₂ + show coeffSum P ((toT (f₁ + f₂)) • m) = + deg_fun P (toT (f₁ + f₂)) * coeffSum P m + change coeffSum P (((toT f₁ + toT f₂) : 𝕋 P ℤ) • m) = + deg_fun P ((toT f₁ + toT f₂) : 𝕋 P ℤ) * coeffSum P m + rw [smul_add_left, coeffSum_add, ih₁, ih₂, deg_fun_add]; ring + · intro D a + show coeffSum P ((toT (Finsupp.single D a)) • m) = + deg_fun P (toT (Finsupp.single D a)) * coeffSum P m + let motm : (HeckeLeftCoset P →₀ ℤ) → Prop := + fun m' ↦ coeffSum P ((toT (Finsupp.single D a)) • (toM m')) = + deg_fun P (toT (Finsupp.single D a)) * coeffSum P (toM m') + change motm m + apply Finsupp.induction_linear + · show coeffSum P ((toT (Finsupp.single D a)) • (toM 0)) = + deg_fun P (toT (Finsupp.single D a)) * coeffSum P (toM 0) + change coeffSum P ((toT (Finsupp.single D a)) • (0 : HeckeModule P ℤ)) = + deg_fun P (toT (Finsupp.single D a)) * coeffSum P (0 : HeckeModule P ℤ) + simp [smul_zero_HeckeModule] + · intro m₁ m₂ ih₁ ih₂ + show coeffSum P ((toT (Finsupp.single D a)) • (toM (m₁ + m₂))) = + deg_fun P (toT (Finsupp.single D a)) * coeffSum P (toM (m₁ + m₂)) + change coeffSum P + ((toT (Finsupp.single D a)) • ((toM m₁ + toM m₂) : HeckeModule P ℤ)) = + deg_fun P (toT (Finsupp.single D a)) * + coeffSum P ((toM m₁ + toM m₂) : HeckeModule P ℤ) + rw [smul_add_right, coeffSum_add, ih₁, ih₂, coeffSum_add, deg_fun_T_single]; ring + · intro m₀ b + show coeffSum P ((toT (Finsupp.single D a)) • (toM (Finsupp.single m₀ b))) = + deg_fun P (toT (Finsupp.single D a)) * coeffSum P (toM (Finsupp.single m₀ b)) + rw [coeffSum_single_smul_single, coeffSum_single, deg_fun_T_single] + +/-- The degree function is multiplicative. -/ +lemma deg_fun_mul (f g : 𝕋 P ℤ) : + deg_fun P (f * g) = deg_fun P f * deg_fun P g := by + have h := (instIsScalarTower P).smul_assoc g f (1 : HeckeModule P ℤ) + simp only [smul_def] at h + rw [deg_fun_eq_coeffSum_smul_one P (f * g), h, coeffSum_smul_eq, + ← deg_fun_eq_coeffSum_smul_one P f]; ring + +/-- The degree ring homomorphism `deg : 𝕋 P ℤ →+* ℤ`, sending each double coset to the +number of left cosets it contains (Shimura Proposition 3.3). -/ +noncomputable def deg : 𝕋 P ℤ →+* ℤ where + toFun := deg_fun P + map_zero' := deg_fun_zero P + map_one' := deg_fun_one P + map_add' := deg_fun_add P + map_mul' := deg_fun_mul P + +end DegreeMap + +section API + +/-- The degree of a basis element is the coefficient times the degree of the double coset. -/ +@[simp] lemma deg_T_single (D : HeckeCoset P) (a : ℤ) : + deg P (T_single P ℤ D a) = a * HeckeCoset_deg P D := deg_fun_T_single P D a + +/-- The degree map is multiplicative: `deg(f * g) = deg(f) * deg(g)`. -/ +lemma deg_mul (f g : 𝕋 P ℤ) : deg P (f * g) = deg P f * deg P g := (deg P).map_mul f g + +/-- **Generic multiplicity-degree-sum identity**: when the support of the +multiplication finsupp `m P D₁ D₂` is contained in `{D_out1, D_out2}`, the +weighted sum of multiplicities by degrees equals the product of degrees. -/ +lemma heckeMultiplicity_deg_sum_eq (D1 D2 D_out1 D_out2 : HeckeCoset P) + (h_ne : D_out1 ≠ D_out2) (h_zero : ∀ A, A ≠ D_out1 → A ≠ D_out2 → + heckeMultiplicity P (HeckeCoset.rep D1) (HeckeCoset.rep D2) + (HeckeCoset.rep A) = 0) : + heckeMultiplicity P (HeckeCoset.rep D1) (HeckeCoset.rep D2) + (HeckeCoset.rep D_out1) * HeckeCoset_deg P D_out1 + + heckeMultiplicity P (HeckeCoset.rep D1) (HeckeCoset.rep D2) + (HeckeCoset.rep D_out2) * HeckeCoset_deg P D_out2 = + HeckeCoset_deg P D1 * HeckeCoset_deg P D2 := by + have h1 : deg P (m P (HeckeCoset.rep D1) (HeckeCoset.rep D2)) = + HeckeCoset_deg P D1 * HeckeCoset_deg P D2 := by + rw [← T_single_one_mul_T_single_one, deg_mul, deg_T_single, deg_T_single]; ring + have h2 : deg P (m P (HeckeCoset.rep D1) (HeckeCoset.rep D2)) = + heckeMultiplicity P (HeckeCoset.rep D1) (HeckeCoset.rep D2) + (HeckeCoset.rep D_out1) * HeckeCoset_deg P D_out1 + + heckeMultiplicity P (HeckeCoset.rep D1) (HeckeCoset.rep D2) + (HeckeCoset.rep D_out2) * HeckeCoset_deg P D_out2 := by + simp only [deg, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, deg_fun] + have hsub : (m P (HeckeCoset.rep D1) (HeckeCoset.rep D2)).support ⊆ + ({D_out1, D_out2} : Finset _) := fun A hA ↦ by + simp only [Finset.mem_insert, Finset.mem_singleton] + rw [Finsupp.mem_support_iff] at hA + exact or_iff_not_imp_left.mpr fun h1 ↦ + (Classical.em (A = D_out2)).elim id fun h2 ↦ absurd (h_zero A h1 h2) hA + exact (Finset.sum_subset hsub fun A _ hA ↦ by + rw [Finsupp.notMem_support_iff.mp hA]; simp).trans (Finset.sum_pair h_ne) + linarith + +end API + +end HeckeRing 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 diff --git a/LeanBridge/ForMathlib/AbstractHeckeRing/StabConjugation.lean b/LeanBridge/ForMathlib/AbstractHeckeRing/StabConjugation.lean new file mode 100644 index 00000000..580ec152 --- /dev/null +++ b/LeanBridge/ForMathlib/AbstractHeckeRing/StabConjugation.lean @@ -0,0 +1,142 @@ +/- +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 + +/-! +# Stabilizer invariance and conjugation equivalences on `decompQuot` + +For an abstract `HeckePair P`: + +* Right multiplication by `h ∈ P.H` does not change the stabilizer subgroup + (`stabilizerSubgroup_mul_right_H`). +* Left multiplication by `h ∈ P.H` conjugates the stabilizer + (`stab_mul_left_eq_map_conj`). +* These combine to give `Equiv`s of decomposition quotients + (`decompQuot_mul_left_equiv`, `decompQuot_double_H_equiv`) used in the + `CongruenceHecke` degree-combinatorics computations. +-/ + +open scoped Pointwise + +namespace HeckeRing + +section StabilizerInvariance + +variable {G : Type*} [Group G] (P : HeckePair G) + +/-- Right multiplication by `h ∈ H` does not change the stabilizer subgroup: +`Stab(g·h) = Stab(g)` when `h ∈ H`, +because `(g·h)H(g·h)⁻¹ = g(hHh⁻¹)g⁻¹ = gHg⁻¹`. -/ +lemma stabilizerSubgroup_mul_right_H (g : P.Δ) (h : P.H) : + (ConjAct.toConjAct ((g : G) * (h : G)) • P.H).subgroupOf P.H = + (ConjAct.toConjAct (g : G) • P.H).subgroupOf P.H := by + ext x + simp only [Subgroup.mem_subgroupOf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, + ConjAct.smul_def, map_inv, ConjAct.ofConjAct_toConjAct, inv_inv] + refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩ + · rw [show (g : G)⁻¹ * (x : G) * g = + (h : G) * (((g : G) * (h : G))⁻¹ * (x : G) * ((g : G) * (h : G))) * (h : G)⁻¹ by group] + exact P.H.mul_mem (P.H.mul_mem h.2 hx) (P.H.inv_mem h.2) + · rw [show ((g : G) * (h : G))⁻¹ * (x : G) * ((g : G) * (h : G)) = + (h : G)⁻¹ * ((g : G)⁻¹ * (x : G) * (g : G)) * (h : G) by group] + exact P.H.mul_mem (P.H.mul_mem (P.H.inv_mem h.2) hx) h.2 + +/-- Left multiplication by `h ∈ H` conjugates the stabilizer: +`Stab(h·g) = conj(h)(Stab(g))` as subgroups of `H`. +Concretely, `x ∈ Stab(h·g)` iff `h⁻¹·x·h ∈ Stab(g)`. -/ +lemma stab_mul_left_eq_map_conj (g : P.Δ) (h : P.H) : + (ConjAct.toConjAct ((h : G) * (g : G)) • P.H).subgroupOf P.H = + ((ConjAct.toConjAct (g : G) • P.H).subgroupOf P.H).map + (MulAut.conj h).toMonoidHom := by + ext x + simp only [Subgroup.mem_subgroupOf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem, + ConjAct.smul_def, map_inv, ConjAct.ofConjAct_toConjAct, inv_inv, + Subgroup.mem_map, MulEquiv.coe_toMonoidHom, MulAut.conj_apply] + refine ⟨fun hx ↦ ?_, ?_⟩ + · refine ⟨⟨(h : G)⁻¹ * (x : G) * (h : G), + P.H.mul_mem (P.H.mul_mem (P.H.inv_mem h.2) x.2) h.2⟩, ?_, ?_⟩ + · change (g : G)⁻¹ * ((h : G)⁻¹ * (x : G) * (h : G)) * (g : G) ∈ P.H + rw [show (g : G)⁻¹ * ((h : G)⁻¹ * (x : G) * (h : G)) * (g : G) = + ((h : G) * (g : G))⁻¹ * (x : G) * ((h : G) * (g : G)) by group] + exact hx + · ext + change (h : G) * ((h : G)⁻¹ * (x : G) * (h : G)) * (h : G)⁻¹ = (x : G) + group + · rintro ⟨y, hy, rfl⟩ + change ((h : G) * (g : G))⁻¹ * ((h : G) * (y : G) * (h : G)⁻¹) * + ((h : G) * (g : G)) ∈ P.H + rw [show ((h : G) * (g : G))⁻¹ * ((h : G) * (y : G) * (h : G)⁻¹) * ((h : G) * (g : G)) = + (g : G)⁻¹ * (y : G) * (g : G) by group] + exact hy + +end StabilizerInvariance + +section ConjugationEquiv + +variable {G : Type*} [Group G] (P : HeckePair G) + +/-- Conjugation by `h⁻¹` is the inverse automorphism of conjugation by `h`; the two `MulAut.conj` +maps used to build `decompQuot_mul_left_equiv` are mutually inverse. -/ +private lemma conj_inv_eq_symm {H : Type*} [Group H] (h : H) : + MulAut.conj h⁻¹ = (MulAut.conj h).symm := by + rw [map_inv, MulAut.inv_def] + +/-- Conjugation by `h ∈ H` gives an Equiv on decomposition quotients: +`H/Stab(h·g) ≃ H/Stab(g)` via `σ ↦ h⁻¹·σ·h`. + +The well-definedness uses `Stab(h·g) = h·Stab(g)·h⁻¹`, which means +`σ₁ ~_{Stab(h·g)} σ₂` iff `h⁻¹·σ₁·h ~_{Stab(g)} h⁻¹·σ₂·h`. -/ +noncomputable def decompQuot_mul_left_equiv (g : P.Δ) (h : P.H) + (hm : (h : G) * (g : G) ∈ P.Δ) : + decompQuot P ⟨(h : G) * g, hm⟩ ≃ decompQuot P g := by + set K := (ConjAct.toConjAct (g : G) • P.H).subgroupOf P.H + set K' := K.map (MulAut.conj h).toMonoidHom + refine (Subgroup.quotientEquivOfEq (stab_mul_left_eq_map_conj P g h)).trans ?_ + have h_wd : ∀ a b : P.H, QuotientGroup.leftRel K' a b → + QuotientGroup.leftRel K ((MulAut.conj h⁻¹) a) ((MulAut.conj h⁻¹) b) := by + intro a b hab + rw [QuotientGroup.leftRel_apply] at hab ⊢ + simp only [← map_inv, ← map_mul] + obtain ⟨k, hk, hkeq⟩ := Subgroup.mem_map.mp hab + rw [show a⁻¹ * b = (MulAut.conj h) k from hkeq.symm, conj_inv_eq_symm, + MulEquiv.symm_apply_apply] + exact hk + exact Equiv.ofBijective + (Quotient.map' (MulAut.conj h⁻¹) h_wd) + ⟨fun x y ↦ by + revert x y + refine Quotient.ind₂ fun a b hxy ↦ ?_ + simp only [Quotient.map'_mk''] at hxy + rw [Quotient.eq''] at hxy ⊢ + rw [QuotientGroup.leftRel_apply] at hxy ⊢ + simp only [← map_inv, ← map_mul] at hxy + exact Subgroup.mem_map.mpr ⟨(MulAut.conj h⁻¹) (a⁻¹ * b), hxy, by + rw [conj_inv_eq_symm, MulEquiv.coe_toMonoidHom, MulEquiv.apply_symm_apply]⟩, + fun x ↦ by + revert x + refine Quotient.ind fun b ↦ ⟨Quotient.mk'' ((MulAut.conj h) b), ?_⟩ + simp only [Quotient.map'_mk''] + rw [Quotient.eq'', QuotientGroup.leftRel_apply, conj_inv_eq_symm, + MulEquiv.symm_apply_apply, inv_mul_cancel] + exact K.one_mem⟩ + +/-- Combined left-right invariance: `decompQuot(h·g·k) ≃ decompQuot(g)` for `h, k ∈ H`. +Composes right-invariance (stabilizer equality) with left-conjugation. -/ +noncomputable def decompQuot_double_H_equiv (g : P.Δ) (h k : P.H) + (hm : (h : G) * (g : G) * (k : G) ∈ P.Δ) : + decompQuot P ⟨(h : G) * (g : G) * (k : G), hm⟩ ≃ decompQuot P g := by + have hgk : (g : G) * (k : G) ∈ P.Δ := P.Δ.mul_mem g.2 (P.h₀ k.2) + have hhgk : (h : G) * ((g : G) * (k : G)) ∈ P.Δ := by rwa [mul_assoc] at hm + refine (Subgroup.quotientEquivOfEq ?_).trans + ((decompQuot_mul_left_equiv P ⟨(g : G) * k, hgk⟩ h hhgk).trans + (Subgroup.quotientEquivOfEq (stabilizerSubgroup_mul_right_H P g k))) + change (ConjAct.toConjAct ((h : G) * (g : G) * (k : G)) • P.H).subgroupOf P.H = + (ConjAct.toConjAct ((h : G) * ((g : G) * (k : G))) • P.H).subgroupOf P.H + congr 2; exact mul_assoc _ _ _ + +end ConjugationEquiv + +end HeckeRing