Hecke Rings: Module Action

The module action of 𝕋 P ℤ on HeckeModule P ℤ (formal sums of left cosets) and the faithfulness theorem eq_of_smul_eq_smul_𝕋.

@[implicit_reducible, instance 1100]

noncomputable instance HeckeRing.instSMul𝕋 {G : Type u_1} [Group G] (P : HeckePair G) : SMul (𝕋 P ℤ) (𝕋 P ℤ)

The scalar multiplication on 𝕋 by itself, defined as reverse multiplication. Higher priority than the inherited Mul.toSMul so that • denotes the reverse action.

Equations

• HeckeRing.instSMul𝕋 P = { smul := fun (x y : HeckeRing.𝕋 P ℤ) => y * x }

noncomputable def HeckeRing.smulOrbit {G : Type u_1} [Group G] (P : HeckePair G) (g β : ↥P.Δ) : Finset (HeckeLeftCoset P)

The orbit of a left coset representative β under double coset representative g: the set of left cosets {β · σ_i · g | σ_i ∈ H/(H ∩ gHg⁻¹)}.

Equations

• HeckeRing.smulOrbit P g β = Finset.image (fun (i : HeckeRing.decompQuot P g) => ⟦⟨↑β * ↑(Quotient.out i) * ↑g, ⋯⟩⟧) ⊤

theorem HeckeRing.smulOrbit_nonempty {G : Type u_1} [Group G] (P : HeckePair G) (g β : ↥P.Δ) : (smulOrbit P g β).Nonempty

The smul orbit of any left coset under any double coset is nonempty.

theorem HeckeRing.smulOrbit_lcRel {G : Type u_1} [Group G] (P : HeckePair G) (g : ↥P.Δ) {β₁ β₂ : ↥P.Δ} (h : lcRel P β₁ β₂) : smulOrbit P g β₁ = smulOrbit P g β₂

The orbit is invariant under left coset equivalence: if β₁H = β₂H, then smulOrbit g β₁ = smulOrbit g β₂. This is the key API lemma that lets us replace HeckeLeftCoset.rep j with any representative of j.

theorem HeckeRing.smulOrbit_rep_mk {G : Type u_1} [Group G] (P : HeckePair G) (g β : ↥P.Δ) : smulOrbit P g (HeckeLeftCoset.rep ⟦β⟧) = smulOrbit P g β

Corollary: smulOrbit g (HeckeLeftCoset.rep ⟦β⟧) = smulOrbit g β.

@[implicit_reducible]

noncomputable instance HeckeRing.instSMulHeckeModule {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] : SMul (𝕋 P Z) (HeckeModule P Z)

The module action of the Hecke ring on formal sums of left cosets.

Equations

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

theorem HeckeRing.smul_eq_sum {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] (T : 𝕋 P Z) (m : HeckeModule P Z) : T • m = Finsupp.sum T fun (D1 : HeckeCoset P) (b₁ : Z) => Finsupp.sum m fun (m : HeckeLeftCoset P) (b₂ : Z) => ∑ i ∈ smulOrbit P D1.rep m.rep, Finsupp.single i (b₁ * b₂)

The scalar multiplication on HeckeModule unfolds as a double sum over orbits.

theorem HeckeRing.single_smul_single {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] (t : HeckeCoset P) (m : HeckeLeftCoset P) (a b : Z) : Finsupp.single t a • Finsupp.single m b = ∑ i ∈ smulOrbit P t.rep m.rep, Finsupp.single i (a * b)

The action of a basis Hecke element on a basis module element.

theorem HeckeRing.single_basis (Z : Type u_2) [CommRing Z] {α : Type u_3} (t : α →₀ Z) : t = ∑ i ∈ t.support, Finsupp.single i (t.toFun i)

Every finsupp is a sum of its basis elements.

@[implicit_reducible]

noncomputable instance HeckeRing.instOneHeckeModule {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] : One (HeckeModule P Z)

The one element of HeckeModule: the basis element for the identity left coset.

Equations

• HeckeRing.instOneHeckeModule P Z = { one := Finsupp.single (HeckeRing.HeckeLeftCoset.one P) 1 }

theorem HeckeRing.one_eq_HeckeLeftCoset_single {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] : 1 = Finsupp.single (HeckeLeftCoset.one P) 1

The one element of HeckeModule is the basis element corresponding to the identity left coset.

theorem HeckeRing.smul_add_left {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] (T₁ T₂ : 𝕋 P Z) (m : HeckeModule P Z) : (T₁ + T₂) • m = T₁ • m + T₂ • m

The module action is additive in the Hecke ring argument.

theorem HeckeRing.zero_smul_HeckeModule {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] (z : HeckeModule P Z) : 0 • z = 0

The zero element of the Hecke ring acts as zero on the module.

theorem HeckeRing.smul_zero_HeckeModule {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] (T : 𝕋 P Z) : T • 0 = 0

Any Hecke ring element acts as zero on the zero module element.

theorem HeckeRing.smul_add_right {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] (T : 𝕋 P Z) (m₁ m₂ : HeckeModule P Z) : T • (m₁ + m₂) = T • m₁ + T • m₂

The module action is additive in the module argument.

theorem HeckeRing.smulOrbit_disjoint_of_ne {G : Type u_1} [Group G] (P : HeckePair G) (g₁ g₂ β : ↥P.Δ) (hne : ⟦g₁⟧ ≠ ⟦g₂⟧) : Disjoint (smulOrbit P g₁ β) (smulOrbit P g₂ β)

The smul orbits of distinct double cosets acting on the same left coset are disjoint.

theorem HeckeRing.eq_of_smul_eq_smul_𝕋 {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] (T1 T2 : 𝕋 P Z) (h : ∀ (a : HeckeModule P Z), T1 • a = T2 • a) : T1 = T2

Faithfulness of the module action: if two Hecke ring elements act identically on all module elements, they are equal.

instance HeckeRing.instFaithfulSMulHeckeModule {G : Type u_1} [Group G] (P : HeckePair G) : FaithfulSMul (𝕋 P ℤ) (HeckeModule P ℤ)

The module action of 𝕋 P ℤ on HeckeModule P ℤ is faithful.

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

The scalar multiplication on 𝕋 is defined as reverse multiplication.