The semigroup Δ₀(N)

The submonoid Δ₀(N) ⊆ GL₂(ℚ) of integral matrices with positive determinant that are upper-triangular modulo N with unit upper-left entry. It is the Δ of the Hecke triples of both Γ₀(N) and Γ₁(N), and nothing about it refers to either group, so it lives here rather than inside one of the two triple modules.

Δ₀(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 Hecke ring of Γ₁(N) carries the diamond operators alongside the T_p. 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), with CoprimeDet and coprimeDet_iff from the CoprimeDet section of LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/Props.lean, and exists_primitive_content_quotient from Gamma0_content_quotient of LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/AtkinLehner.lean (all Chris Birkbeck).

Main definitions

• HeckeRing.GL2.Delta0: the submonoid Δ₀(N).

Main results

• HeckeRing.GL2.mem_Delta0_iff: membership, unfolded.
• HeckeRing.GL2.CoprimeDet, HeckeRing.GL2.coprimeDet_iff: the elements whose integral representative has determinant coprime to N, and the fact that one witness decides it.
• HeckeRing.GL2.Delta0_le_posDetInt: Δ₀(N) consists of integral matrices of positive determinant, which is what puts it in the commensurator of SL₂(ℤ).
• HeckeRing.GL2.Delta0_le_commensurator_map: and therefore in the commensurator of the image of any finite-index subgroup of SL₂(ℤ) — the half of a Hecke triple that does not depend on which congruence subgroup is being used.
• HeckeRing.GL2.exists_primitive_content_quotient: dividing a matrix of the Δ₀(N) shape by the gcd of its entries leaves a primitive matrix of the same shape.

References

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

noncomputable def HeckeRing.GL2.Delta0 (N : ℕ) : Submonoid (GL (Fin 2) ℚ)

Δ₀(N): integral matrices of positive determinant that are upper-triangular modulo N with unit upper-left entry, i.e. c ≡ 0 (mod N) and a a unit in ZMod N. The unit condition (rather than a ≡ 1) is what makes Γ₀(N) ≤ Δ₀(N).

Equations

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

@[simp]

theorem HeckeRing.GL2.mem_Delta0_iff (N : ℕ) {g : GL (Fin 2) ℚ} : g ∈ Delta0 N ↔ ∃ (A : Matrix (Fin 2) (Fin 2) ℤ), ↑g = A.map Int.cast ∧ 0 < (↑g).det ∧ ↑N ∣ A 1 0 ∧ IsUnit ↑(A 0 0)

Membership in Δ₀(N), unfolded.

def HeckeRing.GL2.CoprimeDet (N : ℕ) (g : ↥(Delta0 N)) : Prop

An element of Δ₀(N) has coprime determinant when every integral matrix representing it has determinant coprime to N.

Quantifying over all representatives rather than choosing one keeps the predicate free of a choice; the representative is unique anyway, since ℤ → ℚ is injective.

Equations

• HeckeRing.GL2.CoprimeDet N g = ∀ (A : Matrix (Fin 2) (Fin 2) ℤ), ↑↑g = A.map Int.cast → A.det.gcd ↑N = 1

theorem HeckeRing.GL2.coprimeDet_iff (N : ℕ) {g : ↥(Delta0 N)} {A : Matrix (Fin 2) (Fin 2) ℤ} (hA : ↑↑g = A.map Int.cast) : CoprimeDet N g ↔ A.det.gcd ↑N = 1

CoprimeDet is decided by any single integral witness: the witness is unique, because the entrywise cast ℤ → ℚ is injective. This is the introduction rule for the definition, whose universal quantifier only eliminates.

The upper-left unit character

noncomputable def HeckeRing.GL2.Delta0UpperUnit (N : ℕ) : ↥(Delta0 N) →* (ZMod N)ˣ

The upper-left unit character of Δ₀(N), reducing the upper-left entry of an integral witness modulo N. It is multiplicative because the lower-left entry of a Δ₀(N) matrix vanishes mod N, killing the cross term in the product.

Equations

• HeckeRing.GL2.Delta0UpperUnit N = { toFun := fun (g : ↥(HeckeRing.GL2.Delta0 N)) => ⋯.unit, map_one' := ⋯, map_mul' := ⋯ }

theorem HeckeRing.GL2.Delta0UpperUnit_apply_val (N : ℕ) {g : ↥(Delta0 N)} {A : Matrix (Fin 2) (Fin 2) ℤ} (hA : ↑↑g = A.map Int.cast) : ↑((Delta0UpperUnit N) g) = ↑(A 0 0)

The eliminator. Any integral witness computes the upper-left unit, so a consumer never has to reach for the chosen one.

Not @[simp]: A occurs only in the hypothesis and the right-hand side, so simp cannot infer it — the same reason diamondOp_apply_of_mem_modFormCharSpace is not a simp lemma.

theorem HeckeRing.GL2.Delta0_le_posDetInt (N : ℕ) : Delta0 N ≤ GLn.posDetInt 2

Δ₀(N) consists of integral matrices with positive determinant.

theorem HeckeRing.GL2.Delta0_le_intEntries (N : ℕ) : Delta0 N ≤ GLn.intEntries 2

Δ₀(N) consists of matrices with integer entries: Delta0_le_posDetInt with the positivity forgotten.

theorem HeckeRing.GL2.Delta0_le_commensurator_map (N : ℕ) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [Γ.FiniteIndex] : Delta0 N ≤ (Subgroup.Commensurable.commensurator (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) Γ)).toSubmonoid

Δ₀(N) lies in the commensurator of the image of any finite-index subgroup of SL₂(ℤ).

This is the right-hand half of the Hecke triple Γ ≤ Δ₀(N) ≤ commensurator(Γ.map (mapGL ℚ)), and it holds for every finite-index Γ ≤ SL₂(ℤ): nothing about the subgroup enters beyond its index. Shimura's Lemma 3.10.

theorem HeckeRing.GL2.exists_primitive_content_quotient (N : ℕ) (A : Matrix (Fin 2) (Fin 2) ℤ) (hA_det_pos : 0 < A.det) (hAN : ↑N ∣ A 1 0) (hAco : (A 0 0).gcd ↑N = 1) (d : ℕ) (hd_is_gcd : d = ((A 0 0).natAbs.gcd (A 0 1).natAbs).gcd ((A 1 0).natAbs.gcd (A 1 1).natAbs)) : ∃ (A₀ : Matrix (Fin 2) (Fin 2) ℤ), (∀ (i j : Fin 2), A i j = ↑d * A₀ i j) ∧ 0 < A₀.det ∧ ↑N ∣ A₀ 1 0 ∧ (A₀ 0 0).gcd ↑N = 1 ∧ ∀ (q : ℕ), Nat.Prime q → ¬(↑q ∣ A₀ 0 0 ∧ ↑q ∣ A₀ 0 1 ∧ ↑q ∣ A₀ 1 0 ∧ ↑q ∣ A₀ 1 1)

Content factorisation for the Δ₀(N) shape. Dividing an integral matrix by the gcd d of its entries leaves a primitive matrix — one no prime divides entrywise — that still has positive determinant, N ∣ c, and upper-left entry coprime to N.

The Δ₀(N) conditions survive the division because d is coprime to N: it divides A 0 0, which is coprime to N by hypothesis. This is the reduction step that lets a statement about Δ₀(N) double cosets be proved for primitive representatives first.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/AtkinLehner.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB), where it is Gamma0_content_quotient.