Hecke rings: the identity and the unital non-associative semiring

The identity double coset (1 : HeckeCoset Δ H H) gives the multiplicative identity of the Hecke ring 𝕋 Δ H R, following Shimura, Chapter 3. This file proves that the structure constants collapse to a single basis element on convolution by the identity, deduces the unit laws 1 * f = f and f * 1 = f of the convolution product of Hecke coset modules (where the two identities live at the two different levels), and assembles the NonAssocSemiring (𝕋 Δ H R) instance.

Vendored from the in-review mathlib4 PR #41279 (Chris Birkbeck), per the ModularForms roadmap's dependency policy; migrate to Mathlib and delete this file when that stack merges.

Main results

• HeckeCosetModule.one_def: (1 : 𝕋 Δ H R) = single R 1 1.
• HeckeCosetModule.one_mul, HeckeCosetModule.mul_one: the identities of the diagonal Hecke rings are one-sided units for the convolution product of Hecke coset modules.
• the NonAssocSemiring (𝕋 Δ H R) instance.

theorem HeckeCosetModule.multiplicity_one_right_eq_zero {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] (g : ↥Δ) {A : HeckeCoset Δ H₁ H₂} (hA : A ≠ HeckeCoset.mk H₁ H₂ g) : DoubleCoset.multiplicity H₁ H₂ H₂ ↑g ↑(HeckeCoset.rep 1) ↑A.rep = 0

The multiplicity for right convolution by the identity double coset vanishes off the diagonal.

theorem HeckeCosetModule.multiplicity_one_left_eq_zero {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} [IsHeckeTriple Δ H₁ H₁] (g : ↥Δ) {A : HeckeCoset Δ H₁ H₂} (hA : A ≠ HeckeCoset.mk H₁ H₂ g) : DoubleCoset.multiplicity H₁ H₁ H₂ ↑(HeckeCoset.rep 1) ↑g ↑A.rep = 0

The multiplicity for left convolution by the identity double coset vanishes off the diagonal.

theorem HeckeCosetModule.structureConstants_one_right {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} (R : Type u_2) [Semiring R] [IsHeckeTriple Δ H₁ H₂] [IsHeckeTriple Δ H₂ H₂] (g : ↥Δ) : structureConstants R H₁ H₂ H₂ g (HeckeCoset.rep 1) = single R (HeckeCoset.mk H₁ H₂ g) 1

The structure constants for right convolution by the identity double coset collapse to a single basis element.

theorem HeckeCosetModule.structureConstants_one_left {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} (R : Type u_2) [Semiring R] [IsHeckeTriple Δ H₁ H₁] [IsHeckeTriple Δ H₁ H₂] (g : ↥Δ) : structureConstants R H₁ H₁ H₂ (HeckeCoset.rep 1) g = single R (HeckeCoset.mk H₁ H₂ g) 1

The structure constants for left convolution by the identity double coset collapse to a single basis element.

@[instance_reducible]

noncomputable instance HeckeCosetModule.instOneHeckeRing {G : Type u_1} [Group G] {Δ : Submonoid G} (R : Type u_2) [Semiring R] {H : Subgroup G} : One (HeckeRing Δ H R)

The multiplicative identity of the Hecke ring is the basis element of the identity double coset.

Equations

• HeckeCosetModule.instOneHeckeRing R = { one := HeckeCosetModule.single R 1 1 }

theorem HeckeCosetModule.one_def {G : Type u_1} [Group G] {Δ : Submonoid G} (R : Type u_2) [Semiring R] {H : Subgroup G} : 1 = single R 1 1

The unit of the Hecke ring is the basis element of the identity double coset.

@[simp]

theorem HeckeCosetModule.one_mul {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} (R : Type u_2) [Semiring R] [IsHeckeTriple Δ H₁ H₁] [IsHeckeTriple Δ H₁ H₂] (f : HeckeCosetModule Δ H₁ H₂ R) : mul R 1 f = f

The identity of the Hecke ring at the left level is a left unit for the convolution product of Hecke coset modules.

@[simp]

theorem HeckeCosetModule.mul_one {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} (R : Type u_2) [Semiring R] [IsHeckeTriple Δ H₁ H₂] [IsHeckeTriple Δ H₂ H₂] (f : HeckeCosetModule Δ H₁ H₂ R) : mul R f 1 = f

The identity of the Hecke ring at the right level is a right unit for the convolution product of Hecke coset modules.

@[instance_reducible]

noncomputable instance HeckeCosetModule.instNonAssocSemiringHeckeRing {G : Type u_1} [Group G] {Δ : Submonoid G} (R : Type u_2) [Semiring R] {H : Subgroup G} [IsHeckeTriple Δ H H] : NonAssocSemiring (HeckeRing Δ H R)

The Hecke ring is a non-associative semiring: the identity double coset is a two-sided identity.

Equations

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