Congruence subgroups: the pair Γ₁(N) ⊴ Γ₀(N), the index of Γ₀(pᵏ), and the level

Foundational results about the pair Γ₁(N) ≤ Γ₀(N) beyond Mathlib's Mathlib.NumberTheory.ModularForms.CongruenceSubgroups: Γ₀(N) normalizes Γ₁(N) (also after mapping to GL₂(S), over any commutative ring S), the ratio of two Γ₀(N)-elements with equal lower-right entry lies in Γ₁(N), the lower-right-entry map Γ₀(N) →* (ZMod N)ˣ is surjective, and the location of -I: it always lies in Γ₀(N), with lower-right entry the unit -1, and it lies in Γ₁(N) exactly when N ∣ 2; and every power of the translation matrix T lies in Γ₁(N), at every level. The file then computes the index of Γ₀ at prime-power levels — the degree count of Shimura, Theorem 3.24 — which lives here because it is congruence-subgroup arithmetic consumed by, but independent of, the Hecke-ring layer.

A final section records how the principal congruence subgroups compose with the arithmetic of the level: Γ is antitone in the level like the other two families, it sits inside those two at the same level along the chain Γ(N) ≤ Γ₁(N) ≤ Γ₀(N), and the join of two of them is the principal congruence subgroup of the gcd, Γ(gcd a b) = Γ(a) ⊔ Γ(b). That identity is Shimura's Lemma 3.28; it is the Chinese remainder theorem for SL₂, and it is what lets a Hecke operator at level ab be analysed one prime at a time.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/Gamma1Pair.lean, for the index section LeanModularForms/HeckeRIngs/GL2/CongruenceIndex.lean, for the level-antitonicity lemmas LeanModularForms/HeckeRIngs/GL2/LevelEmbed.lean, and for the gcd decomposition LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/Foundation.lean, all Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), extracted from TauCeti/NumberTheory/ModularForms/DiamondOperators.lean as congruence-subgroup infrastructure independent of the diamond operators.

Main results

• CongruenceSubgroup.Gamma1_le_Gamma1_of_dvd, CongruenceSubgroup.Gamma0_le_Gamma0_of_dvd, CongruenceSubgroup.Gamma_le_Gamma_of_dvd: all three families are antitone in the level, Γ(N) ≤ Γ(M) whenever M ∣ N.
• CongruenceSubgroup.Gamma_le_Gamma1, CongruenceSubgroup.Gamma_le_Gamma0: at a fixed level the three families are nested, Γ(N) ≤ Γ₁(N) ≤ Γ₀(N).
• CongruenceSubgroup.mem_Gamma0_iff_dvd: Γ₀(N) membership read as the integer divisibility (N : ℤ) ∣ A 1 0 rather than as a ZMod N congruence, for a proof that wants to name the quotient. Valid at every level, N = 0 included.
• CongruenceSubgroup.mem_Gamma1_iff: Γ₁(N) is cut out inside Γ₀(N) by the single congruence d ≡ 1.
• CongruenceSubgroup.mem_Gamma1_iff_dvd_lowerRow: Γ₁(N) membership read as the two integer divisibilities (N : ℤ) ∣ c and (N : ℤ) ∣ d - 1 on the lower row, the Γ₁ counterpart of mem_Gamma0_iff_dvd.
• CongruenceSubgroup.isUnit_intCast_apply_zero_zero_of_mem_Gamma0: a Γ₀(N) matrix has unit upper-left entry modulo N.
• CongruenceSubgroup.intCast_apply_zero_zero_mul_apply_one_one_of_mem_Gamma0: modulo its level, a Γ₀(N) matrix has mutually inverse diagonal entries.
• CongruenceSubgroup.intCast_apply_zero_zero_add_natCast_mul_apply_one_zero_of_mem_Gamma0 and CongruenceSubgroup.isUnit_intCast_apply_zero_zero_add_natCast_mul_apply_one_zero_of_mem_Gamma0: shearing the first column by a natural-number multiple of the lower-left entry changes nothing modulo the level, so the sheared entry is a unit too.
• CongruenceSubgroup.mem_Gamma1_iff_toHomUnits_eq_one: inside Γ₀(N), Γ₁(N) is the kernel of the unit-valued lower-right entry.
• CongruenceSubgroup.Gamma0_normalizes_Gamma1 and CongruenceSubgroup.Gamma0_le_normalizer_Gamma1: conjugation by Γ₀(N) preserves Γ₁(N).
• CongruenceSubgroup.Gamma1_map_le_Gamma0_map: the inclusion Γ₁(N) ≤ Γ₀(N) after mapping to GL₂(ℝ).
• CongruenceSubgroup.Gamma1_map_le_Gamma1_map_of_dvd: the antitonicity Γ₁(N) ≤ Γ₁(M) for M ∣ N, after mapping to GL₂(ℝ).
• CongruenceSubgroup.mapGL_mem_normalizer_Gamma1_map and CongruenceSubgroup.Gamma1_map_inv_conjAct_eq: (Gamma1 N).map (mapGL S) is invariant under conjugation by Γ₀(N) elements in GL₂(S), over any commutative ring S, stated as normalizer membership and — over ℝ — as a pointwise conjugation. CongruenceSubgroup.conjAct_mapGL_mul_smul_Gamma1 is the corresponding level-transfer rule after multiplying an arbitrary real matrix on the left.
• CongruenceSubgroup.Gamma0Map_toHomUnits_surjective: every unit of ZMod N is the lower-right entry of a matrix in Γ₀(N) (via strong approximation for SL₂).
• CongruenceSubgroup.exists_mem_Gamma_map_intCast_zmod_eq: strong approximation along a coprime level — for coprime d and d', Γ(d') still surjects onto SL₂(ℤ/dℤ).
• CongruenceSubgroup.gamma0Twist: an explicit Γ₀(N) element whose lower-right entry is any natural number coprime to N.
• CongruenceSubgroup.gamma0TwistOfUnit and CongruenceSubgroup.Gamma0Map_toHomUnits_gamma0TwistOfUnit: the Bézout twist taken at a representative of a unit u is a Γ₀(N) element whose nebentypus label is exactly u — the constructive counterpart of Gamma0Map_toHomUnits_surjective, which gives no control over the entries. Its bottom row is (N, (u : ZMod N).val), by CongruenceSubgroup.gamma0TwistOfUnit_apply_one_zero and CongruenceSubgroup.gamma0TwistOfUnit_apply_one_one.
• CongruenceSubgroup.neg_one_mem_Gamma0 and CongruenceSubgroup.Gamma0Map_toHomUnits_negOne: -I ∈ Γ₀(N), with lower-right entry the unit -1; CongruenceSubgroup.neg_one_mem_Gamma1_iff: -I ∈ Γ₁(N) ↔ N ∣ 2.
• CongruenceSubgroup.withCenter_le_Gamma0: adjoining the centre of SL₂(ℤ) to a subgroup of Γ₀(N) keeps it inside Γ₀(N), since Γ₀(N) already contains -I.
• CongruenceSubgroup.Gamma0_prime_index: [SL₂(ℤ) : Γ₀(p)] = p + 1 for prime p.
• CongruenceSubgroup.Gamma0_relIndex_pow_succ: [Γ₀(pᵏ) : Γ₀(p^(k+1))] = p for 0 < p and 0 < k.
• CongruenceSubgroup.Gamma0_prime_power_index: [SL₂(ℤ) : Γ₀(pᵏ)] = p^(k-1) * (p + 1) for prime p and k ≥ 1.
• CongruenceSubgroup.Gamma_gcd_eq_sup: Γ(gcd a b) = Γ(a) ⊔ Γ(b) — Shimura's Lemma 3.28, the Chinese remainder theorem for SL₂.
• CongruenceSubgroup.intCast_mul_apply_one_zero_eq_zero_of_mem_Gamma0_div and CongruenceSubgroup.intCast_apply_one_one_eq_of_mem_Gamma0_of_eq: entry congruences for elements of Γ₀, the shapes the descent factorisations produce.
• CongruenceSubgroup.Gamma_lcm_eq_inf: Γ(lcm a b) = Γ(a) ⊓ Γ(b), with the coprime case CongruenceSubgroup.Gamma_mul_eq_inf_of_coprime.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Lemma 3.28 and Theorem 3.24.

theorem CongruenceSubgroup.Gamma1_le_Gamma1_of_dvd {M N : ℕ} (h : M ∣ N) : Gamma1 N ≤ Gamma1 M

Γ₁ is antitone in the level: if M ∣ N then Γ₁(N) ≤ Γ₁(M), since reducing the congruences a ≡ d ≡ 1, c ≡ 0 modulo N along ZMod N → ZMod M gives them modulo M.

theorem CongruenceSubgroup.Gamma_le_Gamma_of_dvd {M N : ℕ} (h : M ∣ N) : Gamma N ≤ Gamma M

Γ is antitone in the level: if M ∣ N then Γ(N) ≤ Γ(M). Reduction modulo M factors through reduction modulo N, so a matrix congruent to the identity modulo N is congruent to the identity modulo M. CongruenceSubgroup.Gamma1_le_Gamma1_of_dvd and CongruenceSubgroup.Gamma0_le_Gamma0_of_dvd are the corresponding statements for the other two families.

theorem CongruenceSubgroup.Gamma_le_Gamma1 (N : ℕ) : Gamma N ≤ Gamma1 N

Γ(N) ≤ Γ₁(N): the principal congruence subgroup sits inside Γ₁(N), since the three congruences a ≡ 1, d ≡ 1, c ≡ 0 that Γ₁(N) imposes are three of the four that Γ(N) does.

theorem CongruenceSubgroup.Gamma_le_Gamma0 (N : ℕ) : Gamma N ≤ Gamma0 N

Γ(N) ≤ Γ₀(N): the principal congruence subgroup sits inside Γ₀(N), along the chain Γ(N) ≤ Γ₁(N) ≤ Γ₀(N).

theorem CongruenceSubgroup.mem_Gamma0_iff_dvd {N : ℕ} {A : Matrix.SpecialLinearGroup (Fin 2) ℤ} : A ∈ Gamma0 N ↔ ↑N ∣ ↑A 1 0

Γ₀(N) membership as an integer divisibility. CongruenceSubgroup.Gamma0_mem states it as a congruence in ZMod N; this is the same fact with the congruence already discharged into (N : ℤ) ∣ A 1 0, which is the form a proof needs whenever it wants to name the quotient.

It holds at every level, N = 0 included, where both sides say A 1 0 = 0.

theorem CongruenceSubgroup.Gamma0_le_Gamma0_of_dvd {M N : ℕ} (h : M ∣ N) : Gamma0 N ≤ Gamma0 M

Γ₀ is antitone in the level: if M ∣ N then Γ₀(N) ≤ Γ₀(M).

theorem CongruenceSubgroup.mem_Gamma1_iff {N : ℕ} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} : γ ∈ Gamma1 N ↔ γ ∈ Gamma0 N ∧ ↑(↑γ 1 1) = 1

Γ₁(N) is the fibre of Gamma0Map over 1. A matrix lies in Γ₁(N) exactly when it lies in Γ₀(N) and its lower-right entry is 1 modulo N; the congruence a ≡ 1 that CongruenceSubgroup.Gamma1_mem also asks for is then forced by the determinant. This is the form in which membership is checked whenever a construction produces a Γ₀(N) matrix and controls only its lower-right entry.

theorem CongruenceSubgroup.mem_Gamma1_iff_dvd_lowerRow {N : ℕ} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} : γ ∈ Gamma1 N ↔ ↑N ∣ ↑γ 1 0 ∧ ↑N ∣ ↑γ 1 1 - 1

Γ₁(N) membership is exactly two divisibilities on the lower row, (N : ℤ) ∣ c and (N : ℤ) ∣ d - 1: mem_Gamma1_iff with both conditions read in ℤ, as mem_Gamma0_iff_dvd reads Gamma0_mem. The congruence a ≡ 1 is forced by the determinant, so it is omitted. Integer divisibilities are the form an explicitly constructed matrix has; mem_Gamma1_of_dvd_lowerRow is the unbundled mpr.

theorem CongruenceSubgroup.mem_Gamma1_of_dvd_lowerRow {N : ℕ} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (h10 : ↑N ∣ ↑γ 1 0) (h11 : ↑N ∣ ↑γ 1 1 - 1) : γ ∈ Gamma1 N

Γ₁(N) membership from two divisibilities on the lower row, the mpr direction of mem_Gamma1_iff_dvd_lowerRow with the conjunction unbundled — the shape a construction that has just built an explicit matrix wants to apply. When the two divisibilities arrive as one conjunction, pass it to mem_Gamma1_iff_dvd_lowerRow.mpr directly rather than destructuring it.

theorem CongruenceSubgroup.intCast_apply_zero_zero_mul_apply_one_one_of_mem_Gamma0 {M : ℕ} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ Gamma0 M) : ↑(↑γ 0 0) * ↑(↑γ 1 1) = 1

The diagonal entries of a Γ₀(M) matrix are mutually inverse modulo M: the determinant identity ad - bc = 1 with the bc term killed by M ∣ c. It refines CongruenceSubgroup.isUnit_intCast_apply_zero_zero_of_mem_Gamma0 by naming the inverse.

theorem CongruenceSubgroup.isUnit_intCast_apply_zero_zero_of_mem_Gamma0 {N : ℕ} {σ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hσ : σ ∈ Gamma0 N) : IsUnit ↑(↑σ 0 0)

The upper-left entry of a Γ₀(N) matrix is a unit modulo N: the determinant is one and the lower-left entry vanishes modulo N, so ad ≡ 1.

@[simp]

theorem CongruenceSubgroup.intCast_apply_zero_zero_add_natCast_mul_apply_one_zero_of_mem_Gamma0 {N : ℕ} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ Gamma0 N) (j : ℕ) : ↑(↑γ 0 0) + ↑j * ↑(↑γ 1 0) = ↑(↑γ 0 0)

The first column of a Γ₀(N) matrix collapses under a natural-number shear: a + j c ≡ a modulo N for every j : ℕ, because c ≡ 0. Stated with the casts already distributed, since that — not the cast of the sum — is the simp normal form.

theorem CongruenceSubgroup.isUnit_intCast_apply_zero_zero_add_natCast_mul_apply_one_zero_of_mem_Gamma0 {N : ℕ} {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ Gamma0 N) (j : ℕ) : IsUnit ↑(↑γ 0 0 + ↑j * ↑γ 1 0)

The sheared entry is still a unit, for every j : ℕ: it is the upper-left entry modulo N, which isUnit_intCast_apply_zero_zero_of_mem_Gamma0 knows to be a unit.

theorem CongruenceSubgroup.Gamma0_normalizes_Gamma1 {N : ℕ} (g : ↥(Gamma0 N)) (h : Matrix.SpecialLinearGroup (Fin 2) ℤ) (hh : h ∈ Gamma1 N) : ↑g * h * (↑g)⁻¹ ∈ Gamma1 N

Conjugation by a Gamma0 N element preserves Gamma1 N. This is the foundation for the diamond operator ⟨d⟩ on modular forms.

theorem CongruenceSubgroup.Gamma0_le_normalizer_Gamma1 (N : ℕ) : Gamma0 N ≤ Subgroup.normalizer ↑(Gamma1 N)

Γ₀(N) lies in the normaliser of Γ₁(N): the statement of Gamma0_normalizes_Gamma1 in the form the coset combinatorics of the Petersson product consumes.

theorem CongruenceSubgroup.Gamma1_map_le_Gamma0_map (N : ℕ) : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma1 N) ≤ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma0 N)

The inclusion Γ₁(N) ≤ Γ₀(N), transported to GL₂(ℝ).

theorem CongruenceSubgroup.Gamma1_map_le_Gamma1_map_of_dvd {M N : ℕ} (h : M ∣ N) : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma1 N) ≤ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma1 M)

The antitonicity Γ₁(N) ≤ Γ₁(M) for M ∣ N, transported to GL₂(ℝ). This is the inclusion along which a form of level M is read as a form of level N.

theorem CongruenceSubgroup.mapGL_mem_normalizer_Gamma1_map {N : ℕ} (S : Type u_1) [CommRing S] (g : ↥(Gamma0 N)) : (Matrix.SpecialLinearGroup.mapGL S) ↑g ∈ Subgroup.normalizer ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL S) (Gamma1 N))

Γ₀(N) normalizes Γ₁(N) after mapping to GL₂(S), for any commutative ring S. This is Gamma0_normalizes_Gamma1 transported along the monoid homomorphism mapGL S: the conjugate of an integral witness is again one.

The ring is arbitrary because both rings occur: the slash action of a modular form lives over ℝ, while the Hecke triples of Γ₀(N) and Γ₁(N) live over ℚ.

theorem CongruenceSubgroup.Gamma1_map_inv_conjAct_eq {N : ℕ} (g : ↥(Gamma0 N)) : ConjAct.toConjAct ((Matrix.SpecialLinearGroup.mapGL ℝ) ↑g)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma1 N) = Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma1 N)

(Gamma1 N).map (mapGL ℝ) is invariant under conjugation by Gamma0 N elements in GL₂(ℝ): the pointwise-conjugation form of mapGL_mem_normalizer_Gamma1_map.

theorem CongruenceSubgroup.conjAct_mapGL_mul_smul_Gamma1 {N : ℕ} {A : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hA : A ∈ Gamma0 N) (x : GL (Fin 2) ℝ) : ConjAct.toConjAct ((Matrix.SpecialLinearGroup.mapGL ℝ) A * x)⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma1 N) = ConjAct.toConjAct x⁻¹ • Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (Gamma1 N)

Left multiplication by an element of Γ₀(N) does not change the conjugated real Γ₁(N)-level.

theorem CongruenceSubgroup.mul_inv_mem_Gamma1_of_Gamma0Map_eq {N : ℕ} (g₁ g₂ : ↥(Gamma0 N)) (heq : (Gamma0Map N) g₁ = (Gamma0Map N) g₂) : ↑g₁ * (↑g₂)⁻¹ ∈ Gamma1 N

If two Γ₀(N) elements have equal image under Gamma0Map, their ratio g₁ · g₂⁻¹ lies in Γ₁(N) (as an SL₂(ℤ) element).

theorem CongruenceSubgroup.mul_inv_mem_Gamma1_iff_Gamma0Map_eq {N : ℕ} (g₁ g₂ : ↥(Gamma0 N)) : ↑g₁ * (↑g₂)⁻¹ ∈ Gamma1 N ↔ (Gamma0Map N) g₁ = (Gamma0Map N) g₂

Two Γ₀(N) elements have the same lower-right entry exactly when their ratio lies in Γ₁(N). The mpr direction is mul_inv_mem_Gamma1_of_Gamma0Map_eq; the converse reads the membership back through Gamma1_mem', which says that Gamma0Map N is trivial on Γ₁(N).

theorem CongruenceSubgroup.Gamma0Map_apply {N : ℕ} (g : ↥(Gamma0 N)) : (Gamma0Map N) g = ↑(↑↑g 1 1)

The value of Mathlib's Gamma0Map: the lower-right entry of the matrix, reduced mod N.

Gamma0Map is a bare MonoidHom.mk, so this holds definitionally; naming it keeps that one definitional step out of the simp sets that consume it, and gives downstream files a lemma to rewrite with instead of unfolding the definition.

theorem CongruenceSubgroup.mem_Gamma1_iff_toHomUnits_eq_one {N : ℕ} (g : ↥(Gamma0 N)) : ↑g ∈ Gamma1 N ↔ (Gamma0Map N).toHomUnits g = 1

An element of Γ₀(N) lies in Γ₁(N) exactly when its diamond label is 1: mem_Gamma1_iff read through the unit-valued lower-right entry (Gamma0Map N).toHomUnits.

theorem CongruenceSubgroup.Gamma0Map_toHomUnits_surjective {N : ℕ} : Function.Surjective ⇑(Gamma0Map N).toHomUnits

(Gamma0Map N).toHomUnits is surjective: every unit u ∈ (ZMod N)ˣ is realized as the lower-right entry of some g ∈ Gamma0 N, by strong approximation for SL₂.

noncomputable def CongruenceSubgroup.gamma0Twist (N p : ℕ) (h : p.Coprime N) : Matrix.SpecialLinearGroup (Fin 2) ℤ

A Bézout matrix with bottom row (N, p), for p coprime to N.

Equations

• CongruenceSubgroup.gamma0Twist N p h = ⋯.choose

@[simp]

theorem CongruenceSubgroup.gamma0Twist_apply_one_zero {N p : ℕ} (h : p.Coprime N) : ↑(gamma0Twist N p h) 1 0 = ↑N

The lower-left entry of the Bézout twist is N.

@[simp]

theorem CongruenceSubgroup.gamma0Twist_apply_one_one {N p : ℕ} (h : p.Coprime N) : ↑(gamma0Twist N p h) 1 1 = ↑p

The lower-right entry of the Bézout twist is p.

theorem CongruenceSubgroup.gamma0Twist_mem_Gamma0 {N p : ℕ} (h : p.Coprime N) : gamma0Twist N p h ∈ Gamma0 N

The Bézout twist lies in Γ₀(N).

theorem CongruenceSubgroup.Gamma0Map_toHomUnits_gamma0Twist {N p : ℕ} (h : p.Coprime N) : (Gamma0Map N).toHomUnits ⟨gamma0Twist N p h, ⋯⟩ = ZMod.unitOfCoprime p h

The unit-valued lower-right entry of the Bézout twist is the residue class of p.

noncomputable def CongruenceSubgroup.gamma0TwistOfUnit {N : ℕ} (u : (ZMod N)ˣ) : Matrix.SpecialLinearGroup (Fin 2) ℤ

The Bézout twist at a representative of a unit: gamma0Twist at p = (u : ZMod N).val. Its bottom row is (N, (u : ZMod N).val), which is what gamma0TwistOfUnit_apply_one_zero and gamma0TwistOfUnit_apply_one_one record.

Equations

• CongruenceSubgroup.gamma0TwistOfUnit u = CongruenceSubgroup.gamma0Twist N (↑u).val ⋯

@[simp]

theorem CongruenceSubgroup.gamma0TwistOfUnit_apply_one_zero {N : ℕ} (u : (ZMod N)ˣ) : ↑(gamma0TwistOfUnit u) 1 0 = ↑N

The lower-left entry of the Bézout twist at a unit is N.

@[simp]

theorem CongruenceSubgroup.gamma0TwistOfUnit_apply_one_one {N : ℕ} (u : (ZMod N)ˣ) : ↑(gamma0TwistOfUnit u) 1 1 = ↑(↑u).val

The lower-right entry of the Bézout twist at a unit is the chosen representative of u.

theorem CongruenceSubgroup.gamma0TwistOfUnit_mem_Gamma0 {N : ℕ} (u : (ZMod N)ˣ) : gamma0TwistOfUnit u ∈ Gamma0 N

The Bézout twist at a unit lies in Γ₀(N).

@[simp]

theorem CongruenceSubgroup.Gamma0Map_toHomUnits_gamma0TwistOfUnit {N : ℕ} [NeZero N] (u : (ZMod N)ˣ) : (Gamma0Map N).toHomUnits ⟨gamma0TwistOfUnit u, ⋯⟩ = u

The Bézout twist at a representative of u lifts u. The nebentypus reads the lower-right entry, and there that entry is (u : ZMod N).val.

This is the constructive form of Gamma0Map_toHomUnits_surjective: that lemma produces some preimage of u, whereas this one names an explicit matrix whose bottom row is (N, u.val), which is what an argument comparing the entries of two lifts needs.

theorem CongruenceSubgroup.neg_one_mem_Gamma0 {N : ℕ} : -1 ∈ Gamma0 N

-I lies in Γ₀(N): its lower-left entry is 0.

theorem CongruenceSubgroup.withCenter_le_Gamma0 {N : ℕ} {H : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (hH : H ≤ Gamma0 N) : H.withCenter ≤ Gamma0 N

Adjoining the centre keeps a subgroup of Γ₀(N) inside Γ₀(N). The central factor is absorbed: the centre of SL₂(ℤ) is {±I}, and -I already lies in Γ₀(N).

Γ.withCenter is the enlargement that makes "this subgroup contains -I" true, which matters because Γ₁(N) does not contain -I once N ∤ 2; this lemma says the enlargement is free as far as Γ₀(N) is concerned.

def CongruenceSubgroup.Gamma0.negOne (N : ℕ) : ↥(Gamma0 N)

-I ∈ Γ₀(N), packaged as an element of the subgroup. It is the representative through which the diamond operator at -1 is computed.

Equations

• CongruenceSubgroup.Gamma0.negOne N = ⟨-1, ⋯⟩

@[simp]

theorem CongruenceSubgroup.Gamma0.coe_negOne (N : ℕ) : ↑(negOne N) = -1

@[simp]

theorem CongruenceSubgroup.Gamma0Map_negOne {N : ℕ} : (Gamma0Map N) (Gamma0.negOne N) = -1

The lower-right entry of -I ∈ Γ₀(N) is -1.

@[simp]

theorem CongruenceSubgroup.Gamma0Map_toHomUnits_negOne {N : ℕ} : (Gamma0Map N).toHomUnits (Gamma0.negOne N) = -1

The unit-valued lower-right entry of -I ∈ Γ₀(N) is the unit -1.

theorem CongruenceSubgroup.neg_one_mem_Gamma1_iff {N : ℕ} : -1 ∈ Gamma1 N ↔ N ∣ 2

-I lies in Γ₁(N) exactly when N ∣ 2, i.e. for N ∈ {1, 2}. This is the degenerate range in which Γ₁(N) contains -I, so that all odd-weight forms for it vanish.

theorem CongruenceSubgroup.T_zpow_mem_Gamma1 (N : ℕ) (n : ℤ) : ModularGroup.T ^ n ∈ Gamma1 N

Every power of the translation matrix lies in Γ₁(N), at every level. Tⁿ has diagonal (1, 1) and vanishing lower-left entry, so the three congruences of Gamma1_mem hold with no condition on n or N. (In particular the width of the cusp ∞ for Γ₁(N) is 1.)

The index of Γ₀(pᵏ)

The coset representatives of Γ₀(p) in SL₂(ℤ) are TʲS for 0 ≤ j < p together with the identity, giving [SL₂(ℤ) : Γ₀(p)] = p + 1; the relative index of Γ₀(p^(k+1)) in Γ₀(pᵏ) is p via lower-unitriangular representatives, and the tower multiplies to [SL₂(ℤ) : Γ₀(pᵏ)] = p^(k-1)(p + 1) for prime p and k ≥ 1 — the degree count of Shimura, Theorem 3.24.

theorem CongruenceSubgroup.Gamma0_prime_index (p : ℕ) (hp : Nat.Prime p) : (Gamma0 p).index = p + 1

[SL₂(ℤ) : Γ₀(p)] = p + 1 for prime p.

theorem CongruenceSubgroup.Gamma0_relIndex_pow_succ (p : ℕ) (hp : 0 < p) (k : ℕ) (hk : 0 < k) : (Gamma0 (p ^ (k + 1))).relIndex (Gamma0 (p ^ k)) = p

[Γ₀(pᵏ) : Γ₀(p^(k+1))] = p for any positive base p and k ≥ 1.

theorem CongruenceSubgroup.Gamma0_prime_power_index (p : ℕ) (hp : Nat.Prime p) (k : ℕ) (hk : 0 < k) : (Gamma0 (p ^ k)).index = p ^ (k - 1) * (p + 1)

[SL₂(ℤ) : Γ₀(pᵏ)] = p^(k-1) * (p + 1) for prime p and k ≥ 1.

The Chinese-remainder decomposition Γ(gcd a b) = Γ(a) ⊔ Γ(b)

theorem CongruenceSubgroup.Gamma_gcd_eq_sup (a b : ℕ) : Gamma (a.gcd b) = Gamma a ⊔ Gamma b

Shimura, Lemma 3.28. Γ(gcd a b) = Γ(a) ⊔ Γ(b): the join of two principal congruence subgroups is the principal congruence subgroup of the gcd.

The inclusion ⊇ is antitonicity. For ⊆, lift γ ∈ Γ(gcd a b) entrywise: its entries agree with the identity's modulo gcd a b, so the Chinese remainder theorem supplies a matrix M congruent to 1 modulo a and to γ modulo b. Strong approximation (map_intCast_zmod_surjective) realises M mod lcm a b by an actual β ∈ SL₂(ℤ), and then β ∈ Γ(a) while β⁻¹γ ∈ Γ(b), so γ = β · (β⁻¹γ).

theorem CongruenceSubgroup.exists_mem_Gamma_map_intCast_zmod_eq {d d' : ℕ} (hcop : d.Coprime d') (A : Matrix.SpecialLinearGroup (Fin 2) (ZMod d)) : ∃ γ ∈ Gamma d', (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod d))) γ = A

Strong approximation along a coprime level. For coprime d and d', the principal congruence subgroup Γ(d') still surjects onto SL₂(ℤ/dℤ): imposing a congruence condition at d' costs nothing at d.

Entry congruences in Γ₀

theorem CongruenceSubgroup.intCast_mul_apply_one_zero_eq_zero_of_mem_Gamma0_div {p N : ℕ} (hpN : p ∣ N) {δ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hδ : δ ∈ Gamma0 (N / p)) : ↑(↑p * ↑δ 1 0) = 0

The level hypothesis of the factorisation at a divided level. For δ ∈ Γ₀(N / p) with p ∣ N, N = p (N / p) divides p δ₁₀, because N / p ∣ δ₁₀.

theorem CongruenceSubgroup.intCast_apply_one_one_eq_of_mem_Gamma0_of_eq {M : ℕ} {δ α : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hδ : δ ∈ Gamma0 M) {k : ℤ} (h : ↑α 1 1 = ↑δ 1 1 - ↑δ 1 0 * k) : ↑(↑α 1 1) = ↑(↑δ 1 1)

The entry equation reads as a congruence at any level where c vanishes. If a factorisation gives α 1 1 = δ 1 1 - δ 1 0 * k, then modulo a level M with δ ∈ Γ₀(M) the lower-right entry of α is that of δ.

theorem CongruenceSubgroup.Gamma_lcm_eq_inf (a b : ℕ) : Gamma (a.lcm b) = Gamma a ⊓ Gamma b

Γ(lcm a b) = Γ(a) ⊓ Γ(b): a matrix is congruent to the identity modulo two levels exactly when it is modulo their least common multiple.

theorem CongruenceSubgroup.Gamma_mul_eq_inf_of_coprime {a b : ℕ} (hab : a.Coprime b) : Gamma (a * b) = Gamma a ⊓ Gamma b

Γ(a b) = Γ(a) ⊓ Γ(b) for coprime a and b: Gamma_lcm_eq_inf at coprime levels.