Hecke rings: the multiplicity of the identity double coset

For e ∈ Γ₂ the double coset Γ₂eΓ₂ is Γ₂ itself, the identity of the Hecke ring of Γ₂; this file proves the two computations expressing this at the level of Shimura's multiplicity: multiplying by such an e on either side, the multiplicity is 1 exactly on the diagonal Γ₁gΓ₂ = Γ₁dΓ₂. Specialised to a Hecke coset module, these compute the products T(g) * T(1) and T(1) * T(g) in later files.

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

Main results

• DoubleCoset.multiplicity_eq_one_iff_of_mem_right: for e ∈ Γ₂, multiplicity Γ₁ Γ₂ Γ₂ g e d = 1 ↔ Γ₁gΓ₂ = Γ₁dΓ₂.
• DoubleCoset.multiplicity_eq_one_iff_of_mem_left: for e ∈ Γ₁, multiplicity Γ₁ Γ₁ Γ₂ e g d = 1 ↔ Γ₁gΓ₂ = Γ₁dΓ₂.

theorem DoubleCoset.multiplicity_eq_one_iff_of_mem_right {G : Type u_1} [Group G] {Γ₁ Γ₂ : Subgroup G} {g e d : G} (he : e ∈ Γ₂) : multiplicity Γ₁ Γ₂ Γ₂ g e d = 1 ↔ doubleCoset g ↑Γ₁ ↑Γ₂ = doubleCoset d ↑Γ₁ ↑Γ₂

For e ∈ Γ₂, right multiplication by the identity double coset Γ₂eΓ₂ = Γ₂ has multiplicity 1 exactly on the diagonal.

theorem DoubleCoset.multiplicity_eq_one_iff_of_mem_left {G : Type u_1} [Group G] {Γ₁ Γ₂ : Subgroup G} {e g d : G} (he : e ∈ Γ₁) : multiplicity Γ₁ Γ₁ Γ₂ e g d = 1 ↔ doubleCoset g ↑Γ₁ ↑Γ₂ = doubleCoset d ↑Γ₁ ↑Γ₂

For e ∈ Γ₁, left multiplication by the identity double coset Γ₁eΓ₁ = Γ₁ has multiplicity 1 exactly on the diagonal.

theorem HeckeCoset.mulMapOf_one_right {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} (h₁ : H₁.toSubmonoid ≤ Δ) (h₂ : H₂.toSubmonoid ≤ Δ) (g₁ : ↥Δ) (p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₂ ↑(rep 1)) : mulMapOf h₁ h₂ H₂ g₁ (rep 1) p = mk H₁ H₂ g₁

Every pair of representatives multiplies into mk H₁ H₂ g₁ when the second double coset is the identity, from bare containments.

@[simp]

theorem HeckeCoset.mulMap_one_right {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] (g₁ : ↥Δ) (p : DoubleCoset.DecompQuotient H₁ H₂ ↑g₁ × DoubleCoset.DecompQuotient H₂ H₂ ↑(rep 1)) : mulMap H₁ H₂ H₂ g₁ (rep 1) p = mk H₁ H₂ g₁

Every pair of representatives multiplies into mk H₁ H₂ g₁ when the second double coset is the identity.

theorem HeckeCoset.mulMapOf_one_left {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} (h₁ : H₁.toSubmonoid ≤ Δ) (g₁ : ↥Δ) (p : DoubleCoset.DecompQuotient H₁ H₁ ↑(rep 1) × DoubleCoset.DecompQuotient H₁ H₂ ↑g₁) : mulMapOf h₁ h₁ H₂ (rep 1) g₁ p = mk H₁ H₂ g₁

Every pair of representatives multiplies into mk H₁ H₂ g₁ when the first double coset is the identity, from bare containments.

@[simp]

theorem HeckeCoset.mulMap_one_left {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} [IsHeckeTriple Δ H₁ H₁] (g₁ : ↥Δ) (p : DoubleCoset.DecompQuotient H₁ H₁ ↑(rep 1) × DoubleCoset.DecompQuotient H₁ H₂ ↑g₁) : mulMap H₁ H₁ H₂ (rep 1) g₁ p = mk H₁ H₂ g₁

Every pair of representatives multiplies into mk H₁ H₂ g₁ when the first double coset is the identity.

@[simp]

theorem HeckeCoset.multiplicity_mul_one {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} (g d : ↥Δ) : DoubleCoset.multiplicity H₁ H₂ H₂ ↑g ↑(rep 1) ↑d = 1 ↔ mk H₁ H₂ g = mk H₁ H₂ d

Right multiplication by the identity double coset has multiplicity 1 exactly on the diagonal.

@[simp]

theorem HeckeCoset.multiplicity_one_mul {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} (g d : ↥Δ) : DoubleCoset.multiplicity H₁ H₁ H₂ ↑(rep 1) ↑g ↑d = 1 ↔ mk H₁ H₂ g = mk H₁ H₂ d

Left multiplication by the identity double coset has multiplicity 1 exactly on the diagonal.