Hecke Rings: Basic Definitions

Basic definitions for Hecke rings following Shimura Ch. 3: HeckePair, double coset spaces HeckeCoset and HeckeLeftCoset, the Hecke ring type 𝕋, and foundational double coset lemmas.

theorem HeckeRing.conjAct_smul_coe_eq {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : ConjAct.toConjAct g • ↑H = {g} * ↑H * {g⁻¹}

The conjugation action on H as a set product: gHg⁻¹ = {g} * H * {g⁻¹}.

theorem HeckeRing.conjAct_smul_elt_eq {G : Type u_1} [Group G] (H : Subgroup G) (h : ↥H) : ConjAct.toConjAct ↑h • H = H

Conjugation by an element of H fixes H.

theorem HeckeRing.leftCoset_eq_of_subset {G : Type u_1} [Group G] (H : Subgroup G) (a b : G) (h : {a} * ↑H ⊆ {b} * ↑H) : {a} * ↑H = {b} * ↑H

A left coset contained in another left coset is equal to it.

structure HeckeRing.HeckePair (G : Type u_2) [Group G] : Type u_2

An arithmetic group pair (H, Δ) consisting of a subgroup H and a submonoid Δ of a group G, satisfying H ≤ Δ ≤ commensurator(H).

• H : Subgroup G

  The distinguished subgroup H of the arithmetic pair.

• Δ : Submonoid G

  The commensurating submonoid Δ of the arithmetic pair.

• h₀ : self.H.toSubmonoid ≤ self.Δ
• h₁ : self.Δ ≤ (Subgroup.Commensurable.commensurator self.H).toSubmonoid

def HeckeRing.dcRel {G : Type u_1} [Group G] (P : HeckePair G) (g h : ↥P.Δ) : Prop

Two elements of Δ define the same double coset HgH = HhH.

Equations

• HeckeRing.dcRel P g h = (DoubleCoset.doubleCoset ↑g ↑P.H ↑P.H = DoubleCoset.doubleCoset ↑h ↑P.H ↑P.H)

@[implicit_reducible]

instance HeckeRing.dcSetoid {G : Type u_1} [Group G] (P : HeckePair G) : Setoid ↥P.Δ

The setoid on Δ identifying elements with the same double coset.

Equations

• HeckeRing.dcSetoid P = { r := HeckeRing.dcRel P, iseqv := ⋯ }

@[reducible, inline]

abbrev HeckeRing.HeckeCoset {G : Type u_1} [Group G] (P : HeckePair G) : Type u_1

A Hecke double coset: an equivalence class of Δ-elements under HgH = HhH. This is the basis type for the Hecke ring.

Equations

• HeckeRing.HeckeCoset P = Quotient (HeckeRing.dcSetoid P)

@[implicit_reducible]

noncomputable instance HeckeRing.instDecidableEqHeckeCoset {G : Type u_1} [Group G] (P : HeckePair G) : DecidableEq (HeckeCoset P)

Equations

• HeckeRing.instDecidableEqHeckeCoset P = Classical.decEq (HeckeRing.HeckeCoset P)

def HeckeRing.lcRel {G : Type u_1} [Group G] (P : HeckePair G) (g h : ↥P.Δ) : Prop

Two elements of Δ define the same left coset gH = hH.

Equations

• HeckeRing.lcRel P g h = ({↑g} * ↑P.H = {↑h} * ↑P.H)

@[implicit_reducible]

instance HeckeRing.lcSetoid {G : Type u_1} [Group G] (P : HeckePair G) : Setoid ↥P.Δ

The setoid on Δ identifying elements with the same left coset.

Equations

• HeckeRing.lcSetoid P = { r := HeckeRing.lcRel P, iseqv := ⋯ }

def HeckeRing.HeckeLeftCoset {G : Type u_1} [Group G] (P : HeckePair G) : Type u_1

A Hecke left coset: an equivalence class of Δ-elements under gH = hH.

Equations

• HeckeRing.HeckeLeftCoset P = Quotient (HeckeRing.lcSetoid P)

@[implicit_reducible]

noncomputable instance HeckeRing.instDecidableEqHeckeLeftCoset {G : Type u_1} [Group G] (P : HeckePair G) : DecidableEq (HeckeLeftCoset P)

Equations

• HeckeRing.instDecidableEqHeckeLeftCoset P = Classical.decEq (HeckeRing.HeckeLeftCoset P)

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

The underlying set HgH, well-defined on the quotient.

Equations

• D.toSet = Quotient.lift (fun (g : ↥P.Δ) => DoubleCoset.doubleCoset ↑g ↑P.H ↑P.H) ⋯ D

noncomputable def HeckeRing.HeckeCoset.rep {G : Type u_1} [Group G] {P : HeckePair G} (D : HeckeCoset P) : ↥P.Δ

A representative g : Δ (via Quotient.out).

Equations

• D.rep = Quotient.out D

theorem HeckeRing.HeckeCoset.eq_iff {G : Type u_1} [Group G] {P : HeckePair G} (g h : ↥P.Δ) : ⟦g⟧ = ⟦h⟧ ↔ DoubleCoset.doubleCoset ↑g ↑P.H ↑P.H = DoubleCoset.doubleCoset ↑h ↑P.H ↑P.H

⟦g⟧ = ⟦h⟧ ↔ HgH = HhH.

@[simp]

theorem HeckeRing.HeckeCoset.toSet_mk {G : Type u_1} [Group G] {P : HeckePair G} (g : ↥P.Δ) : toSet ⟦g⟧ = DoubleCoset.doubleCoset ↑g ↑P.H ↑P.H

The carrier set of ⟦g⟧ is definitionally HgH.

theorem HeckeRing.HeckeCoset.mem_toSet_mk {G : Type u_1} [Group G] {P : HeckePair G} (g : ↥P.Δ) (x : G) : x ∈ toSet ⟦g⟧ ↔ x ∈ DoubleCoset.doubleCoset ↑g ↑P.H ↑P.H

Membership in toSet ⟦g⟧ is membership in the double coset HgH.

theorem HeckeRing.HeckeCoset.ext_toSet {G : Type u_1} [Group G] {P : HeckePair G} {D₁ D₂ : HeckeCoset P} (h : D₁.toSet = D₂.toSet) : D₁ = D₂

If two HeckeCosets have the same toSet, they are equal.

theorem HeckeRing.HeckeCoset.toSet_eq_rep {G : Type u_1} [Group G] {P : HeckePair G} (D : HeckeCoset P) : D.toSet = DoubleCoset.doubleCoset ↑D.rep ↑P.H ↑P.H

The carrier set equals the double coset of the representative.

theorem HeckeRing.HeckeCoset.rep_mem {G : Type u_1} [Group G] {P : HeckePair G} (D : HeckeCoset P) : ↑D.rep ∈ D.toSet

The representative lies in its double coset.

theorem HeckeRing.HeckeCoset.doubleCoset_eq_of_mem {G : Type u_1} [Group G] {P : HeckePair G} {g : ↥P.Δ} {x : G} (hx : x ∈ DoubleCoset.doubleCoset ↑g ↑P.H ↑P.H) : DoubleCoset.doubleCoset x ↑P.H ↑P.H = DoubleCoset.doubleCoset ↑g ↑P.H ↑P.H

If x ∈ HgH, then HxH = HgH. The fundamental double coset absorption lemma.

theorem HeckeRing.HeckeCoset.eq_mk_of_mem {G : Type u_1} [Group G] {P : HeckePair G} {g₁ g₂ : ↥P.Δ} (h : ↑g₁ ∈ DoubleCoset.doubleCoset ↑g₂ ↑P.H ↑P.H) : ⟦g₁⟧ = ⟦g₂⟧

⟦g₁⟧ = ⟦g₂⟧ when g₁ is in the double coset of g₂.

def HeckeRing.HeckeCoset.one {G : Type u_1} [Group G] (P : HeckePair G) : HeckeCoset P

The identity double coset H1H = H.

Equations

• HeckeRing.HeckeCoset.one P = ⟦⟨1, ⋯⟩⟧

theorem HeckeRing.HeckeCoset.ind {G : Type u_1} [Group G] {P : HeckePair G} {motive : HeckeCoset P → Prop} (h : ∀ (g : ↥P.Δ), motive ⟦g⟧) (D : HeckeCoset P) : motive D

Induction: to prove something for all double cosets, prove it for ⟦g⟧.

theorem HeckeRing.HeckeCoset.ind₂ {G : Type u_1} [Group G] {P : HeckePair G} {motive : HeckeCoset P → HeckeCoset P → Prop} (h : ∀ (g₁ g₂ : ↥P.Δ), motive ⟦g₁⟧ ⟦g₂⟧) (D₁ D₂ : HeckeCoset P) : motive D₁ D₂

Two-argument induction.

theorem HeckeRing.HeckeCoset.one_rep_mem_H {G : Type u_1} [Group G] (P : HeckePair G) : ↑(one P).rep ∈ P.H

The representative of HeckeCoset.one belongs to H.

noncomputable def HeckeRing.HeckeLeftCoset.toSet {G : Type u_1} [Group G] {P : HeckePair G} (D : HeckeLeftCoset P) : Set G

The underlying set gH, well-defined on the quotient.

Equations

• D.toSet = Quotient.lift (fun (g : ↥P.Δ) => {↑g} * ↑P.H) ⋯ D

noncomputable def HeckeRing.HeckeLeftCoset.rep {G : Type u_1} [Group G] {P : HeckePair G} (D : HeckeLeftCoset P) : ↥P.Δ

A representative g : Δ.

Equations

• D.rep = Quotient.out D

def HeckeRing.HeckeLeftCoset.one {G : Type u_1} [Group G] (P : HeckePair G) : HeckeLeftCoset P

The identity left coset 1H = H.

Equations

• HeckeRing.HeckeLeftCoset.one P = ⟦⟨1, ⋯⟩⟧

theorem HeckeRing.HeckeLeftCoset.ind {G : Type u_1} [Group G] {P : HeckePair G} {motive : HeckeLeftCoset P → Prop} (h : ∀ (g : ↥P.Δ), motive ⟦g⟧) (D : HeckeLeftCoset P) : motive D

Induction for left cosets.

theorem HeckeRing.doset_mul_left_eq_self {G : Type u_1} [Group G] (P : HeckePair G) (h : ↥P.H) (g : G) : DoubleCoset.doubleCoset (↑h * g) ↑P.H ↑P.H = DoubleCoset.doubleCoset g ↑P.H ↑P.H

Left-multiplying the representative by an element of H does not change the double coset.

theorem HeckeRing.DoubleCoset.doubleCoset_mul_right_eq_self {G : Type u_1} [Group G] (P : HeckePair G) (h : ↥P.H) (g : G) : DoubleCoset.doubleCoset (g * ↑h) ↑P.H ↑P.H = DoubleCoset.doubleCoset g ↑P.H ↑P.H

Right-multiplying the representative by an element of H does not change the double coset.

theorem HeckeRing.DoubleCoset.doubleCoset_mul_assoc {G : Type u_1} [Group G] (H : Subgroup G) (f g h : G) : DoubleCoset.doubleCoset (f * g * h) ↑H ↑H = DoubleCoset.doubleCoset (f * (g * h)) ↑H ↑H

Associativity of group multiplication lifts to double coset representatives.

theorem HeckeRing.smul_eq_singleton_mul {G : Type u_1} [Group G] (s : Set G) (g : G) : g • s = {g} * s

Scalar multiplication by a group element is the same as singleton set multiplication.

theorem HeckeRing.set_eq_iUnion_leftCosets {G : Type u_1} [Group G] (H K : Subgroup G) (hK : K ≤ H) : ↑H = ⋃ (i : ↥H ⧸ K.subgroupOf H), ↑(Quotient.out i) • ↑K

A subgroup H is the union of left cosets of any sub-subgroup K ≤ H.

theorem HeckeRing.conjAct_mul_self_eq_self {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : ConjAct.toConjAct g • ↑H * ConjAct.toConjAct g • ↑H = ConjAct.toConjAct g • ↑H

The conjugate subgroup gHg⁻¹ is closed under multiplication.

theorem HeckeRing.inter_mul_conjAct_eq_conjAct {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : ↑H ∩ ConjAct.toConjAct g • ↑H * ConjAct.toConjAct g • ↑H = ConjAct.toConjAct g • ↑H

The intersection H ∩ gHg⁻¹ acts trivially on gHg⁻¹ by left multiplication.

theorem HeckeRing.mul_singleton_right_cancel {G : Type u_1} [Group G] (g : G) (K L : Set G) (h : K * {g} = L * {g}) : K = L

Right multiplication by a singleton is cancellative.

theorem HeckeRing.DoubleCoset.doubleCoset_eq_iUnion_leftCosets {G : Type u_1} [Group G] (H : Subgroup G) (g : G) : DoubleCoset.doubleCoset g ↑H ↑H = ⋃ (i : ↥H ⧸ (ConjAct.toConjAct g • H).subgroupOf H), (↑(Quotient.out i) * g) • ↑H

A double coset HgH decomposes as a disjoint union of left cosets of H.

theorem HeckeRing.doubleCoset_mul_doubleCoset_left {G : Type u_1} [Group G] (H : Subgroup G) (g h : G) : DoubleCoset.doubleCoset g ↑H ↑H * DoubleCoset.doubleCoset h ↑H ↑H = DoubleCoset.doubleCoset g ↑H ↑H * {h} * ↑H

The product of two double cosets simplifies using H * H = H on the left.

theorem HeckeRing.doubleCoset_mul_doubleCoset_right {G : Type u_1} [Group G] (H : Subgroup G) (g h : G) : DoubleCoset.doubleCoset g ↑H ↑H * DoubleCoset.doubleCoset h ↑H ↑H = ↑H * {g} * DoubleCoset.doubleCoset h ↑H ↑H

The product of two double cosets simplifies using H * H = H on the right.

theorem HeckeRing.doubleCoset_mul_eq_iUnion_doubleCoset {G : Type u_1} [Group G] (H : Subgroup G) (g h : G) : DoubleCoset.doubleCoset g ↑H ↑H * DoubleCoset.doubleCoset h ↑H ↑H = ⋃ (i : ↥H ⧸ (ConjAct.toConjAct h • H).subgroupOf H), DoubleCoset.doubleCoset (g * ↑(Quotient.out i) * h) ↑H ↑H

The set-theoretic product of two double cosets is a union of double cosets.

theorem HeckeRing.DoubleCoset.doubleCoset_one_mul {G : Type u_1} [Group G] (H : Subgroup G) (h : G) : DoubleCoset.doubleCoset h ↑H ↑H = ⋃ (x : ↥H ⧸ (ConjAct.toConjAct h • H).subgroupOf H), DoubleCoset.doubleCoset h ↑H ↑H

The double coset HhH is a constant union indexed by the trivial quotient.

@[reducible, inline]

abbrev HeckeRing.𝕋 {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] : Type (max u_2 u_1)

The Hecke ring type: formal Z-linear combinations of double cosets HeckeCoset P. Changed from def to abbrev for transparency in instance resolution (Lean 4.29+).

Equations

• HeckeRing.𝕋 P Z = (HeckeRing.HeckeCoset P →₀ Z)

@[reducible, inline]

abbrev HeckeRing.HeckeModule {G : Type u_1} [Group G] (P : HeckePair G) (Z : Type u_2) [CommRing Z] : Type (max u_2 u_1)

The Hecke module type: formal Z-linear combinations of left cosets HeckeLeftCoset P. Changed from def to abbrev for transparency in instance resolution (Lean 4.29+).

Equations

• HeckeRing.HeckeModule P Z = (HeckeRing.HeckeLeftCoset P →₀ Z)

@[reducible, inline]

abbrev HeckeRing.decompQuot {G : Type u_1} [Group G] (P : HeckePair G) (g : ↥P.Δ) : Type u_1

The decomposition quotient H / (H ∩ gHg⁻¹) for a concrete g : Δ. Indexes the left cosets in the decomposition of HgH.

Equations

• HeckeRing.decompQuot P g = (↥P.H ⧸ (ConjAct.toConjAct ↑g • P.H).subgroupOf P.H)

@[implicit_reducible]

noncomputable instance HeckeRing.instFintypeDecompQuot {G : Type u_1} [Group G] (P : HeckePair G) (g : ↥P.Δ) : Fintype (decompQuot P g)

The decomposition quotient is finite because Δ ≤ commensurator(H).

Equations

• HeckeRing.instFintypeDecompQuot P g = Subgroup.fintypeOfIndexNeZero ⋯

theorem HeckeRing.delta_mul_mem {G : Type u_1} [Group G] (H : Subgroup G) (Δ : Submonoid G) (i : ↥H) (a b : ↥Δ) (h₀ : H.toSubmonoid ≤ Δ) : ↑a * ↑i * ↑b ∈ Δ

Products of the form a · h · b with h ∈ H, a, b ∈ Δ remain in Δ.

@[implicit_reducible]

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

The additive commutative group structure on the Hecke ring.

Equations

• HeckeRing.instAddCommGroup𝕋 P Z = { toAddGroup := Finsupp.instAddGroup, add_comm := ⋯ }

@[implicit_reducible]

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

The additive commutative group structure on the Hecke module.

Equations

• HeckeRing.instAddCommGroupHeckeModule P Z = { toAddGroup := Finsupp.instAddGroup, add_comm := ⋯ }