Hecke rings: the module of left cosets

The scalar operations underlying the natural representation of the Hecke ring, following Shimura, §3.1: on the free module LeftCosetModule Δ H R over the left cosets Δ/H, each element of 𝕋 Δ H R defines a scalar operation, with a double coset HgH = ⊔ᵢ σᵢgH sending a left coset βH to Σᵢ βσᵢgH. This file constructs the left-coset presentation, the orbit Finsets, and the scalar multiplication, and proves it is additive in both arguments and faithful. Since HgH sends βH to Σᵢ βσᵢgH by right multiplication, this is right multiplication, encoded as scalar operations of the opposite ring (𝕋 Δ H R)ᵐᵒᵖ per Mathlib convention. This file provides only the scalar operations, not yet an action: Shimura's compatibility law (f * g) • m = g • (f • m) (Proposition 3.2) is exactly mul_smul for the opposite ring, and is established — turning these scalars into a genuine action — together with the degree homomorphism in the follow-up development.

Ported from the AINTLIB LeanModularForms project (HeckeRIngs/AbstractHeckeRing/Module.lean, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), per the ModularForms roadmap's dependency policy, rebuilt on the left-coset quotient of the vendored Mathlib stack.

Main definitions

• HeckeCoset.mk_bot_eq_mk_bot: the left cosets of H with a representative in Δ are the bottom-left double cosets HeckeCoset Δ ⊥ H (⊥βH = βH); this characterization makes the existing double-coset quotient serve as the left-coset quotient, with no new type.
• HeckeCoset.smulOrbit H g β: the orbit Finset {βσᵢgH} of a left coset under a double coset representative.
• the SMul (𝕋 Δ H R)ᵐᵒᵖ (LeftCosetModule Δ H R) instance — right multiplication by the Hecke ring in its opposite-ring encoding.

Main results

• HeckeCoset.smulOrbit_congr, HeckeCoset.smulOrbit_disjoint: the orbit depends only on the left coset, and orbits of distinct double cosets are disjoint.
• HeckeCoset.mk_bot_mem_smulOrbit_iff: membership in an orbit, characterized by membership in the corresponding double coset.
• LeftCosetModule.instFaithfulSMul: the scalar multiplication of the (opposite) Hecke ring on the module of left cosets is faithful.

The left cosets βH of Δ-elements are the bottom-left specialization HeckeCoset Δ ⊥ H of the double cosets: ⊥βH = βH. The type, constructor HeckeCoset.mk ⊥ H, representative HeckeCoset.rep, and induction principle are all reused from the double-coset API (they are built from the data alone); this section adds only the ⊥-specialized characterizations.

@[instance_reducible]

instance HeckeCoset.instOneBot {G : Type u_1} [Group G] (Δ : Submonoid G) {H : Subgroup G} : One (HeckeCoset Δ ⊥ H)

The identity left coset 1H = H in the bottom-left specialization.

Equations

• HeckeCoset.instOneBot Δ = { one := HeckeCoset.mk ⊥ H ⟨1, ⋯⟩ }

theorem HeckeCoset.one_bot_def {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} : 1 = mk ⊥ H ⟨1, ⋯⟩

theorem HeckeCoset.mk_bot_eq_mk_bot {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} {β₁ β₂ : ↥Δ} : mk ⊥ H β₁ = mk ⊥ H β₂ ↔ (↑β₁)⁻¹ * ↑β₂ ∈ H

In the bottom-left specialization two elements define the same class iff they differ by an element of H on the right: ⊥β₁H = ⊥β₂H ↔ β₁H = β₂H. This is the entry point through which the double-coset quotient serves as the left-coset quotient.

theorem HeckeCoset.inv_rep_mul_mem {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (β : ↥Δ) : (↑(mk ⊥ H β).rep)⁻¹ * ↑β ∈ H

The representative of the class of β differs from β by an element of H.

noncomputable def HeckeCoset.smulOrbit {G : Type u_1} [Group G] {Δ : Submonoid G} (H : Subgroup G) [IsHeckeTriple Δ H H] (g β : ↥Δ) : Finset (HeckeCoset Δ ⊥ H)

The orbit of a left coset representative β under a double coset representative g: the left cosets βσᵢgH over the decomposition HgH = ⊔ᵢ σᵢgH.

Equations

• HeckeCoset.smulOrbit H g β = Finset.image (fun (i : DoubleCoset.DecompQuotient H H ↑g) => HeckeCoset.mk ⊥ H ⟨↑β * ↑(Quotient.out i) * ↑g, ⋯⟩) Finset.univ

theorem HeckeCoset.smulOrbit_eq_image {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] (g β : ↥Δ) : smulOrbit H g β = Finset.image (fun (i : DoubleCoset.DecompQuotient H H ↑g) => mk ⊥ H ⟨↑β * ↑(Quotient.out i) * ↑g, ⋯⟩) Finset.univ

The orbit as an explicit image: the defining equation, exported for consumers that count over the enumeration.

@[simp]

theorem HeckeCoset.mem_smulOrbit {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {g β : ↥Δ} {x : HeckeCoset Δ ⊥ H} : x ∈ smulOrbit H g β ↔ ∃ (i : DoubleCoset.DecompQuotient H H ↑g), mk ⊥ H ⟨↑β * ↑(Quotient.out i) * ↑g, ⋯⟩ = x

Membership in the orbit: the left cosets of the products β · σᵢ · g over the decomposition representatives.

theorem HeckeCoset.mk_bot_mem_smulOrbit_iff {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {g w ξ : ↥Δ} : mk ⊥ H ξ ∈ smulOrbit H g w ↔ (↑w)⁻¹ * ↑ξ ∈ DoubleCoset.doubleCoset ↑g ↑H ↑H

Membership in an orbit, tested at an arbitrary representative: the left coset ξH lies in the orbit of g on wH iff w⁻¹ * ξ lies in the double coset HgH.

theorem HeckeCoset.smulOrbit_nonempty {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] (g β : ↥Δ) : (smulOrbit H g β).Nonempty

theorem HeckeCoset.smulOrbit_congr {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] (g : ↥Δ) {β₁ β₂ : ↥Δ} (h : mk ⊥ H β₁ = mk ⊥ H β₂) : smulOrbit H g β₁ = smulOrbit H g β₂

The orbit depends on β only through its left coset.

theorem HeckeCoset.smulOrbit_congr_left {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] (β : ↥Δ) {g₁ g₂ : ↥Δ} (h : mk H H g₁ = mk H H g₂) : smulOrbit H g₁ β = smulOrbit H g₂ β

The orbit is invariant in the acting double-coset representative: representatives of the same double coset produce the same orbit.

theorem HeckeCoset.smulOrbit_map_injective {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] (g β : ↥Δ) : Function.Injective fun (i : DoubleCoset.DecompQuotient H H ↑g) => mk ⊥ H ⟨↑β * ↑(Quotient.out i) * ↑g, ⋯⟩

The orbit enumeration is injective: distinct decomposition classes give distinct left cosets.

theorem HeckeCoset.smulOrbit_card {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] (g β : ↥Δ) : (smulOrbit H g β).card = Fintype.card (DoubleCoset.DecompQuotient H H ↑g)

The orbit of a left coset under g has exactly as many elements as the decomposition HgH = ⊔ᵢ σᵢgH: the map i ↦ βσᵢgH is injective.

theorem HeckeCoset.smulOrbit_disjoint {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {g₁ g₂ : ↥Δ} (β : ↥Δ) (hne : mk H H g₁ ≠ mk H H g₂) : Disjoint (smulOrbit H g₁ β) (smulOrbit H g₂ β)

Orbits of representatives of distinct double cosets on a common left coset are disjoint.

@[reducible, inline]

abbrev LeftCosetModule {G : Type u_1} [Group G] (Δ : Submonoid G) (H : Subgroup G) (R : Type u_2) [Zero R] : Type (max u_1 u_2)

The left-coset module: the free R-module on the left cosets Δ/H (the bottom-left Hecke cosets), the carrier of the natural representation of the Hecke ring. An abbrev of the underlying Finsupp, so the full Finsupp API applies transparently at every coefficient class — the stable named interface for the scalar operations below.

Equations

• LeftCosetModule Δ H R = (HeckeCoset Δ ⊥ H →₀ R)

@[instance_reducible]

noncomputable instance LeftCosetModule.instSMulLeftCosetModule {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [NonUnitalNonAssocSemiring R] : SMul (HeckeRing Δ H R)ᵐᵒᵖ (LeftCosetModule Δ H R)

The scalar multiplication of the Hecke ring on the free module of left cosets: a double coset scales a left coset by summing over its orbit, extended biadditively. Since HgH sends βH to the cosets βσᵢgH by right multiplication, the scalars come from the opposite ring (𝕋 Δ H R)ᵐᵒᵖ, per Mathlib convention. Shimura's compatibility (f * g) • m = g • (f • m) — precisely mul_smul for the opposite ring, which upgrades these scalar operations to an action — is proved with the degree homomorphism in the follow-up development.

Equations

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

theorem LeftCosetModule.smul_eq_sum {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [NonUnitalNonAssocSemiring R] (t : HeckeRing Δ H R) (m : LeftCosetModule Δ H R) : MulOpposite.op t • m = Finsupp.sum t fun (D : HeckeCoset Δ H H) (b₁ : R) => Finsupp.sum m fun (q : HeckeCoset Δ ⊥ H) (b₂ : R) => ∑ i ∈ HeckeCoset.smulOrbit H D.rep q.rep, Finsupp.single i (b₂ * b₁)

The defining formula of the scalar multiplication.

@[simp]

theorem LeftCosetModule.single_smul_single {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [NonUnitalNonAssocSemiring R] (D : HeckeCoset Δ H H) (q : HeckeCoset Δ ⊥ H) (a b : R) : MulOpposite.op (HeckeCosetModule.single R D a) • Finsupp.single q b = ∑ i ∈ HeckeCoset.smulOrbit H D.rep q.rep, Finsupp.single i (b * a)

A basis element of the Hecke ring scales a basis element of the module into its orbit sum.

@[simp]

theorem LeftCosetModule.add_smul {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [NonUnitalNonAssocSemiring R] (t₁ t₂ : (HeckeRing Δ H R)ᵐᵒᵖ) (m : LeftCosetModule Δ H R) : (t₁ + t₂) • m = t₁ • m + t₂ • m

The scalar multiplication is additive in the (opposite) Hecke-ring argument.

@[instance_reducible]

noncomputable instance LeftCosetModule.distribSMul {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [NonUnitalNonAssocSemiring R] : DistribSMul (HeckeRing Δ H R)ᵐᵒᵖ (LeftCosetModule Δ H R)

The scalar operations distribute over the module's addition, packaged as the DistribSMul typeclass (the strongest action class available before the compatibility law with the convolution product); the generic smul_zero/smul_add supersede ad-hoc laws.

Equations

• LeftCosetModule.distribSMul = { toSMul := LeftCosetModule.instSMulLeftCosetModule, smul_zero := ⋯, smul_add := ⋯ }

@[instance_reducible]

noncomputable instance LeftCosetModule.smulWithZero {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [NonUnitalNonAssocSemiring R] : SMulWithZero (HeckeRing Δ H R)ᵐᵒᵖ (LeftCosetModule Δ H R)

Zero acts as zero and acting on zero gives zero: the SMulWithZero typeclass.

Equations

• LeftCosetModule.smulWithZero = { toSMul := LeftCosetModule.instSMulLeftCosetModule, smul_zero := ⋯, zero_smul := ⋯ }

theorem LeftCosetModule.eq_of_smul_eq_smul {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [NonAssocSemiring R] {t₁ t₂ : HeckeRing Δ H R} (h : ∀ (m : LeftCosetModule Δ H R), MulOpposite.op t₁ • m = MulOpposite.op t₂ • m) : t₁ = t₂

The scalar multiplication of the Hecke ring on the module of left cosets is faithful.

instance LeftCosetModule.instFaithfulSMul {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [NonAssocSemiring R] : FaithfulSMul (HeckeRing Δ H R)ᵐᵒᵖ (LeftCosetModule Δ H R)

The scalar operations of the opposite Hecke ring on the left-coset module are faithful, as an instance.