Hecke rings: the degree homomorphism

The degree of a double coset HgH = ⊔ᵢ σᵢgH is the number of left cosets in its decomposition, deg(HgH) = [H : H ∩ gHg⁻¹]. Extended linearly it gives the degree homomorphism deg : 𝕋 Δ H R →+* R of the Hecke ring (Proposition 3.3 of Shimura). Multiplicativity is proved through the module of left cosets: deg f is the coefficient sum of f • [H], and the action satisfies the compatibility law op (f * g) • m = op g • (op f • m) — mul_smul of the opposite ring (Proposition 3.4) — so the coefficient sum multiplies.

Ported from the AINTLIB LeanModularForms project (HeckeRIngs/AbstractHeckeRing/Degree.lean and the compatibility law of HeckeRIngs/AbstractHeckeRing/Associativity.lean, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), per the ModularForms roadmap's dependency policy. The compatibility law is proved as a private lemma and exposed through the public Module (𝕋 Δ H R)ᵐᵒᵖ instance, rather than through AINTLIB's reversed scalar action.

Main definitions

• LeftCosetModule.deg: the degree homomorphism 𝕋 Δ H R →+* R over any semiring of coefficients, built on Mathlib's coefficient sum Finsupp.degree of the left-coset module.

Main results

• LeftCosetModule.degree_single_smul_single, LeftCosetModule.degree_smul: the coefficient sum against the scalar operations — the bridge to the degree.
• LeftCosetModule.degree_smul_eq_deg: the same law with the named degree on the right.
• LeftCosetModule.deg_single, RingHom laws of deg: Proposition 3.3.

theorem LeftCosetModule.degree_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) : Finsupp.degree (MulOpposite.op (HeckeCosetModule.single R D a) • Finsupp.single q b) = D.degree • (b * a)

The coefficient sum of the action of a ring basis element on a module basis element: the degree of the double coset appears as the orbit size. Only the additive structure and the single product b * a are involved, so no unit or associativity is needed.

theorem LeftCosetModule.degree_smul {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [Semiring R] (t : HeckeRing Δ H R) (m : LeftCosetModule Δ H R) : Finsupp.degree (MulOpposite.op t • m) = Finsupp.degree m * Finsupp.degree (MulOpposite.op t • Finsupp.single 1 1)

The coefficient sum is multiplicative against the action: the orbit-sum coefficient is independent of the acted-on coset, so the action factors through the degree.

noncomputable def LeftCosetModule.deg {G : Type u_1} [Group G] (Δ : Submonoid G) (H : Subgroup G) [IsHeckeTriple Δ H H] (R : Type u_2) [Semiring R] : HeckeRing Δ H R →+* R

The degree homomorphism (Shimura, Proposition 3.3): the coefficient sum of the action on the identity coset, as a ring homomorphism 𝕋 Δ H R →+* R. On a basis element it is the degree of the double coset — the number of left cosets in its decomposition — scaled by the coefficient; multiplicativity is the compatibility law mul_smul'.

Equations

• LeftCosetModule.deg Δ H R = { toFun := fun (t : HeckeRing Δ H R) => Finsupp.degree (MulOpposite.op t • Finsupp.single 1 1), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem LeftCosetModule.deg_apply {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [Semiring R] (t : HeckeRing Δ H R) : (deg Δ H R) t = Finsupp.degree (MulOpposite.op t • Finsupp.single 1 1)

The defining equation of deg.

theorem LeftCosetModule.degree_smul_eq_deg {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [Semiring R] (t : HeckeRing Δ H R) (m : LeftCosetModule Δ H R) : Finsupp.degree (MulOpposite.op t • m) = Finsupp.degree m * (deg Δ H R) t

degree_smul in terms of deg: acting by t multiplies the coefficient sum by deg t. This is the form consumers want — degree_smul leaves the right-hand factor as the unfolded action on the identity coset.

@[simp]

theorem LeftCosetModule.deg_single {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} [IsHeckeTriple Δ H H] {R : Type u_2} [Semiring R] (D : HeckeCoset Δ H H) (a : R) : (deg Δ H R) (HeckeCosetModule.single R D a) = D.degree • a

The degree of a basis element: the degree of its double coset, scaled by the coefficient.