Hecke Rings: Degree Map

The degree ring homomorphism deg : 𝕋 P ℤ →+* ℤ, which sends each double coset HgH to the number of left cosets it contains: deg(HgH) = [H : H ∩ gHg⁻¹].

This is Shimura §3.1, Proposition 3.3.

Main definitions

• HeckeCosetDeg P D : the degree of a single double coset
• deg P : the degree ring homomorphism 𝕋 P ℤ →+* ℤ

Main results

• deg_T_single : deg(TSingle D a) = a * HeckeCosetDeg D
• HeckeCoset_deg_pos : 0 < HeckeCosetDeg D
• deg_one : deg 1 = 1

Proof strategy

Multiplicativity deg(f * g) = deg(f) * deg(g) is proved using the module action on HeckeModule P ℤ. We show deg(f) = coeffSum(f • 1) where coeffSum sums all coefficients, and then use IsScalarTower (Shimura Prop 3.4) to get (f * g) • 1 = g • (f • 1). The key intermediate result is coeffSum(f • m) = deg(f) * coeffSum(m), which follows from the orbit cardinality lemma smulOrbit_card.

noncomputable def HeckeRing.HeckeCosetDeg {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) : ℤ

The degree of a double coset: deg(HgH) = [H : H ∩ gHg⁻¹], the number of left cosets in the decomposition of HgH.

Equations

• HeckeRing.HeckeCosetDeg P D = ↑(Fintype.card (HeckeRing.decompQuot P D.rep))

@[simp]

theorem HeckeRing.HeckeCoset_deg_T_one {G : Type u_1} [Group G] (P : HeckePair G) : HeckeCosetDeg P (HeckeCoset.one P) = 1

The degree of the identity double coset is 1.

theorem HeckeRing.HeckeCoset_deg_pos {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) : 0 < HeckeCosetDeg P D

Every double coset has positive degree.

theorem HeckeRing.smulOrbit_card {G : Type u_1} [Group G] (P : HeckePair G) (g β : ↥P.Δ) : (smulOrbit P g β).card = Fintype.card (decompQuot P g)

The cardinality of a smul orbit equals the degree of the acting double coset.

theorem HeckeRing.smulOrbit_card_intCast {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) (β : ↥P.Δ) : ↑(smulOrbit P D.rep β).card = HeckeCosetDeg P D

The cardinality of a smul orbit cast to ℤ equals HeckeCosetDeg.

noncomputable def HeckeRing.coeffSum {G : Type u_1} [Group G] (P : HeckePair G) : HeckeModule P ℤ →+ ℤ

The coefficient sum homomorphism: sums all coefficients of a formal linear combination of left cosets.

Equations

• HeckeRing.coeffSum P = Finsupp.liftAddHom fun (x : HeckeRing.HeckeLeftCoset P) => AddMonoidHom.id ℤ

@[simp]

theorem HeckeRing.coeffSum_single {G : Type u_1} [Group G] (P : HeckePair G) (m₀ : HeckeLeftCoset P) (b : ℤ) : (coeffSum P) (HeckeLeftCosetSingle P ℤ m₀ b) = b

The coefficient sum of a single basis element is its coefficient.

theorem HeckeRing.coeffSum_zero {G : Type u_1} [Group G] (P : HeckePair G) : (coeffSum P) 0 = 0

The coefficient sum of zero is zero.

theorem HeckeRing.coeffSum_add {G : Type u_1} [Group G] (P : HeckePair G) (m₁ m₂ : HeckeModule P ℤ) : (coeffSum P) (m₁ + m₂) = (coeffSum P) m₁ + (coeffSum P) m₂

The coefficient sum is additive.

theorem HeckeRing.coeffSum_finset_sum {G : Type u_1} [Group G] (P : HeckePair G) {ι : Type u_2} (s : Finset ι) (f : ι → HeckeModule P ℤ) : (coeffSum P) (∑ i ∈ s, f i) = ∑ i ∈ s, (coeffSum P) (f i)

The coefficient sum distributes over finite sums.

theorem HeckeRing.coeffSum_single_smul_single {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) (m₀ : HeckeLeftCoset P) (a b : ℤ) : (coeffSum P) (TSingle P ℤ D a • HeckeLeftCosetSingle P ℤ m₀ b) = a * HeckeCosetDeg P D * b

The coefficient sum of a single-single smul product equals a * deg(D) * b.

noncomputable def HeckeRing.degFun {G : Type u_1} [Group G] (P : HeckePair G) (f : 𝕋 P ℤ) : ℤ

The underlying function of the degree map: Σ_D a_D * deg(D).

Equations

• HeckeRing.degFun P f = Finsupp.sum f fun (D : HeckeRing.HeckeCoset P) (a : ℤ) => a * HeckeRing.HeckeCosetDeg P D

@[simp]

theorem HeckeRing.deg_fun_zero {G : Type u_1} [Group G] (P : HeckePair G) : degFun P 0 = 0

The degree function of zero is zero.

@[simp]

theorem HeckeRing.deg_fun_T_single {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) (a : ℤ) : degFun P (TSingle P ℤ D a) = a * HeckeCosetDeg P D

The degree function of a basis element is a * deg(D).

theorem HeckeRing.deg_fun_add {G : Type u_1} [Group G] (P : HeckePair G) (f g : 𝕋 P ℤ) : degFun P (f + g) = degFun P f + degFun P g

The degree function is additive.

@[simp]

theorem HeckeRing.deg_fun_one {G : Type u_1} [Group G] (P : HeckePair G) : degFun P 1 = 1

The degree function of the identity is 1.

theorem HeckeRing.deg_fun_eq_coeffSum_smul_one {G : Type u_1} [Group G] (P : HeckePair G) (f : 𝕋 P ℤ) : degFun P f = (coeffSum P) (f • 1)

The degree equals the coefficient sum of the action on the identity module element.

theorem HeckeRing.coeffSum_smul_eq {G : Type u_1} [Group G] (P : HeckePair G) (f : 𝕋 P ℤ) (m : HeckeModule P ℤ) : (coeffSum P) (f • m) = degFun P f * (coeffSum P) m

The coefficient sum of a smul product factors as deg(f) * coeffSum(m).

theorem HeckeRing.deg_fun_mul {G : Type u_1} [Group G] (P : HeckePair G) (f g : 𝕋 P ℤ) : degFun P (f * g) = degFun P f * degFun P g

The degree function is multiplicative.

noncomputable def HeckeRing.deg {G : Type u_1} [Group G] (P : HeckePair G) : 𝕋 P ℤ →+* ℤ

The degree ring homomorphism deg : 𝕋 P ℤ →+* ℤ, sending each double coset to the number of left cosets it contains (Shimura Proposition 3.3).

Equations

• HeckeRing.deg P = { toFun := HeckeRing.degFun P, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem HeckeRing.deg_T_single {G : Type u_1} [Group G] (P : HeckePair G) (D : HeckeCoset P) (a : ℤ) : (deg P) (TSingle P ℤ D a) = a * HeckeCosetDeg P D

The degree of a basis element is the coefficient times the degree of the double coset.

@[simp]

theorem HeckeRing.deg_one_val {G : Type u_1} [Group G] (P : HeckePair G) : (deg P) 1 = 1

The degree of the identity element is 1.

theorem HeckeRing.deg_mul {G : Type u_1} [Group G] (P : HeckePair G) (f g : 𝕋 P ℤ) : (deg P) (f * g) = (deg P) f * (deg P) g

The degree map is multiplicative: deg(f * g) = deg(f) * deg(g).

theorem HeckeRing.deg_add {G : Type u_1} [Group G] (P : HeckePair G) (f g : 𝕋 P ℤ) : (deg P) (f + g) = (deg P) f + (deg P) g

The degree map is additive: deg(f + g) = deg(f) + deg(g).

theorem HeckeRing.deg_intCast {G : Type u_1} [Group G] (P : HeckePair G) (n : ℤ) : (deg P) ↑n = n

The degree of an integer cast is the integer itself.