Congruence subgroups and Newman forms

Definitions for the normalizers of Γ₀(N) and Γ_Δ(N) in SL₂(ℝ), using Mathlib's congruence subgroups. The integer representatives of Γ_Δ(N) have lower-right entry in Δ. The parameters h and h_Δ record the local square divisors appearing in the normalizer bounds.

Adapted from Filip Najman's normalizer-lean, commit ea4445c0d991a65d54fc77af0af559f2322e8660 (Apache-2.0).

Definitions

def CongruenceNormalizers.Gamma0R (N : ℕ) : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)

Γ₀(N) as a subgroup of SL₂(ℝ): the image of Mathlib's CongruenceSubgroup.Gamma0 N ≤ SL(2, ℤ).

Equations

• CongruenceNormalizers.Gamma0R N = Subgroup.map (Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (CongruenceSubgroup.Gamma0 N)

@[reducible, inline]

abbrev CongruenceNormalizers.Norm0 (N : ℕ) : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)

The normalizer of Γ₀(N) in SL₂(ℝ).

Equations

• CongruenceNormalizers.Norm0 N = Subgroup.normalizer ↑(CongruenceNormalizers.Gamma0R N)

@[reducible, inline]

abbrev CongruenceNormalizers.B (N : ℕ) : Type

B(N) = Norm_{SL₂(ℝ)}(Γ₀(N)) / Γ₀(N).

Equations

• CongruenceNormalizers.B N = (↥(CongruenceNormalizers.Norm0 N) ⧸ (CongruenceNormalizers.Gamma0R N).subgroupOf (CongruenceNormalizers.Norm0 N))

instance CongruenceNormalizers.instNormalSubtypeSpecialLinearGroupFinOfNatNatRealMemSubgroupNorm0SubgroupOfGamma0R (N : ℕ) : ((Gamma0R N).subgroupOf (Norm0 N)).Normal

def CongruenceNormalizers.B.IsClassOf {N : ℕ} (x : B N) (g : Matrix.SpecialLinearGroup (Fin 2) ℝ) : Prop

x : B N is the class of the real matrix g: g normalizes Γ₀(N) and x = g Γ₀(N).

Equations

• x.IsClassOf g = ∃ (hg : g ∈ CongruenceNormalizers.Norm0 N), x = ↑⟨g, hg⟩

noncomputable def CongruenceNormalizers.projSL (A : Matrix (Fin 2) (Fin 2) ℝ) : Matrix.SpecialLinearGroup (Fin 2) ℝ

The image in SL₂(ℝ) of a real 2×2 matrix A of positive determinant: (det A)^{-1/2} • A. Junk value 1 if det A ≤ 0; below it is only applied to matrices of positive determinant.

Equations

• CongruenceNormalizers.projSL A = if hA : 0 < A.det then ⟨(√A.det)⁻¹ • A, ⋯⟩ else 1

def CongruenceNormalizers.hPart (N : ℕ) : ℕ

h(N) = 2^{min(3, ⌊v₂(N)/2⌋)} · 3^{min(1, ⌊v₃(N)/2⌋)}. By hPart_isGreatest this is the largest divisor of 24 whose square divides N.

Equations

• CongruenceNormalizers.hPart N = 2 ^ min 3 (N.factorization 2 / 2) * 3 ^ min 1 (N.factorization 3 / 2)

def CongruenceNormalizers.nPart (N : ℕ) : ℕ

n(N) = N / h(N)².

Equations

• CongruenceNormalizers.nPart N = N / CongruenceNormalizers.hPart N ^ 2

noncomputable def CongruenceNormalizers.S (k : ℕ) : Matrix.SpecialLinearGroup (Fin 2) ℝ

S_k = [[1, 1/k], [0, 1]].

Equations

• CongruenceNormalizers.S k = ⟨!![1, (↑k)⁻¹; 0, 1], ⋯⟩

def CongruenceNormalizers.IsAtkinLehner (N Q : ℕ) (g : Matrix.SpecialLinearGroup (Fin 2) ℝ) : Prop

g is an Atkin–Lehner element w_Q of level N: g = (1/√Q)·[[Qx, y], [Nz, Qw]] with x y z w : ℤ and Q²xw − Nyz = Q. No divisibility is built in: the theorems below add the hypothesis Q ∣ N, which then forces Q ∥ N. That hypothesis is essential: for N = 4, Q = 8 the element (1/√8)·[[0, 1], [−8, 0]] satisfies the equation but does not normalize Γ₀(4). For Q = 0 the predicate is false.

Equations

• CongruenceNormalizers.IsAtkinLehner N Q g = ∃ (x : ℤ) (y : ℤ) (z : ℤ) (w : ℤ), ↑Q ^ 2 * x * w - ↑N * y * z = ↑Q ∧ ↑g = (√↑Q)⁻¹ • !![↑Q * ↑x, ↑y; ↑N * ↑z, ↑Q * ↑w]

def CongruenceNormalizers.IsNewmanFormH (N h : ℕ) (g : Matrix.SpecialLinearGroup (Fin 2) ℝ) : Prop

g has the form of the generalized Newman bound, with parameter h (and n = N/h²): g = ±(1/√e)·[[ae, b/h], [Nc/h, de]] with a b c d : ℤ, e ≥ 1, e ∣ n, ade² − bcn = e. (Together with e ∣ n, the equation forces e ∥ n. The sign ± is there because we work in SL₂(ℝ).) For h = h(N) this is IsNewmanForm N. The statements only use h = h(N) or h = h_Δ, which are ≥ 1 with h² ∣ N, so the divisions by h and the ℕ-division N / h² are exact.

Equations

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

def CongruenceNormalizers.IsNewmanForm (N : ℕ) (g : Matrix.SpecialLinearGroup (Fin 2) ℝ) : Prop

Newman's form with the canonical Γ₀(N) square-divisor parameter.

Equations

• CongruenceNormalizers.IsNewmanForm N g = CongruenceNormalizers.IsNewmanFormH N (CongruenceNormalizers.hPart N) g

noncomputable def CongruenceNormalizers.Dsl (N : ℕ) : Matrix.SpecialLinearGroup (Fin 2) ℝ

D = diag(h, 1), rescaled into SL₂(ℝ): diag(√h, 1/√h). Conjugation by it equals conjugation by D.

Equations

• CongruenceNormalizers.Dsl N = CongruenceNormalizers.projSL !![↑(CongruenceNormalizers.hPart N), 0; 0, 1]

noncomputable def CongruenceNormalizers.conjGamma0n (N : ℕ) : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)

D⁻¹ Γ₀(n) D ≤ SL₂(ℝ).

Equations

• CongruenceNormalizers.conjGamma0n N = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj (CongruenceNormalizers.Dsl N)⁻¹)) (CongruenceNormalizers.Gamma0R (CongruenceNormalizers.nPart N))

def CongruenceNormalizers.toR (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)

The image in SL₂(ℝ) of a subgroup of SL₂(ℤ).

Equations

• CongruenceNormalizers.toR Γ = Subgroup.map (Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) Γ

@[reducible, inline]

abbrev CongruenceNormalizers.NormG (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)) : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)

The normalizer of Γ in SL₂(ℝ).

Equations

• CongruenceNormalizers.NormG Γ = Subgroup.normalizer ↑Γ

Γ_Δ(N)

def CongruenceNormalizers.GammaDelta (N : ℕ) (Δ : Subgroup (ZMod N)ˣ) : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)

Γ_Δ(N) = {γ ∈ Γ₀(N) : γ₁₁ mod N ∈ Δ} ≤ SL₂(ℤ), for a subgroup Δ ≤ (ℤ/N)ˣ. (γ 1 1 is the lower right entry. For γ ∈ Γ₀(N) it is a unit mod N, since det γ = 1.)

Equations

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

def CongruenceNormalizers.GammaDeltaR (N : ℕ) (Δ : Subgroup (ZMod N)ˣ) : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)

Γ_Δ(N) in SL₂(ℝ).

Equations

• CongruenceNormalizers.GammaDeltaR N Δ = CongruenceNormalizers.toR (CongruenceNormalizers.GammaDelta N Δ)

noncomputable def CongruenceNormalizers.epsDelta (N : ℕ) [NeZero N] (Δ : Subgroup (ZMod N)ˣ) : ℕ

ε_Δ = gcd(N, d² − 1 : d ∈ Δ), with d running over the representatives (d : ZMod N).val ∈ [0, N). The truncated subtraction is harmless: for N ≥ 2 a unit has val ≥ 1, and for N = 1 the result is gcd(1, ·) = 1 anyway.

Equations

• CongruenceNormalizers.epsDelta N Δ = N.gcd ({x : (ZMod N)ˣ | x ∈ Δ}.gcd fun (d : (ZMod N)ˣ) => (↑d).val ^ 2 - 1)

noncomputable def CongruenceNormalizers.hDelta (N : ℕ) [NeZero N] (Δ : Subgroup (ZMod N)ˣ) : ℕ

h_Δ = ∏_{p ∣ N} p^{min(v_p(ε_Δ), ⌊v_p(N)/2⌋)}.

Equations

• CongruenceNormalizers.hDelta N Δ = ∏ p ∈ N.primeFactors, p ^ min ((CongruenceNormalizers.epsDelta N Δ).factorization p) (N.factorization p / 2)

@[reducible, inline]

abbrev CongruenceNormalizers.ofZ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : Matrix.SpecialLinearGroup (Fin 2) ℝ

The image in SL₂(ℝ) of an integer matrix.

Equations

• CongruenceNormalizers.ofZ γ = (Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ