Newman's argument for subgroups of Γ₀(N)

NewmanData records the lattice, unipotent and valuation hypotheses used in the argument. The proof applies both to Γ₀(N), instantiated in NormalizerLean/NewmanFacts, and to ΓΔ(N). Its integer divisibilities, local conclusion and final matrix form are proved once here.

theorem CongruenceNormalizers.int_eq_of_real {e X a : ℤ} (he : e ≠ 0) (h : (↑e)⁻¹ * ↑X = ↑a) : X = e * a

theorem CongruenceNormalizers.int_eq_of_real_div {e X a : ℤ} {d : ℕ} (he : e ≠ 0) (hd : d ≠ 0) (h : (↑e)⁻¹ * (↑X / ↑d) = ↑a) : X = e * ↑d * a

theorem CongruenceNormalizers.dvd_of_forall_vz_le {m x : ℤ} (hm : m ≠ 0) (hx : x ≠ 0) (h : ∀ (p : ℕ), Nat.Prime p → vz p m ≤ vz p x) : m ∣ x

theorem CongruenceNormalizers.vz_int_natCast (p n : ℕ) : vz p ↑n = n.factorization p

def CongruenceNormalizers.nOf (N η : ℕ) : ℕ

n = N / η².

Equations

• CongruenceNormalizers.nOf N η = N / η ^ 2

structure CongruenceNormalizers.NewmanData (N : ℕ) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)) (ε η : ℕ) : Prop

The hypotheses of Newman's argument for Γ ≤ Γ₀(N), with lattice parameter ε and output η.

• le : Γ ≤ Gamma0R N
• T_mem : matT ∈ Γ
• U_mem : matU N ∈ Γ
• inL (Y : Matrix.SpecialLinearGroup (Fin 2) ℝ) : Y ∈ Γ → InLe N ε ↑Y
• eps_dvd : ε ∣ N
• h_pos : 0 < η
• h_sq_dvd : η ^ 2 ∣ N
• h_fact (p : ℕ) : η.factorization p = min (ε.factorization p) (N.factorization p / 2)
• gamma (p : ℕ) : Nat.Prime p → p ∣ N → ε.factorization p < N.factorization p → ∃ (x : ℤ) (y : ℤ) (t : ℤ), x * t - y * ↑N = 1 ∧ (∃ γ ∈ Γ, ↑γ = !![↑x, ↑y; ↑N, ↑t]) ∧ t - x ≠ 0 ∧ vz p (t - x) = ε.factorization p

theorem CongruenceNormalizers.NewmanData.n_mul_sq {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} (D : NewmanData N Γ ε η) : nOf N η * η ^ 2 = N

theorem CongruenceNormalizers.NewmanData.factorization_n {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} (D : NewmanData N Γ ε η) (hN : N ≠ 0) (p : ℕ) : (nOf N η).factorization p + 2 * η.factorization p = N.factorization p

theorem CongruenceNormalizers.local_form_gen (ν j k δ₀ a b c d : ℕ) (hk : k = min j (ν / 2)) (prim : a = 0 ∨ b = 0 ∨ c = 0 ∨ d = 0) (u1 : min (a + d) (b + c) ≤ δ₀) (C2 : δ₀ ≤ 2 * a) (C3 : δ₀ + ν ≤ 2 * k + 2 * c) (C6 : δ₀ + 2 * k ≤ ν + 2 * b) (C7 : δ₀ ≤ 2 * d) (C10 : δ₀ + k ≤ j + a + b) (C11 : δ₀ + ν ≤ j + k + c + d) : δ₀ = 0 ∧ ν - 2 * k ≤ c ∨ δ₀ = ν - 2 * k ∧ ν - 2 * k ≤ a ∧ ν - 2 * k ≤ c ∧ ν - 2 * k ≤ d

The local matrix shape from primitivity and the necessary valuation bounds.

theorem CongruenceNormalizers.products_intG {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (D : NewmanData N Γ ε η) (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.exists_prim_formG {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (D : NewmanData N Γ ε η) (hg : g ∈ NormG Γ) : ∃ (κ : ℝ) (α : ℤ) (β : ℤ) (γ : ℤ) (δ : ℤ), κ ≠ 0 ∧ (∀ (p : ℕ), Nat.Prime p → ¬(↑p ∣ α ∧ ↑p ∣ β ∧ ↑p ∣ γ ∧ ↑p ∣ δ)) ∧ ↑g = κ • !![↑α, ↑β / ↑η; ↑η * ↑γ, ↑δ]

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

theorem CongruenceNormalizers.InLe.entries {ε N : ℕ} {M : Matrix (Fin 2) (Fin 2) ℝ} (h : InLe N ε M) : ∃ (a : ℤ) (b : ℤ) (c : ℤ) (d : ℤ), M 0 0 = ↑a ∧ M 0 1 = ↑b ∧ M 1 0 = ↑c ∧ M 1 1 = ↑d ∧ ↑N ∣ c ∧ ↑ε ∣ d - a

theorem CongruenceNormalizers.phi_InLe {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG Γ) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat η α β γ δ) {Y : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hY : Y ∈ Γ) : InLe N ε (Phi η α β γ δ ↑Y)

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

theorem CongruenceNormalizers.InLe_basic {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG Γ) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat η α β γ δ) (he : α * δ - β * γ ≠ 0) : InLe N ε (Phi η α β γ δ !![0, 1; 0, 0]) ∧ InLe N ε (↑N • Phi η α β γ δ !![0, 0; 1, 0]) ∧ InLe N ε (↑N • Phi η α β γ δ !![0, 0; 0, 1])

The four basic facts in InLe form.

theorem CongruenceNormalizers.InLe_s {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG Γ) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat η α β γ δ) (he : α * δ - β * γ ≠ 0) {x y t : ℤ} {γp : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hγp : γp ∈ Γ) (hγm : ↑γp = !![↑x, ↑y; ↑N, ↑t]) : InLe N ε (↑(t - x) • Phi η α β γ δ !![0, 0; 0, 1]) ∧ ↑ε ∣ t - x

The γ_p fact in InLe form, for γ_p = [[x, y], [N, t]] ∈ Γ.

theorem CongruenceNormalizers.int_factsG {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG Γ) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat η α β γ δ) (he : α * δ - β * γ ≠ 0) : α * δ - β * γ ∣ ↑η * (α * γ) ∧ α * δ - β * γ ∣ 1 * α ^ 2 ∧ (α * δ - β * γ) * ↑N ∣ ↑η ^ 2 * γ ^ 2 ∧ (α * δ - β * γ) * ↑ε ∣ 2 * ↑η * (α * γ) ∧ α * δ - β * γ ∣ ↑(nOf N η) * ↑η * (β * δ) ∧ α * δ - β * γ ∣ ↑(nOf N η) * β ^ 2 ∧ α * δ - β * γ ∣ 1 * δ ^ 2 ∧ (α * δ - β * γ) * ↑ε ∣ 2 * ↑(nOf N η) * ↑η * (β * δ) ∧ α * δ - β * γ ∣ ↑N * (β * γ) ∧ (α * δ - β * γ) * ↑η ∣ ↑N * (α * β) ∧ (α * δ - β * γ) * ↑N ∣ ↑N * ↑η * (γ * δ) ∧ (α * δ - β * γ) * ↑ε ∣ 2 * ↑N * (β * γ)

The integer divisibilities F1–F12.

theorem CongruenceNormalizers.int_facts_sG {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG Γ) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat η α β γ δ) (he : α * δ - β * γ ≠ 0) {x y t : ℤ} {γp : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hγp : γp ∈ Γ) (hγm : ↑γp = !![↑x, ↑y; ↑N, ↑t]) : α * δ - β * γ ∣ (t - x) * (β * γ) ∧ (α * δ - β * γ) * ↑η ∣ (t - x) * (α * β) ∧ (α * δ - β * γ) * ↑N ∣ (t - x) * ↑η * (γ * δ) ∧ (α * δ - β * γ) * ↑ε ∣ 2 * (t - x) * (β * γ)

The four facts with s = t − x in place of N.

theorem CongruenceNormalizers.local_conclusionG {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG Γ) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat η α β γ δ) (he : α * δ - β * γ ≠ 0) (hprim : ∀ (p : ℕ), Nat.Prime p → ¬(↑p ∣ α ∧ ↑p ∣ β ∧ ↑p ∣ γ ∧ ↑p ∣ δ)) {p : ℕ} (hp : Nat.Prime p) : have B := vz p (α * δ - β * γ) + N.factorization p + 1; vz p (α * δ - β * γ) = 0 ∧ (nOf N η).factorization p ≤ vv B p γ ∨ vz p (α * δ - β * γ) = (nOf N η).factorization p ∧ (nOf N η).factorization p ≤ vv B p α ∧ (nOf N η).factorization p ≤ vv B p γ ∧ (nOf N η).factorization p ≤ vv B p δ

The local conclusion at a prime p.

theorem CongruenceNormalizers.newmanG {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℝ)} {ε η N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (D : NewmanData N Γ ε η) (hg : g ∈ NormG Γ) : IsNewmanFormH N η g

Newman's argument for Γ: every element of the normalizer of Γ has the form IsNewmanFormH with parameter η.