Newman's theorem, step 2: the integrality conditions ([Nw §3])

With g = κ·S, S = [[α, β/h], [hγ, δ]] and e = αδ − βγ (so κ²e = 1), conjugation by g is Φ(M) = S M adj(S) / e. InL N M says that M is an integer matrix with N ∣ M₁₀ and ε ∣ M₁₁ − M₀₀ (ε = gcd(N, 24)); it holds on Γ₀(N) (units mod divisors of 24 square to 1) and is closed under integer combinations. Applying Φ to E₁₂ = T − 1, NE₂₁ = U − 1, NE₂₂ = N − (TU − T − U + 1) and (t − x)E₂₂ = γ − x − yE₁₂ − NE₂₁ (γ = [[x, y], [N, t]] ∈ Γ₀(N)) gives integer divisibilities.

def CongruenceNormalizers.epsPart (N : ℕ) : ℕ

ε = gcd(N, 24).

Equations

• CongruenceNormalizers.epsPart N = N.gcd 24

def CongruenceNormalizers.InLe (N ε : ℕ) (M : Matrix (Fin 2) (Fin 2) ℝ) : Prop

An integer matrix with N ∣ M₁₀ and ε ∣ M₁₁ − M₀₀.

Equations

• CongruenceNormalizers.InLe N ε M = ∃ (a : ℤ) (b : ℤ) (c : ℤ) (d : ℤ), M = !![↑a, ↑b; ↑c, ↑d] ∧ ↑N ∣ c ∧ ↑ε ∣ d - a

theorem CongruenceNormalizers.InLe.add {N ε : ℕ} {M M' : Matrix (Fin 2) (Fin 2) ℝ} (h : InLe N ε M) (h' : InLe N ε M') : InLe N ε (M + M')

theorem CongruenceNormalizers.InLe.zsmul {N ε : ℕ} {M : Matrix (Fin 2) (Fin 2) ℝ} (h : InLe N ε M) (m : ℤ) : InLe N ε (↑m • M)

theorem CongruenceNormalizers.InLe.sub {N ε : ℕ} {M M' : Matrix (Fin 2) (Fin 2) ℝ} (h : InLe N ε M) (h' : InLe N ε M') : InLe N ε (M - M')

theorem CongruenceNormalizers.InLe.one {ε : ℕ} (N : ℕ) : InLe N ε 1

def CongruenceNormalizers.InL (N : ℕ) (M : Matrix (Fin 2) (Fin 2) ℝ) : Prop

The Γ₀(N) lattice, with parameter gcd(N, 24).

Equations

• CongruenceNormalizers.InL N M = CongruenceNormalizers.InLe N (CongruenceNormalizers.epsPart N) M

theorem CongruenceNormalizers.InL.add {N : ℕ} {M M' : Matrix (Fin 2) (Fin 2) ℝ} (h : InL N M) (h' : InL N M') : InL N (M + M')

theorem CongruenceNormalizers.InL.zsmul {N : ℕ} {M : Matrix (Fin 2) (Fin 2) ℝ} (h : InL N M) (m : ℤ) : InL N (↑m • M)

theorem CongruenceNormalizers.InL.sub {N : ℕ} {M M' : Matrix (Fin 2) (Fin 2) ℝ} (h : InL N M) (h' : InL N M') : InL N (M - M')

theorem CongruenceNormalizers.InL.one (N : ℕ) : InL N 1

theorem CongruenceNormalizers.epsPart_dvd_24 (N : ℕ) : epsPart N ∣ 24

theorem CongruenceNormalizers.epsPart_dvd (N : ℕ) : epsPart N ∣ N

theorem CongruenceNormalizers.InL.of_mem {N : ℕ} {Y : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hY : Y ∈ Gamma0R N) : InL N ↑Y

Conjugation as a linear map

noncomputable def CongruenceNormalizers.Smat (h : ℕ) (α β γ δ : ℤ) : Matrix (Fin 2) (Fin 2) ℝ

S = [[α, β/h], [hγ, δ]].

Equations

• CongruenceNormalizers.Smat h α β γ δ = !![↑α, ↑β / ↑h; ↑h * ↑γ, ↑δ]

noncomputable def CongruenceNormalizers.Phi (h : ℕ) (α β γ δ : ℤ) (M : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ

Φ(M) = S M adj(S) / e.

Equations

• CongruenceNormalizers.Phi h α β γ δ M = (↑(α * δ - β * γ))⁻¹ • (CongruenceNormalizers.Smat h α β γ δ * M * (CongruenceNormalizers.Smat h α β γ δ).adjugate)

theorem CongruenceNormalizers.Phi_add (h : ℕ) (α β γ δ : ℤ) (M M' : Matrix (Fin 2) (Fin 2) ℝ) : Phi h α β γ δ (M + M') = Phi h α β γ δ M + Phi h α β γ δ M'

theorem CongruenceNormalizers.Phi_smul (h : ℕ) (α β γ δ : ℤ) (r : ℝ) (M : Matrix (Fin 2) (Fin 2) ℝ) : Phi h α β γ δ (r • M) = r • Phi h α β γ δ M

theorem CongruenceNormalizers.Phi_sub (h : ℕ) (α β γ δ : ℤ) (M M' : Matrix (Fin 2) (Fin 2) ℝ) : Phi h α β γ δ (M - M') = Phi h α β γ δ M - Phi h α β γ δ M'

theorem CongruenceNormalizers.det_Smat {h : ℕ} (hh : h ≠ 0) (α β γ δ : ℤ) : (Smat h α β γ δ).det = ↑(α * δ - β * γ)

theorem CongruenceNormalizers.Phi_one {h : ℕ} (hh : h ≠ 0) {α β γ δ : ℤ} (he : α * δ - β * γ ≠ 0) : Phi h α β γ δ 1 = 1

theorem CongruenceNormalizers.coe_conj_eq_Phi {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} {κ : ℝ} {h : ℕ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat h α β γ δ) (hh : h ≠ 0) (Y : Matrix.SpecialLinearGroup (Fin 2) ℝ) : ↑(g * Y * g⁻¹) = Phi h α β γ δ ↑Y

Conjugation by g = κ S is Φ.

theorem CongruenceNormalizers.Phi_E12 (h : ℕ) (α β γ δ : ℤ) : Phi h α β γ δ !![0, 1; 0, 0] = (↑(α * δ - β * γ))⁻¹ • !![-(↑α * ↑h * ↑γ), ↑α ^ 2; -(↑h ^ 2 * ↑γ ^ 2), ↑α * ↑h * ↑γ]

The explicit images of E₁₂, E₂₁, E₂₂ under M ↦ S M adj(S).

theorem CongruenceNormalizers.Phi_E21 {h : ℕ} (hh : h ≠ 0) (α β γ δ : ℤ) : Phi h α β γ δ !![0, 0; 1, 0] = (↑(α * δ - β * γ))⁻¹ • !![↑β * ↑δ / ↑h, -(↑β ^ 2 / ↑h ^ 2); ↑δ ^ 2, -(↑β * ↑δ / ↑h)]

theorem CongruenceNormalizers.Phi_E22 {h : ℕ} (hh : h ≠ 0) (α β γ δ : ℤ) : Phi h α β γ δ !![0, 0; 0, 1] = (↑(α * δ - β * γ))⁻¹ • !![-(↑β * ↑γ), ↑α * ↑β / ↑h; -(↑h * ↑γ * ↑δ), ↑α * ↑δ]