Hecke Rings: Ring Instance and API

The Ring (𝕋 P ℤ) instance and user-facing API lemmas for working with Hecke rings.

theorem HeckeRing.mul_assoc_𝕋 {G : Type u_1} [Group G] (P : HeckePair G) (f g h : 𝕋 P ℤ) : f * g * h = f * (g * h)

Associativity of multiplication in the Hecke ring, deduced from IsScalarTower and faithfulness of the module action.

@[implicit_reducible]

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

The Hecke ring is a non-unital semiring (associativity + distributivity).

Equations

• HeckeRing.instNonUnitalSemiring P = { toNonUnitalNonAssocSemiring := HeckeRing.instNonUnitalNonAssocSemiring P, mul_assoc := ⋯ }

@[implicit_reducible]

noncomputable instance HeckeRing.instOne𝕋 {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] : One (𝕋 P Z)

The multiplicative identity of the Hecke ring is TSingle (HeckeCoset.one P) 1.

Equations

• HeckeRing.instOne𝕋 P Z = { one := HeckeRing.TSingle P Z (HeckeRing.HeckeCoset.one P) 1 }

theorem HeckeRing.one_def {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] : 1 = TSingle P Z (HeckeCoset.one P) 1

The one element of the Hecke ring unfolds to TSingle (HeckeCoset.one P) 1.

@[implicit_reducible]

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

The Hecke ring is a non-associative semiring (one is a two-sided identity).

Equations

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

@[implicit_reducible]

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

The Hecke ring is a semiring.

Equations

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

@[implicit_reducible]

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

The Hecke ring is a non-associative ring (semiring + additive inverses).

Equations

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

@[implicit_reducible]

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

The Hecke ring 𝕋 P ℤ is a ring.

Equations

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

Algebra compatibility lemmas

In mathlib v4.29, Finsupp gains pointwise multiplication instances that conflict with the Hecke ring's custom convolution multiplication. The lemmas below use the Hecke Ring instance explicitly so that rw can match the custom Mul.

theorem HeckeRing.mul_sub {G : Type u_1} [Group G] (P : HeckePair G) (a b c : 𝕋 P ℤ) : a * (b - c) = a * b - a * c

theorem HeckeRing.sub_mul {G : Type u_1} [Group G] (P : HeckePair G) (a b c : 𝕋 P ℤ) : (a - b) * c = a * c - b * c

theorem HeckeRing.mul_assoc {G : Type u_1} [Group G] (P : HeckePair G) (a b c : 𝕋 P ℤ) : a * b * c = a * (b * c)

theorem HeckeRing.mul_add {G : Type u_1} [Group G] (P : HeckePair G) (a b c : 𝕋 P ℤ) : a * (b + c) = a * b + a * c

theorem HeckeRing.add_mul {G : Type u_1} [Group G] (P : HeckePair G) (a b c : 𝕋 P ℤ) : (a + b) * c = a * c + b * c

theorem HeckeRing.pow_succ {G : Type u_1} [Group G] (P : HeckePair G) (a : 𝕋 P ℤ) (n : ℕ) : a ^ (n + 1) = a ^ n * a

theorem HeckeRing.pow_succ' {G : Type u_1} [Group G] (P : HeckePair G) (a : 𝕋 P ℤ) (n : ℕ) : a ^ (n + 1) = a * a ^ n

theorem HeckeRing.T_single_zero {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) : TSingle P ℤ D 0 = 0

A basis element with coefficient zero is zero.

theorem HeckeRing.T_single_add {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) (a b : ℤ) : TSingle P ℤ D a + TSingle P ℤ D b = TSingle P ℤ D (a + b)

Addition of two basis elements with the same double coset.

theorem HeckeRing.T_single_neg {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) (a : ℤ) : -TSingle P ℤ D a = TSingle P ℤ D (-a)

Negation of a basis element.

theorem HeckeRing.T_single_sub {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) (a b : ℤ) : TSingle P ℤ D a - TSingle P ℤ D b = TSingle P ℤ D (a - b)

Subtraction of two basis elements with the same double coset.

theorem HeckeRing.T_single_smul {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) (n a : ℤ) : n • TSingle P ℤ D a = TSingle P ℤ D (n * a)

Scalar multiplication on a basis element.

@[simp]

theorem HeckeRing.intCast_eq {G : Type u_1} [Group G] (P : HeckePair G) (n : ℤ) : ↑n = TSingle P ℤ (HeckeCoset.one P) n

The integer cast into the Hecke ring lands on the identity double coset.

theorem HeckeRing.T_single_mul_T_single {G : Type u_1} [Group G] (P : HeckePair G) (D₁ D₂ : HeckeCoset P) (a b : ℤ) : TSingle P ℤ D₁ a * TSingle P ℤ D₂ b = a • b • m P D₁.rep D₂.rep

The product of two basis elements equals the scaled multiplication finsupp.

@[simp]

theorem HeckeRing.T_single_one_mul_T_single_one {G : Type u_1} [Group G] (P : HeckePair G) (D₁ D₂ : HeckeCoset P) : TSingle P ℤ D₁ 1 * TSingle P ℤ D₂ 1 = m P D₁.rep D₂.rep

The product of two unit-coefficient basis elements is the multiplication finsupp.

theorem HeckeRing.T_single_mul_one {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) (a : ℤ) : TSingle P ℤ D a * 1 = TSingle P ℤ D a

Right multiplication by 1 is the identity.

theorem HeckeRing.one_mul_T_single {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) (a : ℤ) : 1 * TSingle P ℤ D a = TSingle P ℤ D a

Left multiplication by 1 is the identity.

theorem HeckeRing.T_single_one_mul_eq_single {G : Type u_1} [Group G] (P : HeckePair G) (D₁ D₂ D_out : HeckeCoset P) (h_one : heckeMultiplicity P D₁.rep D₂.rep D_out.rep = 1) (h_zero : ∀ (A : HeckeCoset P), A ≠ D_out → heckeMultiplicity P D₁.rep D₂.rep A.rep = 0) : TSingle P ℤ D₁ 1 * TSingle P ℤ D₂ 1 = TSingle P ℤ D_out 1

When heckeMultiplicity is one on a single output and zero elsewhere, multiplication of unit-coefficient basis elements produces a single basis element.

@[simp]

theorem HeckeRing.m_apply {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ : ↥P.Δ) (D : HeckeCoset P) : (m P g₁ g₂) D = heckeMultiplicity P g₁ g₂ D.rep

Evaluating the multiplication finsupp at a double coset gives heckeMultiplicity.

@[simp]

theorem HeckeRing.m_mul_T_one {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) : m P D.rep (HeckeCoset.one P).rep = Finsupp.single ⟦D.rep⟧ 1

Right multiplication by HeckeCoset.one is the identity on m.

@[simp]

theorem HeckeRing.m_T_one_mul {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) : m P (HeckeCoset.one P).rep D.rep = Finsupp.single ⟦D.rep⟧ 1

Left multiplication by HeckeCoset.one is the identity on m.

theorem HeckeRing.m_support {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ : ↥P.Δ) : (m P g₁ g₂).support = mulSupport P g₁ g₂

The support of the multiplication finsupp equals mulSupport.

theorem HeckeRing.heckeMultiplicity_nonneg {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ d : ↥P.Δ) : 0 ≤ heckeMultiplicity P g₁ g₂ d

The multiplicity heckeMultiplicity is nonneg since it is a natural number cast to ℤ.

theorem HeckeRing.ext_𝕋 {G : Type u_1} [Group G] (P : HeckePair G) {f g : 𝕋 P ℤ} (h : ∀ (D : HeckeCoset P), f.toFun D = g.toFun D) : f = g

Extensionality for Hecke ring elements.

theorem HeckeRing.ext_𝕋_iff {G : Type u_1} [Group G] {P : HeckePair G} {f g : 𝕋 P ℤ} : f = g ↔ ∀ (D : HeckeCoset P), f.toFun D = g.toFun D

theorem HeckeRing.induction_on_𝕋 {G : Type u_1} [Group G] (P : HeckePair G) {C : 𝕋 P ℤ → Prop} (f : 𝕋 P ℤ) (h_zero : C 0) (h_add : ∀ (D : HeckeCoset P) (a : ℤ) (g : 𝕋 P ℤ), D ∉ g.support → a ≠ 0 → C g → C (TSingle P ℤ D a + g)) : C f

Induction principle for Hecke ring elements (basis + accumulation).

theorem HeckeRing.induction_linear_𝕋 {G : Type u_1} [Group G] (P : HeckePair G) {C : 𝕋 P ℤ → Prop} (f : 𝕋 P ℤ) (h_zero : C 0) (h_single : ∀ (D : HeckeCoset P) (a : ℤ), C (TSingle P ℤ D a)) (h_add : ∀ (f g : 𝕋 P ℤ), C f → C g → C (f + g)) : C f

Linear induction principle: reduce to zero, single basis elements, and sums.

theorem HeckeRing.sum_single_𝕋 {G : Type u_1} [Group G] (P : HeckePair G) (f : 𝕋 P ℤ) : f = ∑ D ∈ f.support, TSingle P ℤ D (f.toFun D)

Every Hecke ring element is a finite sum of basis elements.

theorem HeckeRing.T_single_smul_HeckeLeftCoset_single {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] (D : HeckeCoset P) (m₀ : HeckeLeftCoset P) (a b : Z) : TSingle P Z D a • HeckeLeftCosetSingle P Z m₀ b = ∑ i ∈ smulOrbit P D.rep m₀.rep, HeckeLeftCosetSingle P Z i (a * b)

The action of a basis Hecke element on a basis module element as a sum over orbits.