The action of the Hecke ring on the left-coset module

The scalar operations of LeftCosetModule (defined with the module itself) satisfy the compatibility law of Shimura, Proposition 3.4: acting by a convolution product is acting by its factors in sequence. Since HgH sends βH to Σᵢ βσᵢgH by right multiplication, this is a right action, encoded per Mathlib convention as a left action of the opposite ring (𝕋 Δ H R)ᵐᵒᵖ — so the compatibility law is mul_smul there, and the operations become a genuine Module.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/AbstractHeckeRing/Module.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), on top of the coset vocabulary vendored from the in-review mathlib4 PR #41253.

Main results

• LeftCosetModule.instModuleMulOpposite: the opposite Hecke ring acts on the left-coset module — Shimura's right action through the standard Module API.
• LeftCosetModule.instIsScalarTowerMulOpposite, LeftCosetModule.instSMulCommClassMulOpposite: the scalar operations are homogeneous in, and commute with, the coefficients.
• HeckeCoset.card_filter_smulOrbit_eq_multiplicity: Shimura's pair count, the combinatorial core of the compatibility law and the public bridge from iterated coset orbits to the Hecke ring's structure constants.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Chapter 3.

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

The scalar tower R → (𝕋 Δ H R)ᵐᵒᵖ → LeftCosetModule Δ H R: the canonical form of the R-homogeneity of the scalar operations.

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

The scalar operations of the opposite Hecke ring commute with the R-scalars: the canonical SMulCommClass form.

theorem HeckeCoset.card_filter_smulOrbit_eq_multiplicity {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] (g₁ g₂ β ξ : ↥Δ) : {i ∈ smulOrbit H g₁ β | mk ⊥ H ξ ∈ smulOrbit H g₂ i.rep}.card = DoubleCoset.multiplicity H H H (↑g₁) (↑g₂) ((↑β)⁻¹ * ↑ξ)

Shimura's pair count (the heart of Proposition 3.4): the number of cosets in the orbit of g₁ on βH whose g₂-orbit contains the coset ξH is the multiplicity of the double coset of β⁻¹ * ξ in the product Hg₁H * Hg₂H.

This is the pointwise bridge between the iterated orbit enumeration smulOrbit — the left cosets βσᵢg₁H through which the Hecke ring acts — and the pair count defining DoubleCoset.multiplicity. In particular, it is the count needed to regroup a composite of two orbit sums by its output coset.

@[instance_reducible]

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

The left-coset module is a module over the opposite Hecke ring (Shimura, Propositions 3.2 and 3.4): the scalar operations of the defining file, packaged with the unit and compatibility laws through the standard Module API.

Equations

• LeftCosetModule.instModuleMulOpposite = { toSMul := LeftCosetModule.instSMulLeftCosetModule, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }