Hecke rings: definitions

This file introduces the abstract Hecke ring of a Hecke pair (H, Δ) and, more generally, the Hecke coset modules attached to a triple (H₁, Δ, H₂), following Shimura, Chapter 3, and Krieg, Chapter I. It sets up the underlying types: the compatibility conditions IsHeckeTriple Δ H₁ H₂ on a submonoid Δ of a group G and a pair of subgroups of G, the double-coset quotient HeckeCoset Δ H₁ H₂ of Δ by H₁gH₂ = H₁hH₂, and the Hecke coset module HeckeCosetModule Δ H₁ H₂ Z of formal finitely-supported linear combinations of double cosets. The convolution product HeckeCosetModule Δ H₁ H₂ Z × HeckeCosetModule Δ H₂ H₃ Z → HeckeCosetModule Δ H₁ H₃ Z and the ring structure on the diagonal Hecke ring 𝕋 Δ H Z are developed in later files.

The relevance of the submonoid Δ may not be immediately obvious; a natural example is H = GL₂(ℤ) inside G = GL₂(ℚ) with Δ the submonoid of integral matrices with nonzero determinant, which is the Hecke pair underlying the classical Hecke operators T_n. Mixed subgroups H₁ ≠ H₂ arise for Hecke operators between different levels, e.g. H₁ = Γ₀(N) and H₂ = Γ₀(M) inside the same Δ.

Main definitions

• IsHeckeTriple Δ H₁ H₂: (H₁, Δ, H₂) is a Hecke triple, i.e. H₁ ≤ Δ, H₂ ≤ Δ, Commensurable H₁ H₂ and Δ ≤ commensurator H₂, making the double cosets H₁\Δ/H₂ finite unions of left cosets. The classical Hecke pair (H, Δ) is the diagonal case IsHeckeTriple Δ H H.
• HeckeCoset Δ H₁ H₂: the quotient of Δ by the relation H₁gH₂ = H₁hH₂, i.e. the double cosets H₁\Δ/H₂ forming the basis of the Hecke coset module.
• HeckeCosetModule Δ H₁ H₂ Z: the Hecke coset module with coefficients in Z, the finitely-supported Z-linear combinations of double cosets.
• HeckeRing Δ H Z, notation 𝕋 Δ H Z: the Hecke ring, the diagonal case HeckeCosetModule Δ H H Z of the Hecke coset module.

Implementation notes

The data (Δ, H₁, H₂) enters unbundled, with the compatibility conditions collected in the Prop-valued class IsHeckeTriple: the types HeckeCoset Δ H₁ H₂ and HeckeCosetModule Δ H₁ H₂ Z are built from the data alone and depend on no proofs, and a single ambient Δ shared by all levels (as in Shimura) means products of double cosets over different subgroups, H₁g₁H₂ * H₂g₂H₃ ⊆ Δ, need no compatibility hypotheses. The conditions are only needed for the finiteness of the coset decompositions, which enters through the Fintype instance on DoubleCoset.DecompQuotient in later files. Requiring Δ to be a submonoid rather than a subsemigroup loses no generality, since H₁ ≤ Δ already forces 1 ∈ Δ.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions
• A. Krieg, Hecke algebras

class IsHeckeTriple {G : Type u_1} [Group G] (Δ : Submonoid G) (H₁ H₂ : Subgroup G) : Prop

A Hecke triple (H₁, Δ, H₂): the compatibility conditions on a submonoid Δ and a pair of subgroups H₁, H₂ of G making the double cosets H₁\Δ/H₂ finite unions of left cosets: both subgroups are contained in Δ, they are commensurable, and Δ commensurates them. The classical Hecke pair (H, Δ) of Shimura, Chapter 3, is the diagonal case IsHeckeTriple Δ H H.

• left_le : H₁.toSubmonoid ≤ Δ

  The left subgroup is contained in Δ.

• right_le : H₂.toSubmonoid ≤ Δ

  The right subgroup is contained in Δ.

• commensurable : H₁.Commensurable H₂

  The two subgroups are commensurable.

• le_commensurator_right : Δ ≤ (Subgroup.Commensurable.commensurator H₂).toSubmonoid

  The submonoid Δ lies in the commensurator of the right subgroup (hence, the subgroups being commensurable, also in that of the left one; see le_commensurator_left).

theorem IsHeckeTriple.of_diagonal {G : Type u_1} [Group G] {Δ : Submonoid G} {H : Subgroup G} (h : H.toSubmonoid ≤ Δ) (hc : Δ ≤ (Subgroup.Commensurable.commensurator H).toSubmonoid) : IsHeckeTriple Δ H H

The Hecke triple (H, Δ, H) coming from a pair (H, Δ) with H ≤ Δ ≤ commensurator H.

theorem IsHeckeTriple.mem_of_mem_left {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ : Subgroup G} (H₂ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] {x : G} (hx : x ∈ H₁) : x ∈ Δ

Elements of the left subgroup lie in Δ.

theorem IsHeckeTriple.mem_of_mem_right {G : Type u_1} [Group G] {Δ : Submonoid G} {H₂ : Subgroup G} (H₁ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] {x : G} (hx : x ∈ H₂) : x ∈ Δ

Elements of the right subgroup lie in Δ.

theorem IsHeckeTriple.le_commensurator_left {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ : Subgroup G} (H₂ : Subgroup G) [h : IsHeckeTriple Δ H₁ H₂] : Δ ≤ (Subgroup.Commensurable.commensurator H₁).toSubmonoid

The submonoid Δ lies in the commensurator of the left subgroup.

theorem IsHeckeTriple.mem_commensurator_right {G : Type u_1} [Group G] {Δ : Submonoid G} {H₂ : Subgroup G} (H₁ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] (g : ↥Δ) : ↑g ∈ Subgroup.Commensurable.commensurator H₂

Elements of Δ lie in the commensurator of the right subgroup.

theorem IsHeckeTriple.mem_commensurator_left {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ : Subgroup G} (H₂ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] (g : ↥Δ) : ↑g ∈ Subgroup.Commensurable.commensurator H₁

Elements of Δ lie in the commensurator of the left subgroup.

theorem IsHeckeTriple.commensurable_conjAct_right {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] (g : ↥Δ) : (ConjAct.toConjAct ↑g • H₂).Commensurable H₁

Conjugating the right subgroup of a Hecke triple (H₁, Δ, H₂) by an element of Δ gives a subgroup commensurable with the left one.

theorem IsHeckeTriple.trans {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ H₃ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] [IsHeckeTriple Δ H₂ H₃] : IsHeckeTriple Δ H₁ H₃

Hecke coset module data compose. Not an instance, since the middle subgroup cannot be inferred from the goal.

theorem IsHeckeTriple.diag_left {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] : IsHeckeTriple Δ H₁ H₁

The left diagonal datum (H₁, Δ, H₁). Not an instance, since H₂ cannot be inferred.

theorem IsHeckeTriple.diag_right {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} [IsHeckeTriple Δ H₁ H₂] : IsHeckeTriple Δ H₂ H₂

The right diagonal datum (H₂, Δ, H₂). Not an instance, since H₁ cannot be inferred.

@[reducible, inline]

abbrev HeckeCoset.setoid {G : Type u_1} [Group G] (Δ : Submonoid G) (H₁ H₂ : Subgroup G) : Setoid ↥Δ

The setoid on Δ identifying elements with the same double coset H₁gH₂ = H₁hH₂, pulled back from DoubleCoset.setoid along the inclusion Δ ↪ G.

This is an abbrev rather than a global instance: the subgroups H₁, H₂ cannot be inferred from the submonoid Δ, so this cannot participate in instance search (and a global instance would also create a Setoid diamond on ↥Δ with the left-coset setoid). The quotient map is HeckeCoset.mk.

Equations

• HeckeCoset.setoid Δ H₁ H₂ = Setoid.comap Subtype.val (DoubleCoset.setoid ↑H₁ ↑H₂)

def HeckeCoset {G : Type u_1} [Group G] (Δ : Submonoid G) (H₁ H₂ : Subgroup G) : Type u_1

A Hecke double coset: an equivalence class of Δ-elements under H₁gH₂ = H₁hH₂. This is the basis type for the HeckeCosetModule.

Equations

• HeckeCoset Δ H₁ H₂ = Quotient (HeckeCoset.setoid Δ H₁ H₂)

def HeckeCoset.mk {G : Type u_1} [Group G] {Δ : Submonoid G} (H₁ H₂ : Subgroup G) (g : ↥Δ) : HeckeCoset Δ H₁ H₂

The double coset H₁gH₂ of an element g : Δ.

Equations

• HeckeCoset.mk H₁ H₂ g = ⟦g⟧

@[implicit_reducible]

instance HeckeCoset.instInhabited {G : Type u_1} [Group G] (Δ : Submonoid G) (H₁ H₂ : Subgroup G) : Inhabited (HeckeCoset Δ H₁ H₂)

Equations

• HeckeCoset.instInhabited Δ H₁ H₂ = { default := HeckeCoset.mk H₁ H₂ ⟨1, ⋯⟩ }

@[implicit_reducible]

instance HeckeCoset.instOne {G : Type u_1} [Group G] (Δ : Submonoid G) (H : Subgroup G) : One (HeckeCoset Δ H H)

The identity double coset H1H = H of the diagonal (Hecke pair) case.

Equations

• HeckeCoset.instOne Δ H = { one := HeckeCoset.mk H H ⟨1, ⋯⟩ }

theorem HeckeCoset.one_def {G : Type u_1} [Group G] {Δ : Submonoid G} (H : Subgroup G) : 1 = mk H H ⟨1, ⋯⟩

def HeckeCosetModule {G : Type u_1} [Group G] (Δ : Submonoid G) (H₁ H₂ : Subgroup G) (Z : Type u_2) [Zero Z] : Type (max u_2 u_1)

The Hecke coset module with coefficients in Z: the finitely-supported Z-linear combinations of double cosets H₁\Δ/H₂. For H₁ = H₂ this is the underlying module of the Hecke ring 𝕋 Δ H Z (see HeckeRing). The coefficients Z need only carry a Zero for the type to make sense; algebraic structure is added by the instances below at the weakest level each requires.

Equations

• HeckeCosetModule Δ H₁ H₂ Z = (HeckeCoset Δ H₁ H₂ →₀ Z)

@[reducible, inline]

abbrev HeckeRing {G : Type u_1} [Group G] (Δ : Submonoid G) (H : Subgroup G) (Z : Type u_2) [Zero Z] : Type (max u_2 u_1)

The Hecke ring 𝕋 Δ H Z with coefficients in Z: the diagonal Hecke coset module HeckeCosetModule Δ H H Z, the finitely-supported Z-linear combinations of double cosets H\Δ/H. The convolution product making it a ring is developed in later files.

Equations

• HeckeRing Δ H Z = HeckeCosetModule Δ H H Z

def HeckeCosetModule.term𝕋 : Lean.ParserDescr

The Hecke ring 𝕋 Δ H Z with coefficients in Z: the diagonal Hecke coset module HeckeCosetModule Δ H H Z, the finitely-supported Z-linear combinations of double cosets H\Δ/H. The convolution product making it a ring is developed in later files.

Equations

• HeckeCosetModule.term𝕋 = Lean.ParserDescr.node `HeckeCosetModule.term𝕋 1024 (Lean.ParserDescr.symbol "𝕋")

@[implicit_reducible]

instance HeckeCosetModule.instFunLikeHeckeCoset {G : Type u_1} [Group G] (Δ : Submonoid G) (H₁ H₂ : Subgroup G) (Z : Type u_2) [Zero Z] : FunLike (HeckeCosetModule Δ H₁ H₂ Z) (HeckeCoset Δ H₁ H₂) Z

Elements of HeckeCosetModule Δ H₁ H₂ Z are functions HeckeCoset Δ H₁ H₂ → Z (finitely supported).

Equations

• HeckeCosetModule.instFunLikeHeckeCoset Δ H₁ H₂ Z = { coe := HeckeCosetModule.instFunLikeHeckeCoset._aux_1 Δ H₁ H₂ Z, coe_injective := ⋯ }

@[implicit_reducible]

noncomputable instance HeckeCosetModule.instAddCommMonoid {G : Type u_1} [Group G] (Δ : Submonoid G) (H₁ H₂ : Subgroup G) (Z : Type u_2) [AddCommMonoid Z] : AddCommMonoid (HeckeCosetModule Δ H₁ H₂ Z)

Equations

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

@[implicit_reducible]

noncomputable instance HeckeCosetModule.instAddCommGroup {G : Type u_1} [Group G] (Δ : Submonoid G) (H₁ H₂ : Subgroup G) (Z : Type u_2) [AddCommGroup Z] : AddCommGroup (HeckeCosetModule Δ H₁ H₂ Z)

Equations

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

def HeckeCosetModule.of {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} {Z : Type u_3} [Zero Z] : (HeckeCoset Δ H₁ H₂ →₀ Z) ≃ HeckeCosetModule Δ H₁ H₂ Z

The sanctioned constructor of HeckeCosetModule Δ H₁ H₂ Z from a finitely-supported function on double cosets. Build elements through of rather than relying on the definitional unfolding HeckeCosetModule Δ H₁ H₂ Z = (HeckeCoset Δ H₁ H₂ →₀ Z).

Equations

• HeckeCosetModule.of = Equiv.refl (HeckeCoset Δ H₁ H₂ →₀ Z)

@[simp]

theorem HeckeCosetModule.of_apply {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} {Z : Type u_3} [Zero Z] (f : HeckeCoset Δ H₁ H₂ →₀ Z) (D : HeckeCoset Δ H₁ H₂) : (of f) D = f D

theorem HeckeCosetModule.ext {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} {Z : Type u_3} [Zero Z] {f g : HeckeCosetModule Δ H₁ H₂ Z} (h : ∀ (D : HeckeCoset Δ H₁ H₂), f D = g D) : f = g

theorem HeckeCosetModule.ext_iff {G : Type u_1} [Group G] {Δ : Submonoid G} {H₁ H₂ : Subgroup G} {Z : Type u_3} [Zero Z] {f g : HeckeCosetModule Δ H₁ H₂ Z} : f = g ↔ ∀ (D : HeckeCoset Δ H₁ H₂), f D = g D