Newman's theorem, step 1: normalizing elements are rational up to a scalar ([Nw §2])

If g = [[x, y], [z, w]] normalizes Γ₀(N), the conjugates of T, U, TU are integral, so x², xz, z², Nyw, Ny², Nw², Nxw, Nxy, Nzw, Nyz are integers. With t = x (or t = z if x = 0), N t x, N t y, N t z, N t w are integers, and g = κ·[[α, β/h], [hγ, δ]] with α, β, γ, δ ∈ ℤ coprime (dividing by the gcd of the entries).

def CongruenceNormalizers.IsIntR (r : ℝ) : Prop

r is an integer.

Equations

• CongruenceNormalizers.IsIntR r = ∃ (m : ℤ), r = ↑m

theorem CongruenceNormalizers.IsIntR.add {r s : ℝ} (hr : IsIntR r) (hs : IsIntR s) : IsIntR (r + s)

theorem CongruenceNormalizers.IsIntR.sub {r s : ℝ} (hr : IsIntR r) (hs : IsIntR s) : IsIntR (r - s)

theorem CongruenceNormalizers.IsIntR.mul {r s : ℝ} (hr : IsIntR r) (hs : IsIntR s) : IsIntR (r * s)

theorem CongruenceNormalizers.IsIntR.neg {r : ℝ} (hr : IsIntR r) : IsIntR (-r)

theorem CongruenceNormalizers.IsIntR.int (m : ℤ) : IsIntR ↑m

theorem CongruenceNormalizers.IsIntR.nat (m : ℕ) : IsIntR ↑m

theorem CongruenceNormalizers.IsIntR.one : IsIntR 1

theorem CongruenceNormalizers.isIntR_entries_of_mem {N : ℕ} {γ : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hγ : γ ∈ Gamma0R N) (i j : Fin 2) : IsIntR (↑γ i j)

def CongruenceNormalizers.matT : Matrix.SpecialLinearGroup (Fin 2) ℝ

The unit upper-unipotent matrix.

Equations

• CongruenceNormalizers.matT = ⟨!![1, 1; 0, 1], CongruenceNormalizers.matT._proof_1⟩

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

The lower-unipotent matrix with lower-left entry N.

Equations

• CongruenceNormalizers.matU N = ⟨!![1, 0; ↑N, 1], ⋯⟩

theorem CongruenceNormalizers.matT_mem (N : ℕ) : matT ∈ Gamma0R N

theorem CongruenceNormalizers.matU_mem (N : ℕ) : matU N ∈ Gamma0R N

theorem CongruenceNormalizers.coe_conj (g Y : Matrix.SpecialLinearGroup (Fin 2) ℝ) : ↑(g * Y * g⁻¹) = ↑g * ↑Y * (↑g).adjugate

theorem CongruenceNormalizers.integral_products_of_normalizer {N : ℕ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} (subgroup_le : Γ ≤ Gamma0R N) (translation_mem : matT ∈ Γ) (lower_translation_mem : matU N ∈ Γ) {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ NormG Γ) {x y z w : ℝ} (hx : ↑g 0 0 = x) (hy : ↑g 0 1 = y) (hz : ↑g 1 0 = z) (hw : ↑g 1 1 = w) : IsIntR (x * x) ∧ IsIntR (x * z) ∧ IsIntR (z * z) ∧ IsIntR (↑N * (y * y)) ∧ IsIntR (↑N * (w * w)) ∧ IsIntR (↑N * (y * w)) ∧ IsIntR (↑N * (x * w)) ∧ IsIntR (↑N * (x * y)) ∧ IsIntR (↑N * (z * w)) ∧ IsIntR (↑N * (y * z))

The products of entries that are integers.

theorem CongruenceNormalizers.products_int {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Norm0 N) {x y z w : ℝ} (hx : ↑g 0 0 = x) (hy : ↑g 0 1 = y) (hz : ↑g 1 0 = z) (hw : ↑g 1 1 = w) : IsIntR (x * x) ∧ IsIntR (x * z) ∧ IsIntR (z * z) ∧ IsIntR (↑N * (y * y)) ∧ IsIntR (↑N * (w * w)) ∧ IsIntR (↑N * (y * w)) ∧ IsIntR (↑N * (x * w)) ∧ IsIntR (↑N * (x * y)) ∧ IsIntR (↑N * (z * w)) ∧ IsIntR (↑N * (y * z))

Integral entry products for the full congruence subgroup.

theorem CongruenceNormalizers.primitive_form_of_normalizer {N : ℕ} [NeZero N] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} (subgroup_le : Γ ≤ Gamma0R N) (translation_mem : matT ∈ Γ) (lower_translation_mem : matU N ∈ Γ) (scale : ℕ) (scale_pos : 0 < scale) {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ NormG Γ) : ∃ (κ : ℝ) (α : ℤ) (β : ℤ) (γ : ℤ) (δ : ℤ), κ ≠ 0 ∧ (∀ (p : ℕ), Nat.Prime p → ¬(↑p ∣ α ∧ ↑p ∣ β ∧ ↑p ∣ γ ∧ ↑p ∣ δ)) ∧ ↑g = κ • !![↑α, ↑β / ↑scale; ↑scale * ↑γ, ↑δ]

Step 1 ([Nw §2]): g = κ·[[α, β/h], [hγ, δ]] with α, β, γ, δ ∈ ℤ without a common prime factor.

theorem CongruenceNormalizers.exists_prim_form {N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Norm0 N) : ∃ (κ : ℝ) (α : ℤ) (β : ℤ) (γ : ℤ) (δ : ℤ), κ ≠ 0 ∧ (∀ (p : ℕ), Nat.Prime p → ¬(↑p ∣ α ∧ ↑p ∣ β ∧ ↑p ∣ γ ∧ ↑p ∣ δ)) ∧ ↑g = κ • !![↑α, ↑β / ↑(hPart N); ↑(hPart N) * ↑γ, ↑δ]

Primitive rational representatives for the full congruence subgroup.