The Hecke triple of Γ₁(N)

The submonoid Δ₀(N) ⊆ GL₂(ℚ) of integral matrices with positive determinant that are upper-triangular modulo N with unit upper-left entry, and the Hecke triple it forms with the image of the congruence subgroup Γ₁(N). This is the level-N counterpart of the arithmetic triple (Δₙ, SL_n(ℤ)), and the setting in which the Hecke operators on M_k(Γ₁(N)) live.

Δ₀(N) is the classical semigroup of Miyake, Modular Forms, §4.5: integral, of positive determinant, with c ≡ 0 and a coprime to N, the coprimality spelled here as IsUnit (a : ZMod N). Asking the upper-left entry to be a unit rather than ≡ 1 is what makes Γ₀(N) ≤ Δ₀(N), so that the resulting Hecke ring carries the diamond operators alongside the T_p: an element of Γ₀(N) has ad ≡ 1 modulo N, hence unit a, but a ≡ 1 only for the elements of Γ₁(N) itself. The smaller classical semigroup Δ₁(N), cut out by a ≡ 1, is the sub-semigroup carrying the T_p alone.

Determinants divisible by N are deliberately admitted: diag(1, p) lies in Δ₀(N) even when p ∣ N, where it gives the bad-prime operator U_p. Because of this, the whole determinant-n part of Δ₀(N) is the full diamond orbit of the classical T_n, not T_n itself; an operator defined downstream must be cut out of the a ≡ 1 part rather than taken as that entire fibre.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/Gamma1Pair.lean, Chris Birkbeck).

Main definitions

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

Main results

• HeckeRing.GL2.Gamma1Image_le_Gamma0Image: Γ₁(N) ≤ Γ₀(N) in GL₂(ℚ).
• HeckeRing.GL2.Gamma1Image_le_Delta0: Γ₁(N) ≤ Δ₀(N), the special case of the Γ₀ result.
• HeckeRing.GL2.Delta0_le_commensurator_Gamma1Image: Δ₀(N) lies in the commensurator of Γ₁(N).
• the IsHeckeTriple (Delta0 N) ((Gamma1 N).map (mapGL ℚ)) ((Gamma1 N).map (mapGL ℚ)) instance.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Chapter 3.

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

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

Equations

• HeckeRing.GL2.Gamma1Image N = Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N)

@[simp]

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

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

theorem HeckeRing.GL2.Gamma1Image_le_Gamma0Image (N : ℕ) : Gamma1Image N ≤ Gamma0Image N

Γ₁(N) ≤ Γ₀(N), transported to the images in GL₂(ℚ).

theorem HeckeRing.GL2.Gamma1Image_le_Delta0 (N : ℕ) : (Gamma1Image N).toSubmonoid ≤ Delta0 N

Γ₁(N) ≤ Δ₀(N): the special case of Gamma0Image_le_Delta0 at the smaller group, since Γ₁(N) ≤ Γ₀(N).

theorem HeckeRing.GL2.commensurable_Gamma1Image_SLnZ (N : ℕ) [NeZero N] : (Gamma1Image N).Commensurable (GLn.SLnZ 2)

Γ₁(N) is commensurable with SL₂(ℤ): it has finite index in it.

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

Δ₀(N) lies in the commensurator of Γ₁(N): it lies in that of SL₂(ℤ), and the two groups are commensurable.

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

The Hecke triple of Γ₁(N): Γ₁(N) ≤ Δ₀(N) ≤ commensurator(Γ₁(N)) inside GL₂(ℚ) — the setting of the Hecke operators on modular forms of level N.

Stated at the unfolded (Gamma1 N).map (mapGL ℚ) rather than at Gamma1Image N: instance search unfolds neither, and the unfolded spelling is the one consumers meet, since the level of a modular form of level N is written (Gamma1 N).map (mapGL ℝ) and its rational companion arrives in the same shape.