The Hecke triple of Γ₀(N)

The image of Γ₀(N) in GL₂(ℚ) forms a Hecke triple with the submonoid Δ₀(N). This is the setting of Shimura §3.3: the Hecke ring R(Γ₀(N), Δ₀(N)) whose operators act on M_k(Γ₀(N)).

Δ₀(N) is shared with the Hecke triple of Γ₁(N) and lives in TauCeti.NumberTheory.HeckeRing.GL2.Delta0; nothing about it refers to either group. What is specific here is which group sits inside it: an element of Γ₀(N) has ad ≡ 1 modulo N, since c ≡ 0 and the determinant is one, so its upper-left entry is a unit — which is exactly the condition Δ₀(N) imposes, and the reason it was defined with a unit upper-left entry rather than a ≡ 1.

Γ₁(N) ≤ Γ₀(N), so R(Γ₀(N), Δ₀(N)) is the smaller of the two rings. Shimura's Theorem 3.35 is a separate statement again: a surjection onto R(Γ₀(N), Δ₀(N)) from the level-one ring R(SL₂(ℤ), Δ) — not from the Γ₁(N) ring — with kernel generated by T(p, p) for p ∣ N. It is not formalised here.

The Γ₀ pair corresponds to the AINTLIB LeanModularForms file LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/Foundation.lean (Chris Birkbeck), whose Delta0_submonoid and Gamma0_pair open that file.

Main definitions

• HeckeRing.GL2.Gamma0Image: the image of Γ₀(N) in GL₂(ℚ).

Main results

• HeckeRing.GL2.Gamma0Image_le_Delta0: Γ₀(N) ≤ Δ₀(N).
• HeckeRing.GL2.map_withCenter_le_Delta0: and H·{±I} ≤ Δ₀(N) for any H ≤ Γ₀(N), the centre being absorbed.
• HeckeRing.GL2.Delta0_le_commensurator_Gamma0Image: Δ₀(N) lies in the commensurator of Γ₀(N).
• HeckeRing.GL2.out_mem_glpos_of_delta0: the chosen representative of a double coset of Δ₀(N) has positive determinant, for any pair of flanking subgroups — the positivity hypothesis every level's Hecke operators carry.
• the IsHeckeTriple (Delta0 N) ((Gamma0 N).map (mapGL ℚ)) ((Gamma0 N).map (mapGL ℚ)) instance, stated in the unfolded spelling that the modular-form side uses.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.3.

noncomputable def HeckeRing.GL2.Gamma0Image (N : ℕ) : Subgroup (GL (Fin 2) ℚ)

The image of Γ₀(N) in GL₂(ℚ).

Equations

• HeckeRing.GL2.Gamma0Image N = Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)

@[simp]

theorem HeckeRing.GL2.mem_Gamma0Image_iff (N : ℕ) {g : GL (Fin 2) ℚ} : g ∈ Gamma0Image N ↔ ∃ σ ∈ CongruenceSubgroup.Gamma0 N, (Matrix.SpecialLinearGroup.mapGL ℚ) σ = g

Membership in the image of Γ₀(N), by an integral witness.

theorem HeckeRing.GL2.Gamma0Image_def (N : ℕ) : Gamma0Image N = Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)

Gamma0Image N unfolded. Stated here, in the file where the definition lives, because downstream modules cannot see through the def: without this lemma a containment proved for Gamma0Image N cannot be reused where (Gamma0 N).map (mapGL ℚ) is expected.

theorem HeckeRing.GL2.Gamma0Image_le_Delta0 (N : ℕ) : (Gamma0Image N).toSubmonoid ≤ Delta0 N

Γ₀(N) ≤ Δ₀(N): an element of Γ₀(N) has ad ≡ 1 modulo N, since c ≡ 0 and the determinant is one, so its upper-left entry is a unit — which is exactly what Δ₀(N) asks. This containment is also what puts the diamond operators into the Hecke ring of Γ₁(N).

theorem HeckeRing.GL2.mapGL_mem_Delta0 (N : ℕ) (γ : ↥(CongruenceSubgroup.Gamma0 N)) : (Matrix.SpecialLinearGroup.mapGL ℚ) ↑γ ∈ Delta0 N

Γ₀(N) lands in Δ₀(N): its elements are integral of determinant one, with lower-left entry divisible by N and upper-left entry a unit because ad ≡ 1.

theorem HeckeRing.GL2.map_withCenter_le_Delta0 (N : ℕ) {H : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hH : H ≤ CongruenceSubgroup.Gamma0 N) : (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) H.withCenter).toSubmonoid ≤ Delta0 N

H·{±I} ≤ Δ₀(N) for any H ≤ Γ₀(N), transported to the images in GL₂(ℚ). Adjoining the centre costs nothing on the Δ₀(N) side, because Γ₀(N) already contains -I and so absorbs the central factor; withCenter_le_Gamma0 is that step. This is what puts the enlarged group Γ₁(N)·{±I} — the one the Petersson layer sums over — into the same Hecke triple.

theorem HeckeRing.GL2.out_mem_glpos_of_delta0 (N : ℕ) {Γ₁ Γ₂ : Subgroup (GL (Fin 2) ℚ)} (D : HeckeCoset (Delta0 N) Γ₁ Γ₂) : ↑(Quotient.out D) ∈ Matrix.GLPos (Fin 2) ℚ

The chosen representative of a double coset of Δ₀(N) has positive determinant, whatever the two flanking subgroups: Δ₀(N) consists of integral matrices of positive determinant. This is the positivity hypothesis the Hecke operators on modular forms of level N carry, discharged once for this semigroup.

Nothing here mentions Γ₀(N): the lemma is about Δ₀(N) and is generic in both flanks. It sits in this file because this is the earliest point where Δ₀(N) and the double-coset API are both in scope, so every level — Γ₀(N), Γ₁(N), and any other flank — reaches it without importing a sibling level's file. It is stated above the [NeZero N] variable deliberately: the proof never needs N to be nonzero.

theorem HeckeRing.GL2.Delta0_le_commensurator_Gamma0Image (N : ℕ) [NeZero N] : Delta0 N ≤ (Subgroup.Commensurable.commensurator (Gamma0Image N)).toSubmonoid

Δ₀(N) lies in the commensurator of Γ₀(N), the right-hand half of its Hecke triple.

instance HeckeRing.GL2.instIsHeckeTripleGeneralLinearGroupFinOfNatNatRatDelta0MapSpecialLinearGroupIntMapGLGamma0 (N : ℕ) [NeZero N] : IsHeckeTriple (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The Hecke triple of Γ₀(N): Γ₀(N) ≤ Δ₀(N) ≤ commensurator(Γ₀(N)) inside GL₂(ℚ) — the setting of Shimura §3.3, in which the Hecke ring R(Γ₀(N), Δ₀(N)) is formed.

Stated on the unfolded (Gamma0 N).map (mapGL ℚ), matching the Γ₁(N) instance: the modular-form side writes the level as (Gamma0 N).map (mapGL ℝ), and its rational companion arrives in the same shape, which is the form instance search looks for.