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.

theorem HeckeRing.HeckeCoset_ext_toSet {G : Type u_1} [Group G] (P : HeckePair G) {D₁ D₂ : HeckeCoset P} (h : D₁.toSet = D₂.toSet) : D₁ = D₂

Two HeckeCoset elements are equal iff their toSets are equal.

theorem HeckeRing.decompQuot_T_one_eq_top {G : Type u_1} [Group G] (P : HeckePair G) : (ConjAct.toConjAct ↑(HeckeCoset.one P).rep • P.H).subgroupOf P.H = ⊤

The stabilizer quotient for the identity double coset is trivial.

theorem HeckeRing.one_in_decompQuot_T_one {G : Type u_1} [Group G] (P : HeckePair G) : Nonempty (decompQuot P (HeckeCoset.one P).rep)

The decomposition quotient for HeckeCoset.one is nonempty.

theorem HeckeRing.subsingleton_decompQuot_T_one {G : Type u_1} [Group G] (P : HeckePair G) : Subsingleton (decompQuot P (HeckeCoset.one P).rep)

The decomposition quotient for HeckeCoset.one is a subsingleton.

theorem HeckeRing.decompQuot_coset_diff {G : Type u_1} [Group G] (P : HeckePair G) (g : ↥P.Δ) (i j : decompQuot P g) (hij : i ≠ j) : {↑(Quotient.out i) * ↑g} * ↑P.H ≠ {↑(Quotient.out j) * ↑g} * ↑P.H

Distinct elements of decompQuot give distinct left cosets.

theorem HeckeRing.leftCoset_eq_of_not_disjoint {G : Type u_1} [Group G] (H : Subgroup G) (f g : G) (h : ¬Disjoint (g • ↑H) (f • ↑H)) : {g} * ↑H = {f} * ↑H

Two left cosets that are not disjoint must be equal.

noncomputable def HeckeRing.mulMap {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ : ↥P.Δ) (i : decompQuot P g₁ × decompQuot P g₂) : HeckeCoset P

The map sending a pair of coset representatives (σ_i, τ_j) to the double coset of their product H(σ_i τ_j)H.

Equations

• HeckeRing.mulMap P g₁ g₂ i = ⟦⟨↑(Quotient.out i.1) * ↑g₁ * (↑(Quotient.out i.2) * ↑g₂), ⋯⟩⟧

noncomputable def HeckeRing.heckeMultiplicity {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ d : ↥P.Δ) : ℤ

Shimura's multiplicity (Proposition 3.2): heckeMultiplicity(g₁, g₂, d) counts pairs (i,j) such that σᵢ τⱼ H = ξ H.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HeckeRing.mulSupport {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ : ↥P.Δ) : Finset (HeckeCoset P)

The finite set of double cosets appearing in the product D1 * D2.

Equations

• HeckeRing.mulSupport P g₁ g₂ = Finset.image (HeckeRing.mulMap P g₁ g₂) ⊤

theorem HeckeRing.doubleCoset_eq_of_rightCoset_eq {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ d : ↥P.Δ) (p : decompQuot P g₁ × decompQuot P g₂) (heq : {↑(Quotient.out p.1) * ↑g₁} * {↑(Quotient.out p.2) * ↑g₂} * ↑P.H = {↑d} * ↑P.H) : mulMap P g₁ g₂ p = ⟦d⟧

If σ_i τ_j H = ξ H then the double coset of σ_i τ_j equals that of ξ.

theorem HeckeRing.set_singleton_mul_left_cancel {G : Type u_1} [Group G] (a : G) {S T : Set G} (h : {a} * S = {a} * T) : S = T

Left multiplication by a singleton set is cancellative.

theorem HeckeRing.decompQuot_snd_eq_of_fst_eq {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ d : ↥P.Δ) (i : decompQuot P g₁) (j₁ j₂ : decompQuot P g₂) (h₁ : {↑(Quotient.out i) * ↑g₁} * {↑(Quotient.out j₁) * ↑g₂} * ↑P.H = {↑d} * ↑P.H) (h₂ : {↑(Quotient.out i) * ↑g₁} * {↑(Quotient.out j₂) * ↑g₂} * ↑P.H = {↑d} * ↑P.H) : j₁ = j₂

When the first-component representatives agree, the second-component representatives must also agree (by left-cancellation on the common prefix).

theorem HeckeRing.decompQuot_fst_eq_of_snd_mem_H {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ d : ↥P.Δ) (i₁ i₂ : decompQuot P g₁) (j : decompQuot P g₂) (hj : ↑(Quotient.out j) * ↑g₂ ∈ P.H) (h₁ : {↑(Quotient.out i₁) * ↑g₁} * {↑(Quotient.out j) * ↑g₂} * ↑P.H = {↑d} * ↑P.H) (h₂ : {↑(Quotient.out i₂) * ↑g₁} * {↑(Quotient.out j) * ↑g₂} * ↑P.H = {↑d} * ↑P.H) : i₁ = i₂

When j.out * g₂ ∈ H, the second factor collapses and first-component injectivity follows from coset disjointness.

theorem HeckeRing.heckeMultiplicity_mul_one {G : Type u_1} [Group G] (P : HeckePair G) (g₁ d : ↥P.Δ) : ⟦g₁⟧ = ⟦d⟧ ↔ heckeMultiplicity P g₁ (HeckeCoset.one P).rep d = 1

Right multiplication by HeckeCoset.one has multiplicity 1 on the diagonal and 0 elsewhere.

theorem HeckeRing.heckeMultiplicity_pos_of_mem_mulSupport {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ : ↥P.Δ) (d : HeckeCoset P) (hd : d ∈ mulSupport P g₁ g₂) : heckeMultiplicity P g₁ g₂ d.rep ≠ 0

The multiplicity heckeMultiplicity is nonzero for double cosets in the multiplication support.

theorem HeckeRing.heckeMultiplicity_eq_zero_of_nmem_mulSupport {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ : ↥P.Δ) (d : HeckeCoset P) (hd : d ∉ mulSupport P g₁ g₂) : heckeMultiplicity P g₁ g₂ d.rep = 0

The multiplicity heckeMultiplicity is zero for double cosets outside the multiplication support.

theorem HeckeRing.heckeMultiplicity_eq_one_of_le_one_and_pos {G : Type u_1} [Group G] (P : HeckePair G) (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

A multiplicity that is both at most one and positive must equal one.

theorem HeckeRing.heckeMultiplicity_pos_of_mem {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ : ↥P.Δ) (d : HeckeCoset P) (hd : d ∈ mulSupport P g₁ g₂) : 0 < heckeMultiplicity P g₁ g₂ d.rep

The multiplicity heckeMultiplicity is positive for double cosets in the multiplication support.

theorem HeckeRing.mem_mulSupport_of_product_mem {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ d : ↥P.Δ) (h₁ h₂ : ↥P.H) (hmem : ↑h₁ * ↑g₁ * (↑h₂ * ↑g₂) ∈ DoubleCoset.doubleCoset ↑d ↑P.H ↑P.H) : ⟦d⟧ ∈ mulSupport P g₁ g₂

If h₁ * g₁ * (h₂ * g₂) ∈ HdH (with h₁, h₂ ∈ H), then ⟦d⟧ ∈ mulSupport g₁ g₂. Avoids manual construction of decomposition quotient elements.

theorem HeckeRing.heckeMultiplicity_one_mul {G : Type u_1} [Group G] (P : HeckePair G) (g₁ d : ↥P.Δ) : ⟦g₁⟧ = ⟦d⟧ ↔ heckeMultiplicity P (HeckeCoset.one P).rep g₁ d = 1

Left multiplication by HeckeCoset.one has multiplicity 1 on the diagonal and 0 elsewhere.

noncomputable def HeckeRing.m {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ : ↥P.Δ) : HeckeCoset P →₀ ℤ

The multiplication finsupp: m(g₁, g₂) is the formal sum Σ_d heckeMultiplicity(g₁, g₂, d) · d encoding the product of two double cosets.

Equations

• HeckeRing.m P g₁ g₂ = { support := HeckeRing.mulSupport P g₁ g₂, toFun := fun (d : HeckeRing.HeckeCoset P) => HeckeRing.heckeMultiplicity P g₁ g₂ d.rep, mem_support_toFun := ⋯ }

@[implicit_reducible]

noncomputable instance HeckeRing.instMul𝕋Int {G : Type u_1} [Group G] (P : HeckePair G) : Mul (𝕋 P ℤ)

The multiplication on the Hecke ring, defined via the multiplicity function m.

Equations

• One or more equations did not get rendered due to their size.

theorem HeckeRing.mul_def {G : Type u_1} [Group G] (P : HeckePair G) (f g : 𝕋 P ℤ) : f * g = Finsupp.sum f fun (D1 : HeckeCoset P) (b₁ : ℤ) => Finsupp.sum g fun (D2 : HeckeCoset P) (b₂ : ℤ) => b₁ • b₂ • m P D1.rep D2.rep

Multiplication in the Hecke ring unfolds as a double Finsupp sum over multiplicities.

@[reducible, inline]

noncomputable abbrev HeckeRing.TSingle {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_3) [CommRing Z] (a : HeckeCoset P) (b : Z) : 𝕋 P Z

A basis element of the Hecke ring: TSingle D b is the formal sum b · [D].

Equations

• HeckeRing.TSingle P Z a b = Finsupp.single a b

@[reducible, inline]

noncomputable abbrev HeckeRing.HeckeLeftCosetSingle {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_3) [CommRing Z] (a : HeckeLeftCoset P) (b : Z) : HeckeModule P Z

A basis element of the Hecke module: HeckeLeftCosetSingle m b is the formal sum b · [m].

Equations

• HeckeRing.HeckeLeftCosetSingle P Z a b = Finsupp.single a b

def HeckeRing.«termT⦃_⦄» : Lean.ParserDescr

Shimura's notation: T⦃D⦄ is the basis element [HgH] in the Hecke ring, corresponding to the double coset D with coefficient 1.

Equations

• One or more equations did not get rendered due to their size.

def HeckeRing.«termT⦃_,_⦄» : Lean.ParserDescr

Shimura's notation: T⦃D, a⦄ is the element a · [HgH] in the Hecke ring.

Equations

• One or more equations did not get rendered due to their size.

theorem HeckeRing.mul_singleton_𝕋 {G : Type u_1} [Group G] (P : HeckePair G) (D1 D2 : HeckeCoset P) (a b : ℤ) : TSingle P ℤ D1 a * TSingle P ℤ D2 b = a • b • m P D1.rep D2.rep

Multiplication of two basis elements in the Hecke ring.

theorem HeckeRing.heckeMultiplicity_eq_zero_of_mulMap_unique {G : Type u_1} [Group G] (P : HeckePair G) (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₂ A.rep = 0

If all pairs under mulMap land on a single double coset D_out, then heckeMultiplicity vanishes on every other coset.

theorem HeckeRing.m_eq_single {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ : ↥P.Δ) (D_out : HeckeCoset P) (h_one : heckeMultiplicity P g₁ g₂ D_out.rep = 1) (h_zero : ∀ (A : HeckeCoset P), A ≠ D_out → heckeMultiplicity P g₁ g₂ A.rep = 0) : m P g₁ g₂ = Finsupp.single D_out 1

When heckeMultiplicity equals one on a single output coset and vanishes elsewhere, the multiplication finsupp is a singleton.

theorem HeckeRing.heckeMultiplicity_mul_one_eq_zero {G : Type u_1} [Group G] (P : HeckePair G) (g₁ : ↥P.Δ) (A : HeckeCoset P) (h : A ≠ ⟦g₁⟧) : heckeMultiplicity P g₁ (HeckeCoset.one P).rep A.rep = 0

The off-diagonal multiplicity for right multiplication by HeckeCoset.one is zero.

theorem HeckeRing.m_mul_one_eq_single {G : Type u_1} [Group G] (P : HeckePair G) (g₁ : ↥P.Δ) : m P g₁ (HeckeCoset.one P).rep = Finsupp.single ⟦g₁⟧ 1

Right multiplication by HeckeCoset.one acts as the identity: m(g₁, one.rep) = δ_{⟦g₁⟧}.

theorem HeckeRing.singleton_one_mul_𝕋 {G : Type u_1} [Group G] (P : HeckePair G) (D2 : HeckeCoset P) (b : ℤ) : TSingle P ℤ D2 b * TSingle P ℤ (HeckeCoset.one P) 1 = TSingle P ℤ D2 b

TSingle D b * TSingle (HeckeCoset.one P) 1 = TSingle D b.

theorem HeckeRing.heckeMultiplicity_one_mul_eq_zero {G : Type u_1} [Group G] (P : HeckePair G) (g₁ : ↥P.Δ) (A : HeckeCoset P) (h : A ≠ ⟦g₁⟧) : heckeMultiplicity P (HeckeCoset.one P).rep g₁ A.rep = 0

The off-diagonal multiplicity for left multiplication by HeckeCoset.one is zero.

theorem HeckeRing.m_one_mul_eq_single {G : Type u_1} [Group G] (P : HeckePair G) (g₁ : ↥P.Δ) : m P (HeckeCoset.one P).rep g₁ = Finsupp.single ⟦g₁⟧ 1

Left multiplication by HeckeCoset.one acts as the identity: m(one.rep, g₁) = δ_{⟦g₁⟧}.

theorem HeckeRing.one_mul_singleton_𝕋 {G : Type u_1} [Group G] (P : HeckePair G) (D2 : HeckeCoset P) (b : ℤ) : TSingle P ℤ (HeckeCoset.one P) 1 * TSingle P ℤ D2 b = TSingle P ℤ D2 b

TSingle (HeckeCoset.one P) 1 * TSingle D b = TSingle D b.

@[implicit_reducible]

noncomputable instance HeckeRing.instNonUnitalNonAssocSemiring {G : Type u_1} [Group G] (P : HeckePair G) : NonUnitalNonAssocSemiring (𝕋 P ℤ)

The Hecke ring is a non-unital non-associative semiring (distributivity and zero laws).

Equations

• One or more equations did not get rendered due to their size.