diff --git a/LeanPool/CongruenceNormalizers.lean b/LeanPool/CongruenceNormalizers.lean new file mode 100644 index 000000000..4b3acb2c7 --- /dev/null +++ b/LeanPool/CongruenceNormalizers.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ + +module + +public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanMain +public import LeanPool.CongruenceNormalizers.NormalizerDelta.NewmanDelta + +/-! +# Newman normalizer bounds for congruence subgroups + +Source: doi:10.1017/S001708950000940X, url:https://github.com/F-Najman/normalizer-lean/tree/ea4445c0d991a65d54fc77af0af559f2322e8660 +Authors: Filip Najman +Status: verified +Main declarations: `CongruenceNormalizers.newman_iff`, `CongruenceNormalizers.newman_delta` +Tags: modular-forms, congruence-subgroups, normalizers, arithmetic-groups +MSC: 11F06, 20H05 +-/ + +/- +Adapted from Filip Najman's Apache-2.0 `normalizer-lean`, commit +`ea4445c0d991a65d54fc77af0af559f2322e8660`. The upstream proofs were written by +Claude Code agents following the author's mathematical blueprints. +-/ + +public section + +namespace CongruenceNormalizers + +open Matrix MatrixGroups + +/-- Newman's integral matrix form characterizes the real normalizer of Γ₀(N). -/ +theorem newman_iff {N : ℕ} [NeZero N] {g : SL(2, ℝ)} : + g ∈ Norm0 N ↔ IsNewmanForm N g := + ⟨newman', newmanForm_mem_normalizer'⟩ + +/-- The corresponding necessary matrix form for the normalizer of Γ_Δ(N). -/ +theorem newman_delta {N : ℕ} [NeZero N] (Δ : Subgroup (ZMod N)ˣ) + {g : SL(2, ℝ)} (hg : g ∈ NormG (GammaDeltaR N Δ)) : + IsNewmanFormH N (hDelta N Δ) g := + newman_delta' Δ hg + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/Imports.lean b/LeanPool/CongruenceNormalizers/Imports.lean new file mode 100644 index 000000000..53224b9ee --- /dev/null +++ b/LeanPool/CongruenceNormalizers/Imports.lean @@ -0,0 +1,22 @@ +/- +Copyright (c) 2026 Lean Pool contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Pool contributors +-/ +module -- shake: keep-all --deprecated_module: ignore + +-- Generated project imports; run `lake exe mk_all`. +public import LeanPool.CongruenceNormalizers +public import LeanPool.CongruenceNormalizers.NormalizerDelta.Basic +public import LeanPool.CongruenceNormalizers.NormalizerDelta.Defs +public import LeanPool.CongruenceNormalizers.NormalizerDelta.NewmanDelta +public import LeanPool.CongruenceNormalizers.NormalizerDelta.NewmanGen +public import LeanPool.CongruenceNormalizers.NormalizerLean.AtkinLehner +public import LeanPool.CongruenceNormalizers.NormalizerLean.Basic +public import LeanPool.CongruenceNormalizers.NormalizerLean.Defs +public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanCond +public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanFacts +public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanMain +public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanRat +public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanVal +public import LeanPool.CongruenceNormalizers.NormalizerLean.T1General diff --git a/LeanPool/CongruenceNormalizers/NormalizerDelta/Basic.lean b/LeanPool/CongruenceNormalizers/NormalizerDelta/Basic.lean new file mode 100644 index 000000000..b01eeb4ec --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerDelta/Basic.lean @@ -0,0 +1,155 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerDelta.NewmanGen + +/-! +# Γ_Δ(N), ε_Δ, h_Δ: basic facts + +* membership in Γ_Δ(N) and its image in SL₂(ℝ); T, U ∈ Γ_Δ(N); +* ε_Δ ∣ N and ε_Δ ∣ d² − 1 for d ∈ Δ (`dvd_epsDelta_iff`), hence every element of Γ_Δ(N) lies in the + lattice L_{ε_Δ} (`inLe_of_mem_GammaDeltaR`); +* v_p(h_Δ) = min(v_p(ε_Δ), ⌊v_p(N)/2⌋) (`factorization_hDelta`); +* the element γ_p ∈ Γ_Δ(N) (`exists_gamma_delta`): if v_p(ε_Δ) < v_p(N), some d ∈ Δ has + v_p(d² − 1) = v_p(ε_Δ), and [[x, y], [N, d]] has v_p(d − x) = v_p(ε_Δ). +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +variable {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} + +theorem mem_toR {Γ : Subgroup SL(2, ℤ)} {g : SL(2, ℝ)} : g ∈ toR Γ ↔ ∃ γ ∈ Γ, ofZ γ = g := + Subgroup.mem_map + +theorem ofZ_mem_toR {Γ : Subgroup SL(2, ℤ)} {γ : SL(2, ℤ)} (h : γ ∈ Γ) : ofZ γ ∈ toR Γ := + Subgroup.mem_map_of_mem _ h + +theorem coe_ofZ (γ : SL(2, ℤ)) : + (ofZ γ : Matrix (Fin 2) (Fin 2) ℝ) = !![(γ 0 0 : ℝ), γ 0 1; γ 1 0, γ 1 1] := by + ext i j; fin_cases i <;> fin_cases j <;> rfl + +theorem GammaDelta_le_Gamma0 : GammaDelta N Δ ≤ CongruenceSubgroup.Gamma0 N := fun _ h => h.1 + +theorem GammaDeltaR_le_Gamma0R : GammaDeltaR N Δ ≤ Gamma0R N := + Subgroup.map_mono GammaDelta_le_Gamma0 + +/-- An integer matrix of determinant 1. -/ +def mkSL (a b c d : ℤ) (h : a * d - b * c = 1) : SL(2, ℤ) := ⟨!![a, b; c, d], by + rw [det_fin_two_of]; exact h⟩ + +theorem mkSL_mem_GammaDelta {a b c d : ℤ} (h : a * d - b * c = 1) (hc : (N : ℤ) ∣ c) + {u : (ZMod N)ˣ} (hu : u ∈ Δ) (hud : (u : ZMod N) = (d : ZMod N)) : + mkSL a b c d h ∈ GammaDelta N Δ := by + refine ⟨?_, u, hu, by simpa [mkSL] using hud⟩ + rw [CongruenceSubgroup.Gamma0_mem] + simpa [mkSL] using (ZMod.intCast_zmod_eq_zero_iff_dvd c N).2 hc + +theorem coe_ofZ_mkSL {a b c d : ℤ} (h : a * d - b * c = 1) : + (ofZ (mkSL a b c d h) : Matrix (Fin 2) (Fin 2) ℝ) = !![(a : ℝ), b; c, d] := by + rw [coe_ofZ]; rfl + +theorem matT_mem_GammaDeltaR : matT ∈ GammaDeltaR N Δ := by + have h : (1 : ℤ) * 1 - 1 * 0 = 1 := by norm_num + refine mem_toR.2 ⟨mkSL 1 1 0 1 h, mkSL_mem_GammaDelta h (dvd_zero _) (Subgroup.one_mem _) + (by simp), ?_⟩ + apply Subtype.ext + rw [coe_ofZ_mkSL] + simp [matT] + +theorem matU_mem_GammaDeltaR : matU N ∈ GammaDeltaR N Δ := by + have h : (1 : ℤ) * 1 - 0 * N = 1 := by norm_num + refine mem_toR.2 ⟨mkSL 1 0 N 1 h, mkSL_mem_GammaDelta h (dvd_refl _) (Subgroup.one_mem _) + (by simp), ?_⟩ + apply Subtype.ext + rw [coe_ofZ_mkSL] + simp [matU] + +/-! ### ε_Δ -/ + +theorem dvd_epsDelta_iff [NeZero N] {m : ℕ} : + m ∣ epsDelta N Δ ↔ m ∣ N ∧ ∀ u ∈ Δ, m ∣ (u : ZMod N).val ^ 2 - 1 := by + classical + unfold epsDelta + rw [Nat.dvd_gcd_iff, Finset.dvd_gcd_iff] + simp only [Finset.mem_filter, Finset.mem_univ, true_and] + +theorem epsDelta_dvd [NeZero N] : epsDelta N Δ ∣ N := (dvd_epsDelta_iff.1 dvd_rfl).1 + +theorem epsDelta_dvd_val [NeZero N] {u : (ZMod N)ˣ} (hu : u ∈ Δ) : + epsDelta N Δ ∣ (u : ZMod N).val ^ 2 - 1 := (dvd_epsDelta_iff.1 dvd_rfl).2 u hu + +theorem epsDelta_pos [NeZero N] : 0 < epsDelta N Δ := + Nat.pos_of_dvd_of_pos epsDelta_dvd (Nat.pos_of_ne_zero (NeZero.ne N)) + +/-- For N ≥ 2 a unit has a positive representative. -/ +theorem one_le_val_unit (hN : 2 ≤ N) (u : (ZMod N)ˣ) : 1 ≤ (u : ZMod N).val := by + have : NeZero N := ⟨by omega⟩ + have : Nontrivial (ZMod N) := ZMod.nontrivial_iff.2 (by omega) + by_contra h + have h0 : (u : ZMod N).val = 0 := by omega + rw [ZMod.val_eq_zero] at h0 + exact u.ne_zero h0 + +/-- The integer form of ε_Δ ∣ val(u)² − 1. -/ +theorem epsDelta_dvd_val_int [NeZero N] {u : (ZMod N)ˣ} (hu : u ∈ Δ) : + (epsDelta N Δ : ℤ) ∣ ((u : ZMod N).val : ℤ) ^ 2 - 1 := by + by_cases hN : N = 1 + · have : epsDelta N Δ = 1 := Nat.dvd_one.1 (hN ▸ epsDelta_dvd) + rw [this]; exact one_dvd _ + have h1 := one_le_val_unit (by have := NeZero.ne N; omega) u + have := Int.natCast_dvd_natCast.2 (epsDelta_dvd_val hu) + rwa [Nat.cast_sub (Nat.one_le_pow _ _ h1), Nat.cast_pow, Nat.cast_one] at this + +/-- Every element of Γ_Δ(N) lies in the lattice L_{ε_Δ}. -/ +theorem inLe_of_mem_GammaDeltaR [NeZero N] {Y : SL(2, ℝ)} (hY : Y ∈ GammaDeltaR N Δ) : + InLe N (epsDelta N Δ) (Y : Matrix (Fin 2) (Fin 2) ℝ) := by + obtain ⟨γ, ⟨h0, u, hu, hγ⟩, rfl⟩ := mem_toR.1 hY + refine ⟨γ 0 0, γ 0 1, γ 1 0, γ 1 1, coe_ofZ γ, ?_, ?_⟩ + · exact (ZMod.intCast_zmod_eq_zero_iff_dvd _ N).1 (CongruenceSubgroup.Gamma0_mem.1 h0) + · have hc : (N : ℤ) ∣ γ 1 0 := + (ZMod.intCast_zmod_eq_zero_iff_dvd _ N).1 (CongruenceSubgroup.Gamma0_mem.1 h0) + have hdet : γ 0 0 * γ 1 1 - γ 0 1 * γ 1 0 = 1 := by + have := γ.2; rwa [det_fin_two] at this + set v : ℤ := ((u : ZMod N).val : ℤ) + have hv : (N : ℤ) ∣ γ 1 1 - v := by + rw [← ZMod.intCast_eq_intCast_iff_dvd_sub] + simp only [v, Int.cast_natCast, ZMod.natCast_zmod_val] + exact hγ + have hεN : (epsDelta N Δ : ℤ) ∣ N := Int.natCast_dvd_natCast.2 epsDelta_dvd + obtain ⟨k1, hk1⟩ := hεN.trans hv + obtain ⟨k2, hk2⟩ := epsDelta_dvd_val_int hu + obtain ⟨k3, hk3⟩ := hεN.trans hc + refine ⟨-(γ 1 1 * (γ 0 1 * k3)) + γ 0 0 * ((γ 1 1 + v) * k1 + k2), ?_⟩ + linear_combination -(γ 1 1) * hdet - (γ 1 1) * (γ 0 1) * hk3 + (γ 0 0) * (γ 1 1 + v) * hk1 + + (γ 0 0) * hk2 + +/-! ### h_Δ -/ + +theorem factorization_hDelta [NeZero N] (p : ℕ) : + (hDelta N Δ).factorization p = + min ((epsDelta N Δ).factorization p) (N.factorization p / 2) := by + unfold hDelta + rw [Nat.factorization_prod (fun q hq => pow_ne_zero _ (Nat.prime_of_mem_primeFactors hq).ne_zero), + Finset.sum_apply'] + rw [Finset.sum_congr rfl (fun q hq => by + rw [(Nat.prime_of_mem_primeFactors hq).factorization_pow, Finsupp.single_apply]), + Finset.sum_ite_eq'] + split_ifs with hp + · rfl + · have : N.factorization p = 0 := by + rwa [← Finsupp.notMem_support_iff, Nat.support_factorization] + simp [this] + +end + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerDelta/Defs.lean b/LeanPool/CongruenceNormalizers/NormalizerDelta/Defs.lean new file mode 100644 index 000000000..e566350e3 --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerDelta/Defs.lean @@ -0,0 +1,15 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerLean.Defs + +/-! The definitions of Part 2 are in `NormalizerLean/Defs.lean`, with those of all six parts. +This file +only imports them, so that `Statements.lean`, which imports this file, is unchanged since +freezing. -/ + +@[expose] public section diff --git a/LeanPool/CongruenceNormalizers/NormalizerDelta/NewmanDelta.lean b/LeanPool/CongruenceNormalizers/NormalizerDelta/NewmanDelta.lean new file mode 100644 index 000000000..c1bf9f4bf --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerDelta/NewmanDelta.lean @@ -0,0 +1,124 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerDelta.Basic + +/-! +# The generalized Newman bound (`newman_delta'`) + +Γ_Δ(N) satisfies the hypotheses `NewmanData N (Γ_Δ(N)) ε_Δ h_Δ` of the generic Newman argument +(`NewmanGen.lean`); the only new ingredient is the element γ_p (`exists_gamma_delta`): +if j = v_p(ε_Δ) < ν = v_p(N), then p^{j+1} ∣ N, so p^{j+1} ∤ d² − 1 for some d ∈ Δ (otherwise +p^{j+1} ∣ ε_Δ), while p^j ∣ ε_Δ ∣ d² − 1. With t = d and x t − y N = 1, the matrix +[[x, y], [N, t]] lies in Γ_Δ(N), and t(t − x) ≡ t² − 1 (mod N) gives v_p(t − x) = j (`gamma_val`). +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +variable {N : ℕ} {Δ : Subgroup (ZMod N)ˣ} + +/-- The element γ_p of Γ_Δ(N). -/ +theorem exists_gamma_delta [NeZero N] {p : ℕ} (hp : p.Prime) (hpN : p ∣ N) + (hj : (epsDelta N Δ).factorization p < N.factorization p) : + ∃ x y t : ℤ, x * t - y * N = 1 ∧ + (∃ γ ∈ GammaDeltaR N Δ, (γ : Matrix (Fin 2) (Fin 2) ℝ) = !![(x : ℝ), y; N, t]) ∧ + t - x ≠ 0 ∧ vz p (t - x) = (epsDelta N Δ).factorization p := by + have hN := NeZero.ne N + have hN2 : 2 ≤ N := le_trans hp.two_le (Nat.le_of_dvd (Nat.pos_of_ne_zero hN) hpN) + set j := (epsDelta N Δ).factorization p with hjdef + set ν := N.factorization p with hν + have hε0 : epsDelta N Δ ≠ 0 := epsDelta_pos.ne' + -- some u ∈ Δ with p^{j+1} ∤ val(u)² − 1 + obtain ⟨u, hu, hnd⟩ : ∃ u ∈ Δ, ¬ p ^ (j + 1) ∣ (u : ZMod N).val ^ 2 - 1 := by + by_contra hcon + push Not at hcon + have h1 : p ^ (j + 1) ∣ N := (hp.pow_dvd_iff_le_factorization hN).2 (by omega) + have h2 : p ^ (j + 1) ∣ epsDelta N Δ := dvd_epsDelta_iff.2 ⟨h1, hcon⟩ + have := (hp.pow_dvd_iff_le_factorization hε0).1 h2 + omega + have hpj : p ^ j ∣ (u : ZMod N).val ^ 2 - 1 := + (Nat.ordProj_dvd (epsDelta N Δ) p).trans (epsDelta_dvd_val hu) + set v := (u : ZMod N).val with hvdef + have hv1 : 1 ≤ v := one_le_val_unit hN2 u + have hcopN : Nat.Coprime v N := ZMod.val_coe_unit_coprime u + -- Bézout: x v − y N = 1 + have hb := Int.gcd_eq_gcd_ab v N + rw [Int.gcd_natCast_natCast, hcopN] at hb + set x := Int.gcdA v N + set y := -Int.gcdB v N + have hdet : x * v - y * N = 1 := by + push_cast at hb + simp only [y] + linear_combination -hb + refine ⟨x, y, v, hdet, ?_, ?_⟩ + · have hdet' : x * v - y * N = 1 := hdet + refine ⟨ofZ (mkSL x y N v hdet'), ofZ_mem_toR (mkSL_mem_GammaDelta hdet' (dvd_refl _) hu ?_), + coe_ofZ_mkSL hdet'⟩ + simp [v] + · -- the valuation, by `gamma_val` with the roles of x and t exchanged + have hdet2 : (v : ℤ) * x - y * N = 1 := by linear_combination hdet + have hpν : (p : ℤ) ^ ν ∣ (N : ℤ) := by exact_mod_cast Nat.ordProj_dvd N p + have hpv : IsCoprime (p : ℤ) (v : ℤ) := by + rw [Int.isCoprime_iff_gcd_eq_one, Int.gcd_natCast_natCast] + exact (Nat.Coprime.coprime_dvd_right hpN hcopN).symm + have hcast : (((v ^ 2 - 1 : ℕ)) : ℤ) = (v : ℤ) ^ 2 - 1 := by + rw [Nat.cast_sub (Nat.one_le_pow _ _ hv1)]; push_cast; ring + have hρ1 : (p : ℤ) ^ j ∣ 1 - (v : ℤ) ^ 2 := by + have := Int.natCast_dvd_natCast.2 hpj + rw [hcast] at this + push_cast at this + have := this.neg_right + convert this using 1; ring + have hρ2 : ¬ (p : ℤ) ^ (j + 1) ∣ 1 - (v : ℤ) ^ 2 := by + intro hd + apply hnd + have hd' : (p : ℤ) ^ (j + 1) ∣ (((v ^ 2 - 1 : ℕ)) : ℤ) := by + rw [hcast]; have := hd.neg_right; convert this using 1; ring + exact_mod_cast hd' + rcases gamma_val hp hdet2 hpν (by simp) hpv hρ1 hρ2 with h | ⟨-, hne, hval⟩ + · omega + · refine ⟨fun h0 => hne (by linear_combination -h0), ?_⟩ + rw [show (v : ℤ) - x = -(x - v) by ring, vz_neg] + exact hval + +/-- Γ_Δ(N) satisfies the hypotheses of the generic Newman argument. -/ +theorem newmanData_delta (N : ℕ) [NeZero N] (Δ : Subgroup (ZMod N)ˣ) : + NewmanData N (GammaDeltaR N Δ) (epsDelta N Δ) (hDelta N Δ) where + le := GammaDeltaR_le_Gamma0R + T_mem := matT_mem_GammaDeltaR + U_mem := matU_mem_GammaDeltaR + inL := fun _ hY => inLe_of_mem_GammaDeltaR hY + eps_dvd := epsDelta_dvd + h_pos := by unfold hDelta; exact Finset.prod_pos (fun q hq => pow_pos + (Nat.pos_of_mem_primeFactors hq) _) + h_sq_dvd := by + have hN := NeZero.ne N + have hh : hDelta N Δ ≠ 0 := by + unfold hDelta + exact Finset.prod_ne_zero_iff.2 (fun q hq => pow_ne_zero _ (Nat.pos_of_mem_primeFactors + hq).ne') + rw [← Nat.factorization_le_iff_dvd (pow_ne_zero 2 hh) hN] + intro p + rw [Nat.factorization_pow, Finsupp.smul_apply, smul_eq_mul, factorization_hDelta] + omega + h_fact := factorization_hDelta + gamma := fun _ hp hpN hj => exists_gamma_delta hp hpN hj + +/-- **The generalized Newman bound.** -/ +theorem newman_delta' {N : ℕ} [NeZero N] (Δ : Subgroup (ZMod N)ˣ) {g : SL(2, ℝ)} + (hg : g ∈ NormG (GammaDeltaR N Δ)) : IsNewmanFormH N (hDelta N Δ) g := + newmanG (newmanData_delta N Δ) hg + +end + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerDelta/NewmanGen.lean b/LeanPool/CongruenceNormalizers/NormalizerDelta/NewmanGen.lean new file mode 100644 index 000000000..2212caaa0 --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerDelta/NewmanGen.lean @@ -0,0 +1,497 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanVal +public import LeanPool.CongruenceNormalizers.NormalizerDelta.Defs + +/-! +# 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. +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +theorem int_eq_of_real {e X a : ℤ} (he : e ≠ 0) (h : ((e : ℝ))⁻¹ * (X : ℝ) = a) : X = e * a := by + have her : (e : ℝ) ≠ 0 := by exact_mod_cast he + have : (X : ℝ) = e * a := by rw [← h]; field_simp + exact_mod_cast this + +theorem int_eq_of_real_div {e X a : ℤ} {d : ℕ} (he : e ≠ 0) (hd : d ≠ 0) + (h : ((e : ℝ))⁻¹ * ((X : ℝ) / d) = a) : X = e * d * a := by + have her : (e : ℝ) ≠ 0 := by exact_mod_cast he + have hdr : (d : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hd + have : (X : ℝ) = e * d * a := by rw [← h]; field_simp + exact_mod_cast this + +theorem dvd_of_forall_vz_le {m x : ℤ} (hm : m ≠ 0) (hx : x ≠ 0) + (h : ∀ p : ℕ, p.Prime → vz p m ≤ vz p x) : m ∣ x := by + rw [← Int.natAbs_dvd_natAbs] + rw [← Nat.factorization_le_iff_dvd (Int.natAbs_ne_zero.2 hm) (Int.natAbs_ne_zero.2 hx)] + intro p + by_cases hp : p.Prime + · exact h p hp + · simp [Nat.factorization_eq_zero_of_not_prime _ hp] + +theorem vz_int_natCast (p n : ℕ) : vz p (n : ℤ) = n.factorization p := vz_natCast p n + +/-- n = N / η². -/ +def nOf (N η : ℕ) : ℕ := N / η ^ 2 + +/-- The hypotheses of Newman's argument for Γ ≤ Γ₀(N), with lattice parameter ε and output η. -/ +structure NewmanData (N : ℕ) (Γ : Subgroup SL(2, ℝ)) (ε η : ℕ) : Prop where + le : Γ ≤ Gamma0R N + T_mem : matT ∈ Γ + U_mem : matU N ∈ Γ + inL : ∀ Y ∈ Γ, InLe N ε (Y : Matrix (Fin 2) (Fin 2) ℝ) + 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 : ℕ, p.Prime → p ∣ N → ε.factorization p < N.factorization p → + ∃ x y t : ℤ, x * t - y * N = 1 ∧ + (∃ γ ∈ Γ, (γ : Matrix (Fin 2) (Fin 2) ℝ) = !![(x : ℝ), y; N, t]) ∧ + t - x ≠ 0 ∧ vz p (t - x) = ε.factorization p + +variable {Γ : Subgroup SL(2, ℝ)} {ε η : ℕ} + +theorem NewmanData.n_mul_sq {N : ℕ} (D : NewmanData N Γ ε η) : nOf N η * η ^ 2 = N := + Nat.div_mul_cancel D.h_sq_dvd + +theorem NewmanData.factorization_n {N : ℕ} (D : NewmanData N Γ ε η) (hN : N ≠ 0) (p : ℕ) : + (nOf N η).factorization p + 2 * η.factorization p = N.factorization p := by + have h := D.n_mul_sq + have hn : nOf N η ≠ 0 := by rintro h0; rw [h0, zero_mul] at h; exact hN h.symm + have := congrArg (fun m => m.factorization p) h + rw [Nat.factorization_mul hn (by have := D.h_pos; positivity), Nat.factorization_pow] at this + simp only [Finsupp.add_apply, Finsupp.smul_apply, smul_eq_mul] at this + omega + +/-- The local matrix shape from primitivity and the necessary valuation bounds. -/ +theorem 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) := by + omega + +/-- The products of entries that are integers. -/ +theorem products_intG {N : ℕ} {g : SL(2, ℝ)} (D : NewmanData N Γ ε η) (hg : g ∈ NormG Γ) {x y z w + : ℝ} + (hx : (g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = x) (hy : (g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = y) + (hz : (g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = z) (hw : (g : Matrix (Fin 2) (Fin 2) ℝ) 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)) := by + exact integral_products_of_normalizer D.le D.T_mem D.U_mem hg hx hy hz hw + +/-- **Step 1** ([Nw §2]): g = κ·[[α, β/h], [hγ, δ]] with α, β, γ, δ ∈ ℤ without a common prime +factor. -/ +theorem exists_prim_formG {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (D : NewmanData N Γ ε η) (hg : g ∈ + NormG Γ) : + ∃ (κ : ℝ) (α β γ δ : ℤ), κ ≠ 0 ∧ + (∀ p : ℕ, p.Prime → ¬ ((p : ℤ) ∣ α ∧ (p : ℤ) ∣ β ∧ (p : ℤ) ∣ γ ∧ (p : ℤ) ∣ δ)) ∧ + (g : Matrix (Fin 2) (Fin 2) ℝ) = + κ • !![(α : ℝ), (β : ℝ) / η; (η : ℝ) * γ, (δ : ℝ)] := by + exact primitive_form_of_normalizer D.le D.T_mem D.U_mem η D.h_pos hg + +theorem 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 := by + obtain ⟨a, b, c, d, rfl, hc, hd⟩ := h + exact ⟨a, b, c, d, by simp, by simp, by simp, by simp, hc, hd⟩ + + +theorem phi_InLe {N : ℕ} {g : SL(2, ℝ)} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG Γ) {κ + : ℝ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (η) α β γ δ) {Y : SL(2, ℝ)} + (hY : Y ∈ Γ) : InLe N ε (Phi (η) α β γ δ (Y : Matrix (Fin 2) (Fin 2) ℝ)) := by + rw [← coe_conj_eq_Phi hg D.h_pos.ne'] + exact D.inL _ ((Subgroup.mem_normalizer_iff.1 hgN Y).1 hY) + +theorem InLe.nsmul' {N : ℕ} {M : Matrix (Fin 2) (Fin 2) ℝ} (h : InLe N ε M) (m : ℕ) : + InLe N ε ((m : ℝ) • M) := by + have := h.zsmul m + simpa using this + +/-- The four basic facts in `InLe` form. -/ +theorem InLe_basic {N : ℕ} {g : SL(2, ℝ)} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG Γ) + {κ : ℝ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • 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]) := by + have hh : η ≠ 0 := D.h_pos.ne' + have h1 : InLe N ε (Phi (η) α β γ δ 1) := by rw [Phi_one hh he]; exact InLe.one N + have hT := phi_InLe D hgN hg D.T_mem + have hU := phi_InLe D hgN hg D.U_mem + have hTU := phi_InLe D hgN hg (mul_mem D.T_mem D.U_mem) + have eE12 : (!![0, 1; 0, 0] : Matrix (Fin 2) (Fin 2) ℝ) = (matT : Matrix (Fin 2) (Fin 2) ℝ) - 1 + := by + ext i j; fin_cases i <;> fin_cases j <;> simp [matT] + have eE21 : (N : ℝ) • (!![0, 0; 1, 0] : Matrix (Fin 2) (Fin 2) ℝ) = + (matU N : Matrix (Fin 2) (Fin 2) ℝ) - 1 := by + ext i j; fin_cases i <;> fin_cases j <;> simp [matU] + have eE22 : (N : ℝ) • (!![0, 0; 0, 1] : Matrix (Fin 2) (Fin 2) ℝ) = + (N : ℝ) • 1 - (((matT * matU N : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) - + (matT : Matrix (Fin 2) (Fin 2) ℝ) - (matU N : Matrix (Fin 2) (Fin 2) ℝ) + 1) := by + rw [Matrix.SpecialLinearGroup.coe_mul] + ext i j; fin_cases i <;> fin_cases j <;> simp [matT, matU] + refine ⟨?_, ?_, ?_⟩ + · rw [eE12, Phi_sub]; exact hT.sub h1 + · rw [← Phi_smul, eE21, Phi_sub]; exact hU.sub h1 + · rw [← Phi_smul, eE22, Phi_sub, Phi_smul, Phi_add, Phi_sub, Phi_sub] + exact (h1.nsmul' N).sub (((hTU.sub hT).sub hU).add h1) + +/-- The γ_p fact in `InLe` form, for γ_p = [[x, y], [N, t]] ∈ Γ. -/ +theorem InLe_s {N : ℕ} {g : SL(2, ℝ)} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG Γ) + {κ : ℝ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (η) α β γ δ) + (he : α * δ - β * γ ≠ 0) {x y t : ℤ} {γp : SL(2, ℝ)} (hγp : γp ∈ Γ) + (hγm : (γp : Matrix (Fin 2) (Fin 2) ℝ) = !![(x : ℝ), y; N, t]) : + InLe N ε (((t - x : ℤ) : ℝ) • Phi (η) α β γ δ !![0, 0; 0, 1]) ∧ + (ε : ℤ) ∣ t - x := by + have hh : η ≠ 0 := D.h_pos.ne' + have hε : (ε : ℤ) ∣ t - x := by + obtain ⟨a, b, c, d, hm, -, hd⟩ := D.inL _ hγp + have h00 := congrFun (congrFun hm 0) 0 + have h11 := congrFun (congrFun hm 1) 1 + rw [hγm] at h00 h11 + simp only [Fin.isValue, of_apply, cons_val', cons_val_zero, cons_val_fin_one, Int.cast_inj, + cons_val_one] at h00 h11 + have : x = a := by exact_mod_cast h00 + have : t = d := by exact_mod_cast h11 + subst_vars + exact hd + refine ⟨?_, hε⟩ + have h1 : InLe N ε (Phi (η) α β γ δ 1) := by rw [Phi_one hh he]; exact InLe.one N + have hP := phi_InLe D hgN hg hγp + obtain ⟨hE12, hE21, -⟩ := InLe_basic D hgN hg he + have eE : ((t - x : ℤ) : ℝ) • (!![0, 0; 0, 1] : Matrix (Fin 2) (Fin 2) ℝ) = + (γp : Matrix (Fin 2) (Fin 2) ℝ) - (x : ℝ) • 1 - (y : ℝ) • !![0, 1; 0, 0] - + (N : ℝ) • !![0, 0; 1, 0] := by + rw [hγm] + ext i j; fin_cases i <;> fin_cases j <;> simp + rw [← Phi_smul, eE, Phi_sub, Phi_sub, Phi_sub, Phi_smul, Phi_smul, Phi_smul] + exact ((hP.sub (h1.zsmul x)).sub (hE12.zsmul y)).sub hE21 + +/-- The integer divisibilities F1–F12. -/ +theorem int_factsG {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG Γ) + {κ : ℝ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • 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 : ℤ)) * (β * γ) := by + have hh : η ≠ 0 := D.h_pos.ne' + have hhr : (η : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hh + have hNr : (N : ℝ) = nOf N η * (η : ℝ) ^ 2 := by + exact_mod_cast D.n_mul_sq.symm + have hNz : (N : ℤ) = (nOf N η : ℤ) * (η : ℤ) ^ 2 := by exact_mod_cast D.n_mul_sq.symm + have hN0 : (N : ℤ) ≠ 0 := Nat.cast_ne_zero.2 (NeZero.ne N) + obtain ⟨P12, P21, P22⟩ := InLe_basic D hgN hg he + -- E₁₂ + obtain ⟨a1, b1, c1, d1, h00, h01, h10, h11, hc1, hd1⟩ := P12.entries + rw [Phi_E12] at h00 h01 h10 h11 + have r00 := int_eq_of_real (X := -(α * (η : ℤ) * γ)) he (by rw [← h00]; simp) + have r01 := int_eq_of_real (X := α ^ 2) he (by rw [← h01]; simp) + have r10 := int_eq_of_real (X := -((η : ℤ) ^ 2 * γ ^ 2)) he (by rw [← h10]; simp) + have r11 := int_eq_of_real (X := α * (η : ℤ) * γ) he (by rw [← h11]; simp) + -- E₂₁ (times N) + obtain ⟨a2, b2, c2, d2, i00, i01, i10, i11, hc2, hd2⟩ := P21.entries + rw [Phi_E21 hh] at i00 i01 i10 i11 + have s00 := int_eq_of_real (X := (nOf N η : ℤ) * (η : ℤ) * (β * δ)) he + (by rw [← i00]; simp [hNr]; field_simp) + have s01 := int_eq_of_real (X := -((nOf N η : ℤ) * β ^ 2)) he + (by rw [← i01]; simp [hNr]; field_simp) + have s10 := int_eq_of_real (X := (N : ℤ) * δ ^ 2) he (by rw [← i10]; simp; ring) + have s11 := int_eq_of_real (X := -((nOf N η : ℤ) * (η : ℤ) * (β * δ))) he + (by rw [← i11]; simp [hNr]; field_simp) + -- E₂₂ (times N) + obtain ⟨a3, b3, c3, d3, j00, j01, j10, j11, hc3, hd3⟩ := P22.entries + rw [Phi_E22 hh] at j00 j01 j10 j11 + have t00 := int_eq_of_real (X := -((N : ℤ) * (β * γ))) he (by rw [← j00]; simp; ring) + have t01 := int_eq_of_real (X := (nOf N η : ℤ) * (η : ℤ) * (α * β)) he + (by rw [← j01]; simp [hNr]; field_simp) + have t10 := int_eq_of_real (X := -((N : ℤ) * (η : ℤ) * (γ * δ))) he + (by rw [← j10]; simp; ring) + have t11 := int_eq_of_real (X := (N : ℤ) * (α * δ)) he (by rw [← j11]; simp; ring) + obtain ⟨c1', rfl⟩ := hc1 + obtain ⟨c2', rfl⟩ := hc2 + obtain ⟨c3', rfl⟩ := hc3 + obtain ⟨k1, hk1⟩ := hd1 + obtain ⟨k2, hk2⟩ := hd2 + obtain ⟨k3, hk3⟩ := hd3 + have hε : (ε : ℤ) ∣ (N : ℤ) := Int.natCast_dvd_natCast.2 D.eps_dvd + obtain ⟨m, hm⟩ := hε + have ha1 : a1 = -d1 := mul_left_cancel₀ he (by linear_combination -r00 - r11) + have ha2 : d2 = -a2 := mul_left_cancel₀ he (by linear_combination -s11 - s00) + have hd3' : d3 - a3 = N - 2 * a3 := mul_left_cancel₀ he (by linear_combination -t11 - t00) + refine ⟨⟨d1, by linear_combination r11⟩, ⟨b1, by linear_combination r01⟩, + ⟨-c1', by linear_combination -r10⟩, + ⟨k1, by linear_combination 2 * r11 + (α * δ - β * γ) * hk1 + (α * δ - β * γ) * ha1⟩, + ⟨a2, by linear_combination s00⟩, ⟨-b2, by linear_combination -s01⟩, + ⟨c2', mul_left_cancel₀ hN0 (by linear_combination s10)⟩, + ⟨-k2, by linear_combination 2 * s00 - (α * δ - β * γ) * hk2 + (α * δ - β * γ) * ha2⟩, + ⟨-a3, by linear_combination -t00⟩, ⟨b3, by rw [hNz]; linear_combination (η : ℤ) * t01⟩, + ⟨-c3', by linear_combination -t10⟩, ?_⟩ + -- F12: ε ∣ N − 2 a3 and ε ∣ N give ε ∣ 2 a3 + have h2a : (ε : ℤ) ∣ 2 * a3 := by + have : (ε : ℤ) ∣ (N : ℤ) - (d3 - a3) := dvd_sub ⟨m, hm⟩ ⟨k3, hk3⟩ + rw [hd3'] at this + simpa using this + obtain ⟨k4, hk4⟩ := h2a + exact ⟨-k4, by linear_combination -2 * t00 - (α * δ - β * γ) * hk4⟩ + + +/-- The four facts with s = t − x in place of N. -/ +theorem int_facts_sG {N : ℕ} {g : SL(2, ℝ)} (D : NewmanData N Γ ε η) (hgN : g ∈ NormG + Γ) {κ : ℝ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (η) α β γ δ) + (he : α * δ - β * γ ≠ 0) {x y t : ℤ} {γp : SL(2, ℝ)} (hγp : γp ∈ Γ) + (hγm : (γp : Matrix (Fin 2) (Fin 2) ℝ) = !![(x : ℝ), y; N, t]) : + (α * δ - β * γ) ∣ (t - x) * (β * γ) ∧ + (α * δ - β * γ) * (η : ℤ) ∣ (t - x) * (α * β) ∧ + (α * δ - β * γ) * N ∣ ((t - x) * (η : ℤ)) * (γ * δ) ∧ + (α * δ - β * γ) * (ε : ℤ) ∣ (2 * (t - x)) * (β * γ) := by + have hh : η ≠ 0 := D.h_pos.ne' + obtain ⟨P, hε⟩ := InLe_s D hgN hg he hγp hγm + obtain ⟨a4, b4, c4, d4, j00, j01, j10, j11, hc4, hd4⟩ := P.entries + rw [Phi_E22 hh] at j00 j01 j10 j11 + have t00 := int_eq_of_real (X := -((t - x) * (β * γ))) he (by rw [← j00]; simp; ring) + have t01 := int_eq_of_real_div (X := (t - x) * (α * β)) he hh + (by rw [← j01]; simp; ring) + have t10 := int_eq_of_real (X := -((t - x) * (η : ℤ) * (γ * δ))) he + (by rw [← j10]; simp; ring) + have t11 := int_eq_of_real (X := (t - x) * (α * δ)) he (by rw [← j11]; simp; ring) + obtain ⟨c4', rfl⟩ := hc4 + obtain ⟨k4, hk4⟩ := hd4 + have hd4' : d4 - a4 = (t - x) - 2 * a4 := mul_left_cancel₀ he (by linear_combination -t11 - t00) + refine ⟨⟨-a4, by linear_combination -t00⟩, ⟨b4, by linear_combination t01⟩, + ⟨-c4', by linear_combination -t10⟩, ?_⟩ + have h2a : (ε : ℤ) ∣ 2 * a4 := by + have : (ε : ℤ) ∣ (t - x) - (d4 - a4) := dvd_sub hε ⟨k4, hk4⟩ + rw [hd4'] at this + simpa using this + obtain ⟨k5, hk5⟩ := h2a + exact ⟨-k5, by linear_combination -2 * t00 - (α * δ - β * γ) * hk5⟩ + +/-- The local conclusion at a prime p. -/ +theorem local_conclusionG {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (D : NewmanData N Γ ε η) (hgN : g ∈ + NormG Γ) {κ : ℝ} + {α β γ δ : ℤ} (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (η) α β γ δ) + (he : α * δ - β * γ ≠ 0) + (hprim : ∀ p : ℕ, p.Prime → ¬ ((p : ℤ) ∣ α ∧ (p : ℤ) ∣ β ∧ (p : ℤ) ∣ γ ∧ (p : ℤ) ∣ δ)) + {p : ℕ} (hp : p.Prime) : + let 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 δ) := by + intro B + have hN := NeZero.ne N + have hNz : (N : ℤ) ≠ 0 := Nat.cast_ne_zero.2 hN + have hhz : (η : ℤ) ≠ 0 := Nat.cast_ne_zero.2 D.h_pos.ne' + have hn0 : nOf N η ≠ 0 := by + intro h0 + have := D.n_mul_sq + rw [h0, zero_mul] at this + exact hN this.symm + have hε0 : ε ≠ 0 := (Nat.pos_of_dvd_of_pos D.eps_dvd (Nat.pos_of_ne_zero hN)).ne' + -- the local constants + set ν := N.factorization p with hν + set j := (ε).factorization p with hj + set k := (η).factorization p with hk + set nν := (nOf N η).factorization p with hnν + set δ₀ := vz p (α * δ - β * γ) with hδ₀ + have hkj : k = min j (ν / 2) := D.h_fact p + have hnk : nν + 2 * k = ν := D.factorization_n hN p + have hjν : j ≤ ν := (Nat.factorization_le_iff_dvd hε0 hN).2 D.eps_dvd p + -- valuations of the constants + have vN : vz p (N : ℤ) = ν := vz_natCast p N + have vh : vz p (η : ℤ) = k := vz_natCast p _ + have vn : vz p (nOf N η : ℤ) = nν := vz_natCast p _ + have v1 : vz p (1 : ℤ) = 0 := by simp [vz] + -- shorthand for the valuations of the entries + set a := vv B p α + set b := vv B p β + set c := vv B p γ + set d := vv B p δ + -- primitivity + have prim : a = 0 ∨ b = 0 ∨ c = 0 ∨ d = 0 := by + by_contra hcon + push Not at hcon + apply hprim p hp + have key : ∀ x : ℤ, vv B p x ≠ 0 → (p : ℤ) ∣ x := by + intro x hx + by_cases h0 : x = 0 + · rw [h0]; exact dvd_zero _ + · rw [vv_of_ne h0] at hx + have := (pow_dvd_iff_le_vz hp h0 1).2 (Nat.pos_of_ne_zero hx) + simpa using this + exact ⟨key α hcon.1, key β hcon.2.1, key γ hcon.2.2.1, key δ hcon.2.2.2⟩ + -- ultrametric relation + have u1 := (ultra_vv (B := B) hp he (by simp only [B]; omega)).1 + obtain ⟨_, F2, F3, _, _, F6, F7, _, _, F10, F11, _⟩ := int_factsG D hgN hg he + have vX : ∀ X : ℤ, X ≠ 0 → vz p ((α * δ - β * γ) * X) = δ₀ + vz p X := fun _ hX => + vz_mul he hX + have hBe : vz p (α * δ - β * γ) ≤ B := by simp only [B]; omega + have hBN : vz p ((α * δ - β * γ) * N) ≤ B := by rw [vX _ hNz, vN]; simp only [B]; omega + have hBh : vz p ((α * δ - β * γ) * (η : ℤ)) ≤ B := by + rw [vX _ hhz, vh]; simp only [B] + omega + have c2 := le_vv_sq (B := B) one_ne_zero hBe F2 + have c3 := le_vv_sq (B := B) (pow_ne_zero 2 hhz) hBN F3 + have c6 := le_vv_sq (B := B) (Nat.cast_ne_zero.2 hn0) hBe F6 + have c7 := le_vv_sq (B := B) one_ne_zero hBe F7 + have c10 := le_vv2 (B := B) hNz hBh F10 + have c11 := le_vv2 (B := B) (mul_ne_zero hNz hhz) hBN F11 + simp only [vX _ hNz, vX _ hhz, vz_mul hNz hhz, vz_mul hhz hhz, pow_two, vN, vh, vn, v1] + at c2 c3 c6 c7 c10 c11 + obtain ⟨C10, C11⟩ : δ₀ + k ≤ j + a + b ∧ δ₀ + ν ≤ j + k + c + d := by + by_cases hνj : ν = j + · exact ⟨by omega, by omega⟩ + have hpN : p ∣ N := by + by_contra hpN + have : ν = 0 := Nat.factorization_eq_zero_of_not_dvd hpN + omega + obtain ⟨x, y, t, _, ⟨γp, hγp, hγm⟩, hs0, hvs⟩ := D.gamma p hp hpN (by omega) + obtain ⟨_, S10, S11, _⟩ := int_facts_sG D hgN hg he hγp hγm + have s10 := le_vv2 (B := B) hs0 hBh S10 + have s11 := le_vv2 (B := B) (mul_ne_zero hs0 hhz) hBN S11 + simp only [vX _ hNz, vX _ hhz, vz_mul hs0 hhz, hvs, vh, vN] at s10 s11 + exact ⟨by omega, by omega⟩ + have := local_form_gen ν j k δ₀ a b c d hkj prim u1 (by omega) (by omega) (by omega) + (by omega) C10 C11 + have hn2 : ν - 2 * k = nν := by omega + rw [hn2] at this + exact this + +/-- **Newman's argument for Γ**: every element of the normalizer of Γ has the form `IsNewmanFormH` +with parameter η. -/ +theorem newmanG {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (D : NewmanData N Γ ε η) (hg : g ∈ NormG Γ) : + IsNewmanFormH N η g := by + obtain ⟨κ, α, β, γ, δ, hκ, hprim, hgm⟩ := exists_prim_formG D hg + have hh : η ≠ 0 := D.h_pos.ne' + have hhr : (η : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hh + have hN := NeZero.ne N + have hgS : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (η) α β γ δ := by rw [hgm]; rfl + have hdet : κ ^ 2 * ((α * δ - β * γ : ℤ) : ℝ) = 1 := by + have := g.2 + rw [hgS, det_smul, Fintype.card_fin, det_Smat hh] at this + exact this + have he : α * δ - β * γ ≠ 0 := by + intro h0 + rw [h0] at hdet + simp at hdet + have hepos : 0 < α * δ - β * γ := by + have hκ2 : 0 < κ ^ 2 := by positivity + have : (0 : ℝ) < ((α * δ - β * γ : ℤ) : ℝ) := by + by_contra hc + push Not at hc + nlinarith + exact_mod_cast this + have hloc := fun (p : ℕ) (hp : p.Prime) => local_conclusionG D hg hgS he hprim hp + have hn0 : nOf N η ≠ 0 := by + intro h0 + have := D.n_mul_sq + rw [h0, zero_mul] at this + exact hN this.symm + have hnz : (nOf N η : ℤ) ≠ 0 := Nat.cast_ne_zero.2 hn0 + -- e ∣ n, n ∣ γ, e ∣ α, e ∣ δ + have hen : (α * δ - β * γ) ∣ (nOf N η : ℤ) := by + refine dvd_of_forall_vz_le he hnz (fun p hp => ?_) + have := hloc p hp + simp only at this + rw [vz_natCast] + rcases this with ⟨h1, -⟩ | ⟨h1, -⟩ <;> omega + have hnγ : (nOf N η : ℤ) ∣ γ := by + by_cases hγ : γ = 0 + · rw [hγ]; exact dvd_zero _ + refine dvd_of_forall_vz_le hnz hγ (fun p hp => ?_) + have := hloc p hp + simp only [vv_of_ne hγ] at this + rw [vz_natCast] + rcases this with ⟨-, h2⟩ | ⟨-, -, h2, -⟩ <;> omega + have heα : (α * δ - β * γ) ∣ α := by + by_cases hα : α = 0 + · rw [hα]; exact dvd_zero _ + refine dvd_of_forall_vz_le he hα (fun p hp => ?_) + have := hloc p hp + simp only [vv_of_ne hα] at this + rcases this with ⟨h1, -⟩ | ⟨h1, h2, -⟩ <;> omega + have heδ : (α * δ - β * γ) ∣ δ := by + by_cases hδ : δ = 0 + · rw [hδ]; exact dvd_zero _ + refine dvd_of_forall_vz_le he hδ (fun p hp => ?_) + have := hloc p hp + simp only [vv_of_ne hδ] at this + rcases this with ⟨h1, -⟩ | ⟨h1, -, -, h2⟩ <;> omega + obtain ⟨a', ha'⟩ := heα + obtain ⟨d', hd'⟩ := heδ + obtain ⟨c', hc'⟩ := hnγ + obtain ⟨m, hm⟩ := hen + set E := α * δ - β * γ with hE + -- e as a natural number + set e : ℕ := E.toNat with he_def + have hEe : (e : ℤ) = E := Int.toNat_of_nonneg hepos.le + have he0 : 0 < e := by omega + have her : (e : ℝ) = (E : ℝ) := by exact_mod_cast hEe + have hsq : Real.sqrt e * Real.sqrt e = e := Real.mul_self_sqrt (Nat.cast_nonneg _) + have hs0 : Real.sqrt e ≠ 0 := (Real.sqrt_pos.2 (Nat.cast_pos.2 he0)).ne' + refine ⟨a', β, c', d', e, he0, ⟨m.toNat, ?_⟩, ?_, κ * Real.sqrt e, ?_, ?_⟩ + · have hm0 : 0 ≤ m := by + by_contra hneg + push Not at hneg + have : (nOf N η : ℤ) < 0 := by rw [hm]; exact mul_neg_of_pos_of_neg hepos hneg + omega + have : ((nOf N η : ℕ) : ℤ) = ((e * m.toNat : ℕ) : ℤ) := by + push_cast + rw [Int.toNat_of_nonneg hm0, hEe] + exact hm + exact_mod_cast this + · rw [hEe] + have h1 : E = α * δ - β * γ := rfl + rw [ha', hd', hc'] at h1 + simp only [nOf] at h1 ⊢ + linear_combination -h1 + · have h1 : (κ * Real.sqrt e) ^ 2 = 1 := by + rw [mul_pow, Real.sq_sqrt (Nat.cast_nonneg _), her] + exact hdet + have h2 : (κ * Real.sqrt e) * (κ * Real.sqrt e) = 1 := by rw [← pow_two]; exact h1 + exact mul_self_eq_one_iff.1 h2 + · have hNr : (N : ℝ) = nOf N η * (η : ℝ) ^ 2 := by + exact_mod_cast D.n_mul_sq.symm + have hα' : (α : ℝ) = a' * e := by rw [her, ha']; push_cast; ring + have hγ' : (γ : ℝ) = nOf N η * c' := by rw [hc']; push_cast; ring + have hδ' : (δ : ℝ) = d' * e := by rw [her, hd']; push_cast; ring + rw [hgm, mul_div_assoc, div_self hs0, mul_one] + congr 1 + ext i j + fin_cases i <;> fin_cases j <;> simp [hα', hγ', hδ', hNr] ; field_simp + +end + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerLean/AtkinLehner.lean b/LeanPool/CongruenceNormalizers/NormalizerLean/AtkinLehner.lean new file mode 100644 index 000000000..57cbccbed --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerLean/AtkinLehner.lean @@ -0,0 +1,192 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerLean.Basic + +/-! +# T1 for Atkin–Lehner elements and translations + +* `S_mem_normalizer'`: S_k normalizes Γ₀(N) for k ∣ h(N); +* `isAtkinLehner_mem_normalizer'`: every AL element w_Q (Q ∣ N) normalizes Γ₀(N); +* `exists_isAtkinLehner'`: AL elements exist for Q ∥ N; +* `isAtkinLehner_mul_inv_mem'`: two AL elements for Q differ by Γ₀(N). + +The AL computations are the identities W γ adj(W) = Q·M₁, adj(W) γ W = Q·M₂, W adj(W') = Q·M₃ +with explicit integer matrices Mᵢ (checked symbolically in sympy before being given to `ring`). +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +/-! ### Scalar bookkeeping -/ + +theorem inv_mul_inv_mul_eq_one {Q s : ℝ} (hs : s * s = Q) (hQ : Q ≠ 0) : s⁻¹ * s⁻¹ * Q = 1 := by + have hs0 : s ≠ 0 := by + rintro rfl + exact hQ (by simpa using hs.symm) + rw [← hs] + field_simp + +theorem smul_mul_mul_smul_eq {Q s : ℝ} (hs : s * s = Q) (hQ : Q ≠ 0) + {W γ A X : Matrix (Fin 2) (Fin 2) ℝ} (h : W * γ * A = Q • X) : + (s⁻¹ • W) * γ * (s⁻¹ • A) = X := by + rw [Matrix.smul_mul, Matrix.smul_mul, Matrix.mul_smul, smul_smul, h, smul_smul, + inv_mul_inv_mul_eq_one hs hQ, one_smul] + +theorem smul_mul_smul_eq {Q s : ℝ} (hs : s * s = Q) (hQ : Q ≠ 0) + {W A X : Matrix (Fin 2) (Fin 2) ℝ} (h : W * A = Q • X) : + (s⁻¹ • W) * (s⁻¹ • A) = X := by + rw [Matrix.smul_mul, Matrix.mul_smul, smul_smul, h, smul_smul, + inv_mul_inv_mul_eq_one hs hQ, one_smul] + +theorem coe_inv_of_coe_eq_smul {g : SL(2, ℝ)} {s a b c d : ℝ} + (h : (g : Matrix (Fin 2) (Fin 2) ℝ) = s • !![a, b; c, d]) : + ((g⁻¹ : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) = s • !![d, -b; -c, a] := by + rw [Matrix.SpecialLinearGroup.coe_inv, h, adjugate_smul, adjugate_fin_two_of] + simp + +/-! ### Translations -/ + +theorem S_conj_mem {N k : ℕ} (hN : N ≠ 0) (hk : k ∣ hPart N) {γ : SL(2, ℝ)} + (hγ : γ ∈ Gamma0R N) : + S k * γ * (S k)⁻¹ ∈ Gamma0R N ∧ (S k)⁻¹ * γ * S k ∈ Gamma0R N := by + have hk24 : k ∣ 24 := dvd_trans hk (hPart_dvd_24 N) + have hk0 : k ≠ 0 := by + rintro rfl + exact (hPart_pos N).ne' (Nat.eq_zero_of_zero_dvd hk) + have hksq : k ^ 2 ∣ N := dvd_trans (pow_dvd_pow_of_dvd hk 2) (hPart_sq_dvd hN) + obtain ⟨a, b, c, d, hdet, hc, hγm⟩ := exists_entries_of_mem_Gamma0R hγ + have hkc : ((k : ℤ) ^ 2) ∣ c := dvd_trans (by exact_mod_cast hksq) hc + -- a ≡ d (mod k) + have had : a * d ≡ 1 [ZMOD k] := by + have hkc1 : (k : ℤ) ∣ c := dvd_trans (dvd_pow_self _ two_ne_zero) hkc + apply Int.ModEq.symm + rw [Int.modEq_iff_dvd, show a * d - 1 = b * c by linarith] + exact dvd_mul_of_dvd_right hkc1 b + obtain ⟨e, he⟩ := (Int.ModEq.dvd (modEq_of_mul_modEq_one hk24 had)) + obtain ⟨c', rfl⟩ := hkc + have hd : d = a + k * e := by linarith + subst hd + have hkr : (k : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hk0 + constructor + · refine mem_Gamma0R_of_entries (a + k * c') (b + e - c') (k ^ 2 * c') (a + k * e - k * c') + ?_ hc + rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.SpecialLinearGroup.coe_mul, hγm, coe_S, + coe_S_inv, mul_fin_two, mul_fin_two] + ext i j + fin_cases i <;> fin_cases j <;> simp <;> field_simp <;> ring + · refine mem_Gamma0R_of_entries (a - k * c') (b - e - c') (k ^ 2 * c') (a + k * e + k * c') + ?_ hc + rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.SpecialLinearGroup.coe_mul, hγm, coe_S, + coe_S_inv, mul_fin_two, mul_fin_two] + ext i j + fin_cases i <;> fin_cases j <;> simp <;> field_simp <;> ring + +/-- **T1** for translations. -/ +theorem S_mem_normalizer' {N k : ℕ} [NeZero N] (hk : k ∣ hPart N) : S k ∈ Norm0 N := + mem_Norm0_of (fun _ hγ => (S_conj_mem (NeZero.ne N) hk hγ).1) + (fun _ hγ => (S_conj_mem (NeZero.ne N) hk hγ).2) + +/-! ### Atkin–Lehner elements -/ + +theorem isAtkinLehner_conj_mem {N Q : ℕ} (hQ : Q ∣ N) (hQ0 : Q ≠ 0) {g : SL(2, ℝ)} + (hg : IsAtkinLehner N Q g) {γ : SL(2, ℝ)} (hγ : γ ∈ Gamma0R N) : + g * γ * g⁻¹ ∈ Gamma0R N ∧ g⁻¹ * γ * g ∈ Gamma0R N := by + obtain ⟨x, y, z, w, -, hgm⟩ := hg + obtain ⟨K, rfl⟩ := hQ + obtain ⟨a, b, c', d, -, ⟨c, rfl⟩, hγm⟩ := exists_entries_of_mem_Gamma0R hγ + have hs : Real.sqrt Q * Real.sqrt Q = Q := Real.mul_self_sqrt (Nat.cast_nonneg _) + have hQr : (Q : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hQ0 + have hginv := coe_inv_of_coe_eq_smul hgm + constructor + · refine mem_Gamma0R_of_entries + ((Q : ℤ) * w * (x * a + y * (K : ℤ) * c) - (K : ℤ) * z * ((Q : ℤ) * x * b + y * d)) + (-y * (x * a + y * (K : ℤ) * c) + x * ((Q : ℤ) * x * b + y * d)) + (((Q * K : ℕ) : ℤ) * (w * (z * a + (Q : ℤ) * w * c) - z * ((K : ℤ) * z * b + w * d))) + (-(K : ℤ) * y * (z * a + (Q : ℤ) * w * c) + (Q : ℤ) * x * ((K : ℤ) * z * b + w * d)) ?_ + (dvd_mul_right _ _) + rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.SpecialLinearGroup.coe_mul, hgm, hγm, hginv] + apply smul_mul_mul_smul_eq hs hQr + rw [mul_fin_two, mul_fin_two] + ext i j + fin_cases i <;> fin_cases j <;> simp <;> ring + · refine mem_Gamma0R_of_entries + ((Q : ℤ) * x * (w * a - y * (K : ℤ) * c) + (K : ℤ) * z * ((Q : ℤ) * w * b - y * d)) + (y * (w * a - y * (K : ℤ) * c) + w * ((Q : ℤ) * w * b - y * d)) + (((Q * K : ℕ) : ℤ) * (x * (-z * a + (Q : ℤ) * x * c) + z * (x * d - (K : ℤ) * z * b))) + ((K : ℤ) * y * (-z * a + (Q : ℤ) * x * c) + (Q : ℤ) * w * (x * d - (K : ℤ) * z * b)) ?_ + (dvd_mul_right _ _) + rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.SpecialLinearGroup.coe_mul, hgm, hγm, hginv] + apply smul_mul_mul_smul_eq hs hQr + rw [mul_fin_two, mul_fin_two] + ext i j + fin_cases i <;> fin_cases j <;> simp <;> ring + +/-- **T1** for Atkin–Lehner elements. -/ +theorem isAtkinLehner_mem_normalizer' {N Q : ℕ} [NeZero N] (hQ : Q ∣ N) {g : SL(2, ℝ)} + (hg : IsAtkinLehner N Q g) : g ∈ Norm0 N := by + have hQ0 : Q ≠ 0 := by + rintro rfl + exact NeZero.ne N (Nat.eq_zero_of_zero_dvd hQ) + exact mem_Norm0_of (fun _ hγ => (isAtkinLehner_conj_mem hQ hQ0 hg hγ).1) + (fun _ hγ => (isAtkinLehner_conj_mem hQ hQ0 hg hγ).2) + +/-- The AL element with explicit integer data. -/ +def alElt (N Q : ℕ) (x y z w : ℤ) (h : (Q : ℤ) ^ 2 * x * w - N * y * z = Q) (hQ : Q ≠ 0) : + SL(2, ℝ) := + ⟨(Real.sqrt Q)⁻¹ • !![(Q : ℝ) * x, (y : ℝ); (N : ℝ) * z, (Q : ℝ) * w], by + have hr : (Q : ℝ) ^ 2 * x * w - N * y * z = Q := by exact_mod_cast h + have hQr : (Q : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hQ + rw [det_smul, Fintype.card_fin, det_fin_two_of, inv_pow, Real.sq_sqrt (Nat.cast_nonneg _)] + rw [show (Q : ℝ) * x * (Q * w) - y * (N * z) = Q by linear_combination hr] + exact inv_mul_cancel₀ hQr⟩ + +theorem alElt_isAtkinLehner {N Q : ℕ} {x y z w : ℤ} (h) (hQ) : + IsAtkinLehner N Q (alElt N Q x y z w h hQ) := ⟨x, y, z, w, h, rfl⟩ + +/-- Atkin–Lehner elements exist for Q ∥ N. -/ +theorem exists_isAtkinLehner' {N Q : ℕ} [NeZero N] (hQ : Q ∣ N) (hcop : Nat.Coprime Q (N / Q)) : + ∃ g, IsAtkinLehner N Q g := by + have hQ0 : Q ≠ 0 := by + rintro rfl + exact NeZero.ne N (Nat.eq_zero_of_zero_dvd hQ) + obtain ⟨K, rfl⟩ := hQ + rw [Nat.mul_div_cancel_left _ (Nat.pos_of_ne_zero hQ0)] at hcop + have hb := Int.gcd_eq_gcd_ab Q K + rw [Int.gcd_natCast_natCast, hcop] at hb + refine ⟨alElt (Q * K) Q (Int.gcdA Q K) (-Int.gcdB Q K) 1 1 ?_ hQ0, alElt_isAtkinLehner _ _⟩ + push_cast + linear_combination (Q : ℤ) * hb.symm + +theorem isAtkinLehner_mul_inv_mem' {N Q : ℕ} [NeZero N] (hQ : Q ∣ N) {g g' : SL(2, ℝ)} + (hg : IsAtkinLehner N Q g) (hg' : IsAtkinLehner N Q g') : g * g'⁻¹ ∈ Gamma0R N := by + have hQ0 : Q ≠ 0 := by + rintro rfl + exact NeZero.ne N (Nat.eq_zero_of_zero_dvd hQ) + obtain ⟨x, y, z, w, -, hgm⟩ := hg + obtain ⟨x2, y2, z2, w2, -, hgm'⟩ := hg' + obtain ⟨K, rfl⟩ := hQ + have hs : Real.sqrt Q * Real.sqrt Q = Q := Real.mul_self_sqrt (Nat.cast_nonneg _) + have hQr : (Q : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hQ0 + have hginv := coe_inv_of_coe_eq_smul hgm' + refine mem_Gamma0R_of_entries ((Q : ℤ) * x * w2 - (K : ℤ) * y * z2) (x2 * y - x * y2) + (((Q * K : ℕ) : ℤ) * (z * w2 - w * z2)) ((Q : ℤ) * w * x2 - (K : ℤ) * z * y2) ?_ + (dvd_mul_right _ _) + rw [Matrix.SpecialLinearGroup.coe_mul, hgm, hginv] + apply smul_mul_smul_eq hs hQr + rw [mul_fin_two] + ext i j + fin_cases i <;> fin_cases j <;> simp <;> ring + +end + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerLean/Basic.lean b/LeanPool/CongruenceNormalizers/NormalizerLean/Basic.lean new file mode 100644 index 000000000..17284580d --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerLean/Basic.lean @@ -0,0 +1,219 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerLean.Defs + +/-! +# Basic API for Γ₀(N) ≤ SL₂(ℝ), its normalizer, B(N), S_k and h(N) +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +/-! ### Membership in Γ₀(N) -/ + +/-- The real matrix of an integer matrix. -/ +abbrev castM (M : Matrix (Fin 2) (Fin 2) ℤ) : Matrix (Fin 2) (Fin 2) ℝ := M.map (Int.cast) + +theorem mem_Gamma0R_iff {N : ℕ} {g : SL(2, ℝ)} : + g ∈ Gamma0R N ↔ ∃ M : Matrix (Fin 2) (Fin 2) ℤ, + (N : ℤ) ∣ M 1 0 ∧ (g : Matrix (Fin 2) (Fin 2) ℝ) = castM M := by + constructor + · rintro ⟨A, hA, rfl⟩ + refine ⟨A, ?_, ?_⟩ + · exact (ZMod.intCast_zmod_eq_zero_iff_dvd _ _).1 (CongruenceSubgroup.Gamma0_mem.1 hA) + · ext i j + simp [Matrix.SpecialLinearGroup.map_apply_coe, RingHom.mapMatrix_apply] + · rintro ⟨M, hM, hg⟩ + have hdet : M.det = 1 := by + have h1 := g.2 + rw [hg, det_fin_two] at h1 + rw [det_fin_two] + simp only [castM, map_apply] at h1 + exact_mod_cast h1 + let A : SL(2, ℤ) := ⟨M, hdet⟩ + refine ⟨A, CongruenceSubgroup.Gamma0_mem.2 ((ZMod.intCast_zmod_eq_zero_iff_dvd _ _).2 hM), ?_⟩ + refine Matrix.SpecialLinearGroup.ext _ _ (fun i j => ?_) + rw [Matrix.SpecialLinearGroup.map_apply_coe, hg] + rfl + +/-- Membership in Γ₀(N) from explicit integer entries. -/ +theorem mem_Gamma0R_of_entries {N : ℕ} {g : SL(2, ℝ)} (a b c d : ℤ) + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = !![(a : ℝ), b; c, d]) (hc : (N : ℤ) ∣ c) : + g ∈ Gamma0R N := by + refine mem_Gamma0R_iff.2 ⟨!![a, b; c, d], by simpa using hc, ?_⟩ + rw [hg] + ext i j + fin_cases i <;> fin_cases j <;> simp + +/-- Elements of Γ₀(N) have integer entries, lower-left divisible by N, determinant 1. -/ +theorem exists_entries_of_mem_Gamma0R {N : ℕ} {g : SL(2, ℝ)} (hg : g ∈ Gamma0R N) : + ∃ a b c d : ℤ, a * d - b * c = 1 ∧ (N : ℤ) ∣ c ∧ + (g : Matrix (Fin 2) (Fin 2) ℝ) = !![(a : ℝ), b; c, d] := by + obtain ⟨M, hM, hgM⟩ := mem_Gamma0R_iff.1 hg + refine ⟨M 0 0, M 0 1, M 1 0, M 1 1, ?_, hM, ?_⟩ + · have h1 := g.2 + rw [hgM, det_fin_two] at h1 + simp only [castM, map_apply] at h1 + exact_mod_cast h1 + · rw [hgM] + ext i j + fin_cases i <;> fin_cases j <;> simp + +/-! ### The normalizer -/ + +/-- Normalizer criterion: g Γ g⁻¹ ⊆ Γ and g⁻¹ Γ g ⊆ Γ. -/ +theorem mem_Norm0_of {N : ℕ} {g : SL(2, ℝ)} + (h₁ : ∀ γ ∈ Gamma0R N, g * γ * g⁻¹ ∈ Gamma0R N) + (h₂ : ∀ γ ∈ Gamma0R N, g⁻¹ * γ * g ∈ Gamma0R N) : g ∈ Norm0 N := by + rw [Subgroup.mem_normalizer_iff] + intro γ + refine ⟨h₁ γ, fun h => ?_⟩ + have := h₂ _ h + simpa [mul_assoc] using this + +theorem Gamma0R_le_Norm0 (N : ℕ) : Gamma0R N ≤ Norm0 N := + Subgroup.le_normalizer + +/-! ### B(N) -/ + +theorem B.isClassOf_mk {N : ℕ} {g : SL(2, ℝ)} (hg : g ∈ Norm0 N) : + B.IsClassOf (QuotientGroup.mk ⟨g, hg⟩ : B N) g := ⟨hg, rfl⟩ + +theorem B.mk_eq_mk_iff {N : ℕ} {g g' : SL(2, ℝ)} (hg : g ∈ Norm0 N) (hg' : g' ∈ Norm0 N) : + (QuotientGroup.mk ⟨g, hg⟩ : B N) = QuotientGroup.mk ⟨g', hg'⟩ ↔ g⁻¹ * g' ∈ Gamma0R N := by + rw [QuotientGroup.eq, Subgroup.mem_subgroupOf] + rfl + +theorem B.mk_eq_one_iff {N : ℕ} {g : SL(2, ℝ)} (hg : g ∈ Norm0 N) : + (QuotientGroup.mk ⟨g, hg⟩ : B N) = 1 ↔ g ∈ Gamma0R N := by + rw [QuotientGroup.eq_one_iff, Subgroup.mem_subgroupOf] + +/-- In the normalizer, `a * b⁻¹ ∈ Γ ↔ a⁻¹ * b ∈ Γ`. -/ +theorem mul_inv_mem_iff_inv_mul_mem {N : ℕ} {a b : SL(2, ℝ)} (ha : a ∈ Norm0 N) : + a * b⁻¹ ∈ Gamma0R N ↔ a⁻¹ * b ∈ Gamma0R N := by + have key : ∀ x, x ∈ Gamma0R N ↔ a⁻¹ * x * a ∈ Gamma0R N := by + intro x + have := (Subgroup.mem_normalizer_iff.1 (inv_mem ha)) x + simpa using this + rw [key (a * b⁻¹), ← inv_mem_iff (x := a⁻¹ * b)] + simp + +/-! ### Translations S_k -/ + +theorem coe_S (k : ℕ) : ((S k : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) = !![1, (k : ℝ)⁻¹; 0, 1] := + rfl + +theorem coe_S_pow (k m : ℕ) : + ((S k ^ m : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) = !![1, (m : ℝ) * (k : ℝ)⁻¹; 0, 1] := by + induction m with + | zero => + ext i j + fin_cases i <;> fin_cases j <;> simp + | succ m ih => + rw [pow_succ, Matrix.SpecialLinearGroup.coe_mul, ih, coe_S, mul_fin_two] + congr 1 + simp only [mul_one, mul_zero, add_zero, one_mul, Nat.cast_succ] + ring_nf + +theorem coe_S_inv (k : ℕ) : + (((S k)⁻¹ : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) = !![1, -(k : ℝ)⁻¹; 0, 1] := by + rw [Matrix.SpecialLinearGroup.coe_inv, coe_S, adjugate_fin_two_of] + simp + +theorem S_one_mem (N : ℕ) : S 1 ∈ Gamma0R N := + mem_Gamma0R_of_entries 1 1 0 1 (by rw [coe_S]; simp) (dvd_zero _) + +/-! ### h(N) -/ + +theorem hPart_pos (N : ℕ) : 0 < hPart N := by + unfold hPart + positivity + +theorem hPart_dvd_24 (N : ℕ) : hPart N ∣ 24 := by + unfold hPart + have h2 : 2 ^ min 3 (N.factorization 2 / 2) ∣ 2 ^ 3 := pow_dvd_pow _ (min_le_left _ _) + have h3 : 3 ^ min 1 (N.factorization 3 / 2) ∣ 3 ^ 1 := pow_dvd_pow _ (min_le_left _ _) + have := mul_dvd_mul h2 h3 + simpa using this + +/-- Key divisibility: if (2^α 3^β)² ∣ N with α ≤ 3, β ≤ 1, then 2^α 3^β ∣ h(N). -/ +theorem dvd_hPart_of_sq_dvd {N : ℕ} (hN : N ≠ 0) {α β : ℕ} (hα : α ≤ 3) (hβ : β ≤ 1) + (h : (2 ^ α * 3 ^ β) ^ 2 ∣ N) : 2 ^ α * 3 ^ β ∣ hPart N := by + unfold hPart + have hsplit : (2 ^ α * 3 ^ β) ^ 2 = 2 ^ (2 * α) * 3 ^ (2 * β) := by ring + rw [hsplit] at h + have h2 : 2 ^ (2 * α) ∣ N := dvd_trans (dvd_mul_right _ _) h + have h3 : 3 ^ (2 * β) ∣ N := dvd_trans (dvd_mul_left _ _) h + rw [Nat.prime_two.pow_dvd_iff_le_factorization hN] at h2 + rw [Nat.prime_three.pow_dvd_iff_le_factorization hN] at h3 + refine mul_dvd_mul (pow_dvd_pow _ ?_) (pow_dvd_pow _ ?_) + · exact le_min hα (by omega) + · exact le_min hβ (by omega) + +theorem hPart_sq_dvd {N : ℕ} (hN : N ≠ 0) : hPart N ^ 2 ∣ N := by + unfold hPart + rw [mul_pow, ← pow_mul, ← pow_mul] + have hc : Nat.Coprime (2 ^ (min 3 (N.factorization 2 / 2) * 2)) + (3 ^ (min 1 (N.factorization 3 / 2) * 2)) := + Nat.Coprime.pow _ _ (by norm_num) + refine hc.mul_dvd_of_dvd_of_dvd ?_ ?_ + · rw [Nat.prime_two.pow_dvd_iff_le_factorization hN] + have := Nat.div_mul_le_self (N.factorization 2) 2 + have := min_le_right 3 (N.factorization 2 / 2) + nlinarith + · rw [Nat.prime_three.pow_dvd_iff_le_factorization hN] + have := Nat.div_mul_le_self (N.factorization 3) 2 + have := min_le_right 1 (N.factorization 3 / 2) + nlinarith + +theorem dvd_hPart_iff {N : ℕ} (hN : N ≠ 0) {d : ℕ} (hd : d ∣ 24) (hsq : d ^ 2 ∣ N) : + d ∣ hPart N := by + have hd24 : d ≤ 24 := Nat.le_of_dvd (by norm_num) hd + interval_cases d <;> norm_num at hd + · exact one_dvd _ + · exact (dvd_hPart_of_sq_dvd hN (α := 1) (β := 0) (by norm_num) (by norm_num) (by simpa using + hsq)) + · exact (dvd_hPart_of_sq_dvd hN (α := 0) (β := 1) (by norm_num) (by norm_num) (by simpa using + hsq)) + · exact (dvd_hPart_of_sq_dvd hN (α := 2) (β := 0) (by norm_num) (by norm_num) (by simpa using + hsq)) + · exact (dvd_hPart_of_sq_dvd hN (α := 1) (β := 1) (by norm_num) (by norm_num) (by simpa using + hsq)) + · exact (dvd_hPart_of_sq_dvd hN (α := 3) (β := 0) (by norm_num) (by norm_num) (by simpa using + hsq)) + · exact (dvd_hPart_of_sq_dvd hN (α := 2) (β := 1) (by norm_num) (by norm_num) (by simpa using + hsq)) + · exact (dvd_hPart_of_sq_dvd hN (α := 3) (β := 1) (by norm_num) (by norm_num) (by simpa using + hsq)) + +theorem hPart_isGreatest' (N : ℕ) [NeZero N] : + IsGreatest {d : ℕ | d ∣ 24 ∧ d ^ 2 ∣ N} (hPart N) := by + refine ⟨⟨hPart_dvd_24 N, hPart_sq_dvd (NeZero.ne N)⟩, ?_⟩ + rintro d ⟨hd, hsq⟩ + exact Nat.le_of_dvd (hPart_pos N) (dvd_hPart_iff (NeZero.ne N) hd hsq) + +/-! ### Units modulo divisors of 24 square to 1 -/ + +theorem modEq_of_mul_modEq_one {k : ℕ} (hk : k ∣ 24) {a d : ℤ} (h : a * d ≡ 1 [ZMOD k]) : + a ≡ d [ZMOD k] := by + have hk24 : k ≤ 24 := Nat.le_of_dvd (by norm_num) hk + rw [← ZMod.intCast_eq_intCast_iff] at h ⊢ + push_cast at h + generalize (a : ZMod k) = x at h ⊢ + generalize (d : ZMod k) = y at h ⊢ + revert x y + interval_cases k <;> norm_num at hk <;> decide + +end + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerLean/Defs.lean b/LeanPool/CongruenceNormalizers/NormalizerLean/Defs.lean new file mode 100644 index 000000000..eaf63985a --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerLean/Defs.lean @@ -0,0 +1,178 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import Mathlib.Analysis.Real.Sqrt +public import Mathlib.Algebra.Group.Subgroup.Basic +public import Mathlib.GroupTheory.QuotientGroup.Basic +public import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups +public import Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp +public import Mathlib.Tactic.FieldSimp +public import Mathlib.Tactic.FinCases +public import Mathlib.Tactic.IntervalCases +public import Mathlib.Tactic.LinearCombination +public import Mathlib.Tactic.NormNum +public import Mathlib.Tactic.Positivity +public import Mathlib.Tactic.Push +public import Mathlib.Tactic.Ring + +/-! +# 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). +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +/-! ## Definitions -/ + +/-- Γ₀(N) as a subgroup of SL₂(ℝ): the image of Mathlib's `CongruenceSubgroup.Gamma0 N ≤ SL(2, +ℤ)`. -/ +def Gamma0R (N : ℕ) : Subgroup SL(2, ℝ) := + (CongruenceSubgroup.Gamma0 N).map (SpecialLinearGroup.map (Int.castRingHom ℝ)) + +/-- The normalizer of Γ₀(N) in SL₂(ℝ). -/ +abbrev Norm0 (N : ℕ) : Subgroup SL(2, ℝ) := + Subgroup.normalizer (Gamma0R N : Set SL(2, ℝ)) + +/-- **B(N) = Norm_{SL₂(ℝ)}(Γ₀(N)) / Γ₀(N).** -/ +abbrev B (N : ℕ) : Type := + Norm0 N ⧸ (Gamma0R N).subgroupOf (Norm0 N) + +instance (N : ℕ) : ((Gamma0R N).subgroupOf (Norm0 N)).Normal := + Subgroup.normal_in_normalizer + +/-- `x : B N` is the class of the real matrix `g`: `g` normalizes Γ₀(N) and `x = g Γ₀(N)`. -/ +def B.IsClassOf {N : ℕ} (x : B N) (g : SL(2, ℝ)) : Prop := + ∃ hg : g ∈ Norm0 N, x = QuotientGroup.mk ⟨g, hg⟩ + +/-- 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. -/ +def projSL (A : Matrix (Fin 2) (Fin 2) ℝ) : SL(2, ℝ) := + if hA : 0 < A.det then + ⟨(Real.sqrt A.det)⁻¹ • A, by + rw [det_smul, Fintype.card_fin, inv_pow, Real.sq_sqrt hA.le, inv_mul_cancel₀ hA.ne']⟩ + else 1 + +/-- 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. -/ +def hPart (N : ℕ) : ℕ := + 2 ^ min 3 (N.factorization 2 / 2) * 3 ^ min 1 (N.factorization 3 / 2) + +/-- n(N) = N / h(N)². -/ +def nPart (N : ℕ) : ℕ := N / hPart N ^ 2 + +/-- S_k = [[1, 1/k], [0, 1]]. -/ +def S (k : ℕ) : SL(2, ℝ) := + ⟨!![1, (k : ℝ)⁻¹; 0, 1], by simp [det_fin_two]⟩ + +/-- `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. -/ +def IsAtkinLehner (N Q : ℕ) (g : SL(2, ℝ)) : Prop := + ∃ x y z w : ℤ, (Q : ℤ) ^ 2 * x * w - N * y * z = Q ∧ + (g : Matrix (Fin 2) (Fin 2) ℝ) = + (Real.sqrt Q)⁻¹ • !![(Q : ℝ) * x, (y : ℝ); (N : ℝ) * z, (Q : ℝ) * w] + +/-- `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. -/ +def IsNewmanFormH (N h : ℕ) (g : SL(2, ℝ)) : Prop := + ∃ (a b c d : ℤ) (e : ℕ), 0 < e ∧ e ∣ N / h ^ 2 ∧ + a * d * (e : ℤ) ^ 2 - b * c * ((N / h ^ 2 : ℕ) : ℤ) = e ∧ + ∃ ε : ℝ, (ε = 1 ∨ ε = -1) ∧ + (g : Matrix (Fin 2) (Fin 2) ℝ) = + (ε / Real.sqrt e) • + !![(a : ℝ) * e, (b : ℝ) / h; (N : ℝ) * c / h, (d : ℝ) * e] + + +/-- Newman's form with the canonical Γ₀(N) square-divisor parameter. -/ +def IsNewmanForm (N : ℕ) (g : SL(2, ℝ)) : Prop := IsNewmanFormH N (hPart N) g + +/-- D = diag(h, 1), rescaled into SL₂(ℝ): `diag(√h, 1/√h)`. Conjugation by it equals conjugation +by D. -/ +def Dsl (N : ℕ) : SL(2, ℝ) := projSL !![(hPart N : ℝ), 0; 0, 1] + +/-- D⁻¹ Γ₀(n) D ≤ SL₂(ℝ). -/ +def conjGamma0n (N : ℕ) : Subgroup SL(2, ℝ) := + (Gamma0R (nPart N)).map (MulAut.conj (Dsl N)⁻¹).toMonoidHom + +/-- The image in SL₂(ℝ) of a subgroup of SL₂(ℤ). -/ +def toR (Γ : Subgroup SL(2, ℤ)) : Subgroup SL(2, ℝ) := + Γ.map (SpecialLinearGroup.map (Int.castRingHom ℝ)) + +/-- The normalizer of Γ in SL₂(ℝ). -/ +abbrev NormG (Γ : Subgroup SL(2, ℝ)) : Subgroup SL(2, ℝ) := + Subgroup.normalizer (Γ : Set SL(2, ℝ)) + +/-! ## Γ_Δ(N) -/ + +/-- Γ_Δ(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.) -/ +def GammaDelta (N : ℕ) (Δ : Subgroup (ZMod N)ˣ) : Subgroup SL(2, ℤ) where + carrier := {γ | γ ∈ CongruenceSubgroup.Gamma0 N ∧ + ∃ u ∈ Δ, (u : ZMod N) = ((γ 1 1 : ℤ) : ZMod N)} + one_mem' := ⟨Subgroup.one_mem _, 1, Subgroup.one_mem _, by simp⟩ + mul_mem' := by + rintro γ γ' ⟨h0, u, hu, hγ⟩ ⟨h0', u', hu', hγ'⟩ + refine ⟨Subgroup.mul_mem _ h0 h0', u * u', Subgroup.mul_mem _ hu hu', ?_⟩ + have hc : ((γ 1 0 : ℤ) : ZMod N) = 0 := CongruenceSubgroup.Gamma0_mem.1 h0 + have e : ((γ * γ') 1 1 : ℤ) = γ 1 0 * γ' 0 1 + γ 1 1 * γ' 1 1 := by + simp [Matrix.mul_apply, Fin.sum_univ_two] + rw [Units.val_mul, hγ, hγ', e] + push_cast + rw [hc, zero_mul, zero_add] + inv_mem' := by + rintro γ ⟨h0, u, hu, hγ⟩ + refine ⟨Subgroup.inv_mem _ h0, u⁻¹, Subgroup.inv_mem _ hu, ?_⟩ + have hc : ((γ 1 0 : ℤ) : ZMod N) = 0 := CongruenceSubgroup.Gamma0_mem.1 h0 + have hdet : ((γ 0 0 : ℤ) : ZMod N) * ((γ 1 1 : ℤ) : ZMod N) = 1 := by + have h := congrArg (fun x : ℤ => (x : ZMod N)) γ.2 + simp only [Matrix.det_fin_two, Int.cast_sub, Int.cast_mul, Int.cast_one] at h + rw [hc, mul_zero, sub_zero] at h + exact h + have e : (γ⁻¹ 1 1 : ℤ) = γ 0 0 := by + simp [Matrix.adjugate_fin_two] + rw [e] + rw [← hγ] at hdet + exact Units.inv_eq_of_mul_eq_one_left hdet + +/-- Γ_Δ(N) in SL₂(ℝ). -/ +def GammaDeltaR (N : ℕ) (Δ : Subgroup (ZMod N)ˣ) : Subgroup SL(2, ℝ) := toR (GammaDelta 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. -/ +def epsDelta (N : ℕ) [NeZero N] (Δ : Subgroup (ZMod N)ˣ) : ℕ := + haveI := Classical.decPred (· ∈ Δ) + Nat.gcd N ((Finset.univ.filter (· ∈ Δ)).gcd fun d : (ZMod N)ˣ => (d : ZMod N).val ^ 2 - 1) + +/-- h_Δ = ∏_{p ∣ N} p^{min(v_p(ε_Δ), ⌊v_p(N)/2⌋)}. -/ +def hDelta (N : ℕ) [NeZero N] (Δ : Subgroup (ZMod N)ˣ) : ℕ := + ∏ p ∈ N.primeFactors, p ^ min ((epsDelta N Δ).factorization p) (N.factorization p / 2) + +/-- The image in SL₂(ℝ) of an integer matrix. -/ +abbrev ofZ (γ : SL(2, ℤ)) : SL(2, ℝ) := SpecialLinearGroup.map (Int.castRingHom ℝ) γ + + +end + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanCond.lean b/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanCond.lean new file mode 100644 index 000000000..08bd1cd9a --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanCond.lean @@ -0,0 +1,180 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanRat + +/-! +# 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. +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +/-- ε = gcd(N, 24). -/ +def epsPart (N : ℕ) : ℕ := Nat.gcd N 24 + +/-- An integer matrix with N ∣ M₁₀ and ε ∣ M₁₁ − M₀₀. -/ +def InLe (N ε : ℕ) (M : Matrix (Fin 2) (Fin 2) ℝ) : Prop := + ∃ a b c d : ℤ, M = !![(a : ℝ), b; c, d] ∧ (N : ℤ) ∣ c ∧ (ε : ℤ) ∣ d - a + +theorem InLe.add {N ε : ℕ} {M M' : Matrix (Fin 2) (Fin 2) ℝ} (h : InLe N ε M) (h' : InLe N ε M') : + InLe N ε (M + M') := by + obtain ⟨a, b, c, d, rfl, hc, hd⟩ := h + obtain ⟨a', b', c', d', rfl, hc', hd'⟩ := h' + refine ⟨a + a', b + b', c + c', d + d', ?_, dvd_add hc hc', ?_⟩ + · ext i j; fin_cases i <;> fin_cases j <;> simp + · rw [show d + d' - (a + a') = (d - a) + (d' - a') by ring]; exact dvd_add hd hd' + +theorem InLe.zsmul {N ε : ℕ} {M : Matrix (Fin 2) (Fin 2) ℝ} (h : InLe N ε M) (m : ℤ) : + InLe N ε ((m : ℝ) • M) := by + obtain ⟨a, b, c, d, rfl, hc, hd⟩ := h + refine ⟨m * a, m * b, m * c, m * d, ?_, dvd_mul_of_dvd_right hc _, ?_⟩ + · ext i j; fin_cases i <;> fin_cases j <;> simp + · rw [show m * d - m * a = m * (d - a) by ring]; exact dvd_mul_of_dvd_right hd _ + +theorem InLe.sub {N ε : ℕ} {M M' : Matrix (Fin 2) (Fin 2) ℝ} (h : InLe N ε M) (h' : InLe N ε M') : + InLe N ε (M - M') := by + have := h.add (h'.zsmul (-1)) + convert this using 1 + simp [sub_eq_add_neg] + +theorem InLe.one {ε : ℕ} (N : ℕ) : InLe N ε 1 := + ⟨1, 0, 0, 1, by ext i j; fin_cases i <;> fin_cases j <;> simp, dvd_zero _, by simp⟩ + + +/-- The Γ₀(N) lattice, with parameter gcd(N, 24). -/ +def InL (N : ℕ) (M : Matrix (Fin 2) (Fin 2) ℝ) : Prop := InLe N (epsPart N) M + +theorem InL.add {N : ℕ} {M M' : Matrix (Fin 2) (Fin 2) ℝ} (h : InL N M) (h' : InL N M') : + InL N (M + M') := InLe.add h h' + +theorem InL.zsmul {N : ℕ} {M : Matrix (Fin 2) (Fin 2) ℝ} (h : InL N M) (m : ℤ) : + InL N ((m : ℝ) • M) := InLe.zsmul h m + +theorem InL.sub {N : ℕ} {M M' : Matrix (Fin 2) (Fin 2) ℝ} (h : InL N M) (h' : InL N M') : + InL N (M - M') := InLe.sub h h' + +theorem InL.one (N : ℕ) : InL N 1 := InLe.one N + +theorem epsPart_dvd_24 (N : ℕ) : epsPart N ∣ 24 := Nat.gcd_dvd_right _ _ + +theorem epsPart_dvd (N : ℕ) : epsPart N ∣ N := Nat.gcd_dvd_left _ _ + +theorem InL.of_mem {N : ℕ} {Y : SL(2, ℝ)} (hY : Y ∈ Gamma0R N) : + InL N (Y : Matrix (Fin 2) (Fin 2) ℝ) := by + obtain ⟨a, b, c, d, hdet, hc, hm⟩ := exists_entries_of_mem_Gamma0R hY + refine ⟨a, b, c, d, hm, hc, ?_⟩ + have hεc : (epsPart N : ℤ) ∣ c := dvd_trans (Int.natCast_dvd_natCast.2 (epsPart_dvd N)) hc + have had : a * d ≡ 1 [ZMOD epsPart N] := by + apply Int.ModEq.symm + rw [Int.modEq_iff_dvd, show a * d - 1 = b * c by linarith] + exact dvd_mul_of_dvd_right hεc _ + exact Int.ModEq.dvd (modEq_of_mul_modEq_one (epsPart_dvd_24 N) had) + +/-! ### Conjugation as a linear map -/ + +/-- S = [[α, β/h], [hγ, δ]]. -/ +def Smat (h : ℕ) (α β γ δ : ℤ) : Matrix (Fin 2) (Fin 2) ℝ := + !![(α : ℝ), (β : ℝ) / h; (h : ℝ) * γ, (δ : ℝ)] + +/-- Φ(M) = S M adj(S) / e. -/ +def Phi (h : ℕ) (α β γ δ : ℤ) (M : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ := + ((α * δ - β * γ : ℤ) : ℝ)⁻¹ • (Smat h α β γ δ * M * (Smat h α β γ δ).adjugate) + +theorem Phi_add (h : ℕ) (α β γ δ : ℤ) (M M' : Matrix (Fin 2) (Fin 2) ℝ) : + Phi h α β γ δ (M + M') = Phi h α β γ δ M + Phi h α β γ δ M' := by + simp [Phi, Matrix.mul_add, Matrix.add_mul, smul_add] + +theorem Phi_smul (h : ℕ) (α β γ δ : ℤ) (r : ℝ) (M : Matrix (Fin 2) (Fin 2) ℝ) : + Phi h α β γ δ (r • M) = r • Phi h α β γ δ M := by + simp [Phi, smul_smul, mul_comm] + +theorem Phi_sub (h : ℕ) (α β γ δ : ℤ) (M M' : Matrix (Fin 2) (Fin 2) ℝ) : + Phi h α β γ δ (M - M') = Phi h α β γ δ M - Phi h α β γ δ M' := by + have := Phi_add h α β γ δ M ((-1 : ℝ) • M') + rw [Phi_smul] at this + simpa [sub_eq_add_neg] using this + +theorem det_Smat {h : ℕ} (hh : h ≠ 0) (α β γ δ : ℤ) : + (Smat h α β γ δ).det = ((α * δ - β * γ : ℤ) : ℝ) := by + have hhr : (h : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hh + rw [Smat, det_fin_two_of] + push_cast + field_simp + +theorem Phi_one {h : ℕ} (hh : h ≠ 0) {α β γ δ : ℤ} (he : α * δ - β * γ ≠ 0) : + Phi h α β γ δ 1 = 1 := by + have her : ((α * δ - β * γ : ℤ) : ℝ) ≠ 0 := by exact_mod_cast he + rw [Phi, Matrix.mul_one, Matrix.mul_adjugate, det_Smat hh, smul_smul, inv_mul_cancel₀ her, + one_smul] + +/-- Conjugation by g = κ S is Φ. -/ +theorem coe_conj_eq_Phi {g : SL(2, ℝ)} {κ : ℝ} {h : ℕ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat h α β γ δ) (hh : h ≠ 0) (Y : SL(2, ℝ)) : + ((g * Y * g⁻¹ : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) = + Phi h α β γ δ (Y : Matrix (Fin 2) (Fin 2) ℝ) := by + have hdet : κ ^ 2 * ((α * δ - β * γ : ℤ) : ℝ) = 1 := by + have := g.2 + rw [hg, det_smul, Fintype.card_fin, Smat, det_fin_two_of] at this + have hhr : (h : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hh + push_cast + field_simp at this + linear_combination this + have hE : ((α * δ - β * γ : ℤ) : ℝ) ≠ 0 := by + intro h0; rw [h0, mul_zero] at hdet; exact zero_ne_one hdet + have hinv : κ ^ 2 = ((α * δ - β * γ : ℤ) : ℝ)⁻¹ := by + field_simp + linear_combination hdet + rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.SpecialLinearGroup.coe_mul, + Matrix.SpecialLinearGroup.coe_inv, hg, adjugate_smul, Fintype.card_fin] + simp only [Matrix.smul_mul, Matrix.mul_smul, smul_smul, Phi] + congr 1 + +/-- The explicit images of E₁₂, E₂₁, E₂₂ under M ↦ S M adj(S). -/ +theorem Phi_E12 (h : ℕ) (α β γ δ : ℤ) : + Phi h α β γ δ !![0, 1; 0, 0] = ((α * δ - β * γ : ℤ) : ℝ)⁻¹ • + !![-(α * h * γ : ℝ), (α : ℝ) ^ 2; -((h : ℝ) ^ 2 * γ ^ 2), α * h * γ] := by + unfold Phi Smat + rw [adjugate_fin_two_of, mul_fin_two, mul_fin_two] + congr 1 + ext i j + fin_cases i <;> fin_cases j <;> simp <;> ring + +theorem Phi_E21 {h : ℕ} (hh : h ≠ 0) (α β γ δ : ℤ) : + Phi h α β γ δ !![0, 0; 1, 0] = ((α * δ - β * γ : ℤ) : ℝ)⁻¹ • + !![(β : ℝ) * δ / h, -((β : ℝ) ^ 2 / (h : ℝ) ^ 2); (δ : ℝ) ^ 2, -((β : ℝ) * δ / h)] := by + have hhr : (h : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hh + unfold Phi Smat + rw [adjugate_fin_two_of, mul_fin_two, mul_fin_two] + congr 1 + ext i j + fin_cases i <;> fin_cases j <;> simp <;> field_simp + +theorem Phi_E22 {h : ℕ} (hh : h ≠ 0) (α β γ δ : ℤ) : + Phi h α β γ δ !![0, 0; 0, 1] = ((α * δ - β * γ : ℤ) : ℝ)⁻¹ • + !![-((β : ℝ) * γ), (α : ℝ) * β / h; -((h : ℝ) * γ * δ), (α : ℝ) * δ] := by + have hhr : (h : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hh + unfold Phi Smat + rw [adjugate_fin_two_of, mul_fin_two, mul_fin_two] + congr 1 + ext i j + fin_cases i <;> fin_cases j <;> simp <;> field_simp + +end + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanFacts.lean b/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanFacts.lean new file mode 100644 index 000000000..fd29f393a --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanFacts.lean @@ -0,0 +1,126 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerDelta.NewmanGen + +/-! +# Newman's theorem, step 2 continued: the integer divisibilities + +For g = κ·S ∈ Norm(Γ₀(N)), S = [[α, β/h], [hγ, δ]], e = αδ − βγ, with h = h(N), n = n(N), +ε = gcd(N, 24): + +* F1 e ∣ h·αγ F2 e ∣ α² F3 eN ∣ h²γ² F4 eε ∣ 2h·αγ +* F5 e ∣ nh·βδ F6 e ∣ n·β² F7 e ∣ δ² F8 eε ∣ 2nh·βδ +* F9 e ∣ N·βγ F10 eh ∣ N·αβ F11 eN ∣ Nh·γδ F12 eε ∣ 2N·βγ +* and, for [[x, y], [N, t]] ∈ Γ₀(N) and s = t − x, the same four with s in place of N. +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +/-- The generic Newman hypotheses for Γ₀(N). -/ +theorem newmanData_gamma0 (N : ℕ) : + NewmanData N (Gamma0R N) (epsPart N) (hPart N) where + le := le_refl _ + T_mem := matT_mem N + U_mem := matU_mem N + inL := fun _ h => InL.of_mem h + eps_dvd := epsPart_dvd N + h_pos := hPart_pos N + h_sq_dvd := by + by_cases hN : N = 0 + · simp [hN] + · exact hPart_sq_dvd hN + h_fact := by + intro p + by_cases hN : N = 0 + · simp [hN, hPart] + · exact (local_constants hN).2 + gamma := by + intro p hp hpN hlt + have hN : N ≠ 0 := by + intro hN + simp [hN] at hlt + obtain ⟨x, y, t, hdet, hs⟩ := exists_gamma_p hN hp hpN + have hs' : t - x ≠ 0 ∧ vz p (t - x) = (epsPart N).factorization p := by + rcases hs with heq | hs + · omega + · exact hs + let γp : SL(2, ℝ) := ⟨!![(x : ℝ), y; N, t], by + rw [det_fin_two_of] + exact_mod_cast hdet⟩ + exact ⟨x, y, t, hdet, + ⟨γp, mem_Gamma0R_of_entries x y N t rfl (dvd_refl _), rfl⟩, hs'⟩ + +theorem InL.entries {N : ℕ} {M : Matrix (Fin 2) (Fin 2) ℝ} (h : InL N M) : + ∃ a b c d : ℤ, M 0 0 = a ∧ M 0 1 = b ∧ M 1 0 = c ∧ M 1 1 = d ∧ (N : ℤ) ∣ c ∧ + (epsPart N : ℤ) ∣ d - a := by + exact InLe.entries h + +theorem phi_InL {N : ℕ} {g : SL(2, ℝ)} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (hPart N) α β γ δ) {Y : SL(2, ℝ)} + (hY : Y ∈ Gamma0R N) : InL N (Phi (hPart N) α β γ δ (Y : Matrix (Fin 2) (Fin 2) ℝ)) := by + exact phi_InLe (newmanData_gamma0 N) hgN hg hY + +theorem InL.nsmul' {N : ℕ} {M : Matrix (Fin 2) (Fin 2) ℝ} (h : InL N M) (m : ℕ) : + InL N ((m : ℝ) • M) := by + exact InLe.nsmul' h m + +theorem InL_basic {N : ℕ} {g : SL(2, ℝ)} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (hPart N) α β γ δ) + (he : α * δ - β * γ ≠ 0) : + InL N (Phi (hPart N) α β γ δ !![0, 1; 0, 0]) ∧ + InL N ((N : ℝ) • Phi (hPart N) α β γ δ !![0, 0; 1, 0]) ∧ + InL N ((N : ℝ) • Phi (hPart N) α β γ δ !![0, 0; 0, 1]) := by + exact InLe_basic (newmanData_gamma0 N) hgN hg he + +theorem InL_s {N : ℕ} {g : SL(2, ℝ)} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (hPart N) α β γ δ) + (he : α * δ - β * γ ≠ 0) {x y t : ℤ} (hdet : x * t - y * N = 1) : + InL N (((t - x : ℤ) : ℝ) • Phi (hPart N) α β γ δ !![0, 0; 0, 1]) ∧ + (epsPart N : ℤ) ∣ t - x := by + let γp : SL(2, ℝ) := ⟨!![(x : ℝ), y; N, t], by + rw [det_fin_two_of] + exact_mod_cast hdet⟩ + have hγp : γp ∈ Gamma0R N := mem_Gamma0R_of_entries x y N t rfl (dvd_refl _) + exact InLe_s (newmanData_gamma0 N) hgN hg he hγp rfl + +theorem int_facts {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (hPart N) α β γ δ) + (he : α * δ - β * γ ≠ 0) : + (α * δ - β * γ) ∣ (hPart N : ℤ) * (α * γ) ∧ (α * δ - β * γ) ∣ 1 * α ^ 2 ∧ (α * δ - β * γ) * N + ∣ (hPart N : ℤ) ^ 2 * γ ^ 2 ∧ (α * δ - β * γ) * (epsPart N : ℤ) ∣ (2 * (hPart N : ℤ)) * (α * + γ) ∧ + (α * δ - β * γ) ∣ ((nPart N : ℤ) * (hPart N : ℤ)) * (β * δ) ∧ (α * δ - β * γ) ∣ (nPart N : ℤ) + * β ^ 2 ∧ (α * δ - β * γ) ∣ 1 * δ ^ 2 ∧ (α * δ - β * γ) * (epsPart N : ℤ) ∣ (2 * (nPart N : + ℤ) * (hPart N : ℤ)) * (β * δ) ∧ + (α * δ - β * γ) ∣ (N : ℤ) * (β * γ) ∧ (α * δ - β * γ) * (hPart N : ℤ) ∣ (N : ℤ) * (α * β) ∧ (α + * δ - β * γ) * N ∣ ((N : ℤ) * (hPart N : ℤ)) * (γ * δ) ∧ + (α * δ - β * γ) * (epsPart N : ℤ) ∣ (2 * (N : ℤ)) * (β * γ) := by + exact int_factsG (newmanData_gamma0 N) hgN hg he + +theorem int_facts_s {N : ℕ} {g : SL(2, ℝ)} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} + (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (hPart N) α β γ δ) + (he : α * δ - β * γ ≠ 0) {x y t : ℤ} (hdet : x * t - y * N = 1) : + (α * δ - β * γ) ∣ (t - x) * (β * γ) ∧ + (α * δ - β * γ) * (hPart N : ℤ) ∣ (t - x) * (α * β) ∧ + (α * δ - β * γ) * N ∣ ((t - x) * (hPart N : ℤ)) * (γ * δ) ∧ + (α * δ - β * γ) * (epsPart N : ℤ) ∣ (2 * (t - x)) * (β * γ) := by + let γp : SL(2, ℝ) := ⟨!![(x : ℝ), y; N, t], by + rw [det_fin_two_of] + exact_mod_cast hdet⟩ + have hγp : γp ∈ Gamma0R N := mem_Gamma0R_of_entries x y N t rfl (dvd_refl _) + exact int_facts_sG (newmanData_gamma0 N) hgN hg he hγp rfl + +end + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanMain.lean b/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanMain.lean new file mode 100644 index 000000000..7c26583f6 --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanMain.lean @@ -0,0 +1,44 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanFacts + +/-! +# Newman's theorem for Γ₀(N) + +The primitive representative and local valuation argument is proved for arbitrary subgroups in +`NormalizerDelta/NewmanGen`. Here it is instantiated with `newmanData_gamma0`, which supplies +Γ₀(N)'s lattice, unipotents and valuation witnesses. The specialized local and final theorems +are wrappers around that shared argument, with no inverse-representative hypothesis needed. +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +theorem local_conclusion {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (hgN : g ∈ Norm0 N) {κ : ℝ} + {α β γ δ : ℤ} (hg : (g : Matrix (Fin 2) (Fin 2) ℝ) = κ • Smat (hPart N) α β γ δ) + (he : α * δ - β * γ ≠ 0) + (hprim : ∀ p : ℕ, p.Prime → ¬ ((p : ℤ) ∣ α ∧ (p : ℤ) ∣ β ∧ (p : ℤ) ∣ γ ∧ (p : ℤ) ∣ δ)) + {p : ℕ} (hp : p.Prime) : + let B := vz p (α * δ - β * γ) + N.factorization p + 1 + (vz p (α * δ - β * γ) = 0 ∧ (nPart N).factorization p ≤ vv B p γ) ∨ + (vz p (α * δ - β * γ) = (nPart N).factorization p ∧ + (nPart N).factorization p ≤ vv B p α ∧ (nPart N).factorization p ≤ vv B p γ ∧ + (nPart N).factorization p ≤ vv B p δ) := by + exact local_conclusionG (newmanData_gamma0 N) hgN hg he hprim hp + +theorem newman' {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (hg : g ∈ Norm0 N) : IsNewmanForm N g := by + exact newmanG (newmanData_gamma0 N) hg + +end + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanRat.lean b/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanRat.lean new file mode 100644 index 000000000..0833f8e62 --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanRat.lean @@ -0,0 +1,297 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerLean.T1General + +/-! +# 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). +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +/-- `r` is an integer. -/ +def IsIntR (r : ℝ) : Prop := ∃ m : ℤ, r = m + +theorem IsIntR.add {r s : ℝ} (hr : IsIntR r) (hs : IsIntR s) : IsIntR (r + s) := by + obtain ⟨m, rfl⟩ := hr; obtain ⟨n, rfl⟩ := hs; exact ⟨m + n, by push_cast; ring⟩ +theorem IsIntR.sub {r s : ℝ} (hr : IsIntR r) (hs : IsIntR s) : IsIntR (r - s) := by + obtain ⟨m, rfl⟩ := hr; obtain ⟨n, rfl⟩ := hs; exact ⟨m - n, by push_cast; ring⟩ +theorem IsIntR.mul {r s : ℝ} (hr : IsIntR r) (hs : IsIntR s) : IsIntR (r * s) := by + obtain ⟨m, rfl⟩ := hr; obtain ⟨n, rfl⟩ := hs; exact ⟨m * n, by push_cast; ring⟩ +theorem IsIntR.neg {r : ℝ} (hr : IsIntR r) : IsIntR (-r) := by + obtain ⟨m, rfl⟩ := hr; exact ⟨-m, by push_cast; ring⟩ +theorem IsIntR.int (m : ℤ) : IsIntR m := ⟨m, rfl⟩ +theorem IsIntR.nat (m : ℕ) : IsIntR m := ⟨m, by simp⟩ +theorem IsIntR.one : IsIntR 1 := ⟨1, by simp⟩ + +theorem isIntR_entries_of_mem {N : ℕ} {γ : SL(2, ℝ)} (hγ : γ ∈ Gamma0R N) (i j : Fin 2) : + IsIntR ((γ : Matrix (Fin 2) (Fin 2) ℝ) i j) := by + obtain ⟨a, b, c, d, -, -, hm⟩ := exists_entries_of_mem_Gamma0R hγ + rw [hm] + fin_cases i <;> fin_cases j <;> simp [IsIntR.int] + +/-- The unit upper-unipotent matrix. -/ +def matT : SL(2, ℝ) := ⟨!![1, 1; 0, 1], by simp [det_fin_two_of]⟩ +/-- The lower-unipotent matrix with lower-left entry N. -/ +def matU (N : ℕ) : SL(2, ℝ) := ⟨!![1, 0; (N : ℝ), 1], by simp [det_fin_two_of]⟩ + +theorem matT_mem (N : ℕ) : matT ∈ Gamma0R N := + mem_Gamma0R_of_entries 1 1 0 1 (by simp [matT]) (dvd_zero _) + +theorem matU_mem (N : ℕ) : matU N ∈ Gamma0R N := + mem_Gamma0R_of_entries 1 0 N 1 (by simp [matU]) (dvd_refl _) + +theorem coe_conj (g Y : SL(2, ℝ)) : + ((g * Y * g⁻¹ : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) = + (g : Matrix (Fin 2) (Fin 2) ℝ) * (Y : Matrix (Fin 2) (Fin 2) ℝ) * + (g : Matrix (Fin 2) (Fin 2) ℝ).adjugate := by + rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.SpecialLinearGroup.coe_mul, + Matrix.SpecialLinearGroup.coe_inv] + +/-- The products of entries that are integers. -/ +theorem integral_products_of_normalizer {N : ℕ} {Γ : Subgroup SL(2, ℝ)} + (subgroup_le : Γ ≤ Gamma0R N) (translation_mem : matT ∈ Γ) + (lower_translation_mem : matU N ∈ Γ) {g : SL(2, ℝ)} + (hg : g ∈ NormG Γ) {x y z w : ℝ} + (hx : (g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = x) (hy : (g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = y) + (hz : (g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = z) (hw : (g : Matrix (Fin 2) (Fin 2) ℝ) 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)) := by + have hconj : ∀ Y ∈ Γ, g * Y * g⁻¹ ∈ Γ := fun Y hY => + (Subgroup.mem_normalizer_iff.1 hg Y).1 hY + have hT := isIntR_entries_of_mem (subgroup_le (hconj _ translation_mem)) + have hU := isIntR_entries_of_mem (subgroup_le (hconj _ lower_translation_mem)) + have hTU := isIntR_entries_of_mem + (subgroup_le (hconj _ (mul_mem translation_mem lower_translation_mem))) + have hdet : x * w - y * z = 1 := by + have := g.2 + rw [det_fin_two, hx, hy, hz, hw] at this + exact this + -- explicit conjugates + have eT : ∀ i j, ((g * matT * g⁻¹ : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) i j = + !![1 - x * z, x * x; -(z * z), 1 + x * z] i j := by + intro i j + rw [coe_conj, adjugate_fin_two] + fin_cases i <;> fin_cases j <;> + simp only [matT, Fin.isValue, hw, hy, hz, hx, Fin.zero_eta, Matrix.mul_apply, of_apply, + cons_val', cons_val_fin_one, Fin.sum_univ_two, cons_val_zero, cons_val_one, mul_one, + mul_zero, add_zero, mul_neg, Fin.mk_one] <;> + first | ring1 | (linear_combination hdet) + have eU : ∀ i j, ((g * matU N * g⁻¹ : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) i j = + !![1 + N * (y * w), -(N * (y * y)); N * (w * w), 1 - N * (y * w)] i j := by + intro i j + rw [coe_conj, adjugate_fin_two] + fin_cases i <;> fin_cases j <;> + simp only [matU, Fin.isValue, hw, hy, hz, hx, Fin.zero_eta, Matrix.mul_apply, of_apply, + cons_val', cons_val_fin_one, Fin.sum_univ_two, cons_val_zero, cons_val_one, mul_one, + mul_zero, zero_add, mul_neg, Fin.mk_one] <;> + first | ring1 | (linear_combination hdet) + have eTU : ∀ i j, ((g * (matT * matU N) * g⁻¹ : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) i j = + !![1 - x * z + N * (y * w) + N * (x * w), x * x - N * (y * y) - N * (x * y); + -(z * z) + N * (w * w) + N * (z * w), 1 + x * z - N * (y * w) - N * (y * z)] i j := by + intro i j + rw [coe_conj, Matrix.SpecialLinearGroup.coe_mul, adjugate_fin_two] + fin_cases i <;> fin_cases j <;> + simp only [matT, matU, cons_mul, Nat.succ_eq_add_one, Nat.reduceAdd, vecMul_cons, head_cons, + one_smul, tail_cons, empty_vecMul, add_zero, add_cons, zero_add, empty_add_empty, + zero_smul, empty_mul, Equiv.symm_apply_apply, Fin.isValue, hw, hy, hz, hx, Fin.zero_eta, + Matrix.mul_apply, of_apply, cons_val', cons_val_fin_one, Fin.sum_univ_two, cons_val_zero, + cons_val_one, mul_one, mul_neg, Fin.mk_one] <;> + first | ring1 | (linear_combination hdet) + have t01 := hT 0 1; rw [eT] at t01; simp only [Fin.isValue, of_apply, cons_val', cons_val_one, + cons_val_fin_one, cons_val_zero] at t01 + have t00 := hT 0 0; rw [eT] at t00; simp only [Fin.isValue, of_apply, cons_val', cons_val_zero, + cons_val_fin_one] at t00 + have t10 := hT 1 0; rw [eT] at t10; simp only [Fin.isValue, of_apply, cons_val', cons_val_zero, + cons_val_fin_one, cons_val_one] at t10 + have u01 := hU 0 1; rw [eU] at u01; simp only [Fin.isValue, of_apply, cons_val', cons_val_one, + cons_val_fin_one, cons_val_zero] at u01 + have u10 := hU 1 0; rw [eU] at u10; simp only [Fin.isValue, of_apply, cons_val', cons_val_zero, + cons_val_fin_one, cons_val_one] at u10 + have u00 := hU 0 0; rw [eU] at u00; simp only [Fin.isValue, of_apply, cons_val', cons_val_zero, + cons_val_fin_one] at u00 + have v00 := hTU 0 0; rw [eTU] at v00; simp only [Fin.isValue, of_apply, cons_val', + cons_val_zero, cons_val_fin_one] at v00 + have v01 := hTU 0 1; rw [eTU] at v01; simp only [Fin.isValue, of_apply, cons_val', cons_val_one, + cons_val_fin_one, cons_val_zero] at v01 + have v10 := hTU 1 0; rw [eTU] at v10; simp only [Fin.isValue, of_apply, cons_val', + cons_val_zero, cons_val_fin_one, cons_val_one] at v10 + have v11 := hTU 1 1; rw [eTU] at v11; simp only [Fin.isValue, of_apply, cons_val', cons_val_one, + cons_val_fin_one] at v11 + have hxz : IsIntR (x * z) := by + have := (IsIntR.one.sub t00) + simpa using this + have hzz : IsIntR (z * z) := by simpa using t10.neg + have hyy : IsIntR (N * (y * y)) := by simpa using u01.neg + have hyw : IsIntR (N * (y * w)) := by + have := u00.sub IsIntR.one + simpa using this + refine ⟨t01, hxz, hzz, hyy, u10, hyw, ?_, ?_, ?_, ?_⟩ + · have := ((v00.sub IsIntR.one).add hxz).sub hyw + convert this using 1; ring + · have := ((t01.sub hyy).sub v01) + convert this using 1; ring + · have := ((v10.add hzz).sub u10) + convert this using 1; ring + · have := (((IsIntR.one.add hxz).sub hyw).sub v11) + convert this using 1; ring + +/-- Integral entry products for the full congruence subgroup. -/ +theorem products_int {N : ℕ} {g : SL(2, ℝ)} (hg : g ∈ Norm0 N) {x y z w : ℝ} + (hx : (g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = x) (hy : (g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = y) + (hz : (g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = z) (hw : (g : Matrix (Fin 2) (Fin 2) ℝ) 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)) := by + exact integral_products_of_normalizer le_rfl (matT_mem N) (matU_mem N) hg hx hy hz hw + +/-- **Step 1** ([Nw §2]): g = κ·[[α, β/h], [hγ, δ]] with α, β, γ, δ ∈ ℤ without a common prime +factor. -/ +theorem primitive_form_of_normalizer {N : ℕ} [NeZero N] {Γ : Subgroup SL(2, ℝ)} + (subgroup_le : Γ ≤ Gamma0R N) (translation_mem : matT ∈ Γ) + (lower_translation_mem : matU N ∈ Γ) (scale : ℕ) (scale_pos : 0 < scale) + {g : SL(2, ℝ)} (hg : g ∈ NormG Γ) : + ∃ (κ : ℝ) (α β γ δ : ℤ), κ ≠ 0 ∧ + (∀ p : ℕ, p.Prime → ¬ ((p : ℤ) ∣ α ∧ (p : ℤ) ∣ β ∧ (p : ℤ) ∣ γ ∧ (p : ℤ) ∣ δ)) ∧ + (g : Matrix (Fin 2) (Fin 2) ℝ) = + κ • !![(α : ℝ), (β : ℝ) / scale; (scale : ℝ) * γ, (δ : ℝ)] := by + set x := (g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 with hx + set y := (g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 with hy + set z := (g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 with hz + set w := (g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 with hw + obtain ⟨hxx, hxz, hzz, hyy, hww, hyw, hxw, hxy, hzw, hyz⟩ := + integral_products_of_normalizer subgroup_le translation_mem lower_translation_mem hg + hx.symm hy.symm hz.symm hw.symm + have hdet : x * w - y * z = 1 := by + have := g.2 + rwa [det_fin_two] at this + have hN : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.2 (NeZero.ne N) + have hh : (scale : ℝ) ≠ 0 := Nat.cast_ne_zero.2 scale_pos.ne' + -- a nonzero t with N t x, N t y, N t z, N t w integral + obtain ⟨t, ht, htx, hty, htz, htw⟩ : ∃ t : ℝ, t ≠ 0 ∧ IsIntR (N * t * x) ∧ IsIntR (N * t * y) ∧ + IsIntR (N * t * z) ∧ IsIntR (N * t * w) := by + by_cases hx0 : x = 0 + · have hz0 : z ≠ 0 := by + intro hz0 + rw [hx0, hz0] at hdet + simp at hdet + refine ⟨z, hz0, ?_, ?_, ?_, ?_⟩ + · convert (IsIntR.nat N).mul hxz using 1; ring + · convert hyz using 1; ring + · convert (IsIntR.nat N).mul hzz using 1; ring + · convert hzw using 1; ring + · refine ⟨x, hx0, ?_, ?_, ?_, ?_⟩ + · convert (IsIntR.nat N).mul hxx using 1; ring + · convert hxy using 1; ring + · convert (IsIntR.nat N).mul hxz using 1; ring + · convert hxw using 1; ring + obtain ⟨Ix, hIx⟩ := htx + obtain ⟨Iy, hIy⟩ := hty + obtain ⟨Iz, hIz⟩ := htz + obtain ⟨Iw, hIw⟩ := htw + set h := scale + set M0 : ℤ := h * Ix + set M1 : ℤ := h ^ 2 * Iy + set M2 : ℤ := Iz + set M3 : ℤ := h * Iw + set G : ℕ := Int.gcd (Int.gcd M0 M1) (Int.gcd M2 M3) with hG + have hNt : (N : ℝ) * t ≠ 0 := mul_ne_zero hN ht + have hG0 : G ≠ 0 := by + intro hG0 + simp only [hG, Int.gcd_eq_zero_iff, Nat.cast_eq_zero] at hG0 + obtain ⟨⟨h0, h1⟩, h2, h3⟩ := hG0 + have hx0 : x = 0 := by + have : (N : ℝ) * t * x = 0 := by + rw [hIx] + have : Ix = 0 := by + simp only [M0] at h0 + rcases mul_eq_zero.1 h0 with h' | h' + · exact absurd (by exact_mod_cast h') scale_pos.ne' + · exact h' + simp [this] + exact (mul_eq_zero.1 this).resolve_left hNt + have hy0 : y = 0 := by + have : (N : ℝ) * t * y = 0 := by + rw [hIy] + have : Iy = 0 := by + simp only [M1] at h1 + rcases mul_eq_zero.1 h1 with h' | h' + · have h'' : (h : ℤ) = 0 := (pow_eq_zero_iff two_ne_zero).1 h' + exact absurd (by exact_mod_cast h'' : h = 0) scale_pos.ne' + · exact h' + simp [this] + exact (mul_eq_zero.1 this).resolve_left hNt + rw [hx0, hy0] at hdet + simp at hdet + have hGdvd : ∀ m : ℤ, m = M0 ∨ m = M1 ∨ m = M2 ∨ m = M3 → (G : ℤ) ∣ m := by + rintro m (rfl | rfl | rfl | rfl) + · exact (Int.gcd_dvd_left _ _).trans (Int.gcd_dvd_left _ _) + · exact (Int.gcd_dvd_left _ _).trans (Int.gcd_dvd_right _ _) + · exact (Int.gcd_dvd_right _ _).trans (Int.gcd_dvd_left _ _) + · exact (Int.gcd_dvd_right _ _).trans (Int.gcd_dvd_right _ _) + obtain ⟨α, hα⟩ := hGdvd M0 (Or.inl rfl) + obtain ⟨β, hβ⟩ := hGdvd M1 (Or.inr (Or.inl rfl)) + obtain ⟨γ, hγ⟩ := hGdvd M2 (Or.inr (Or.inr (Or.inl rfl))) + obtain ⟨δ, hδ⟩ := hGdvd M3 (Or.inr (Or.inr (Or.inr rfl))) + refine ⟨G / ((h : ℝ) * N * t), α, β, γ, δ, ?_, ?_, ?_⟩ + · exact div_ne_zero (Nat.cast_ne_zero.2 hG0) (mul_ne_zero (mul_ne_zero hh hN) ht) + · rintro p hp ⟨hpα, hpβ, hpγ, hpδ⟩ + obtain ⟨α', hα'⟩ := hpα + obtain ⟨β', hβ'⟩ := hpβ + obtain ⟨γ', hγ'⟩ := hpγ + obtain ⟨δ', hδ'⟩ := hpδ + have hpG : ((p * G : ℕ) : ℤ) ∣ (G : ℤ) := by + have h0 : ((p * G : ℕ) : ℤ) ∣ M0 := ⟨α', by rw [hα, hα']; push_cast; ring⟩ + have h1 : ((p * G : ℕ) : ℤ) ∣ M1 := ⟨β', by rw [hβ, hβ']; push_cast; ring⟩ + have h2 : ((p * G : ℕ) : ℤ) ∣ M2 := ⟨γ', by rw [hγ, hγ']; push_cast; ring⟩ + have h3 : ((p * G : ℕ) : ℤ) ∣ M3 := ⟨δ', by rw [hδ, hδ']; push_cast; ring⟩ + rw [hG] + exact Int.dvd_coe_gcd (Int.dvd_coe_gcd h0 h1) (Int.dvd_coe_gcd h2 h3) + have : p * G ∣ G := by exact_mod_cast hpG + have := Nat.le_of_dvd (Nat.pos_of_ne_zero hG0) this + have := hp.two_le + nlinarith [Nat.pos_of_ne_zero hG0] + · have hGr : (G : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hG0 + have eα : (G : ℝ) * α = h * (N * t * x) := by rw [hIx]; exact_mod_cast hα.symm + have eβ : (G : ℝ) * β = h ^ 2 * (N * t * y) := by rw [hIy]; exact_mod_cast hβ.symm + have eγ : (G : ℝ) * γ = N * t * z := by rw [hIz]; exact_mod_cast hγ.symm + have eδ : (G : ℝ) * δ = h * (N * t * w) := by rw [hIw]; exact_mod_cast hδ.symm + ext i j + fin_cases i <;> fin_cases j <;> simp [← hx, ← hy, ← hz, ← hw] + · field_simp + linear_combination -eα + · field_simp + linear_combination -eβ + · field_simp + linear_combination -eγ + · field_simp + linear_combination -eδ + +/-- Primitive rational representatives for the full congruence subgroup. -/ +theorem exists_prim_form {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (hg : g ∈ Norm0 N) : + ∃ (κ : ℝ) (α β γ δ : ℤ), κ ≠ 0 ∧ + (∀ p : ℕ, p.Prime → ¬ ((p : ℤ) ∣ α ∧ (p : ℤ) ∣ β ∧ (p : ℤ) ∣ γ ∧ (p : ℤ) ∣ δ)) ∧ + (g : Matrix (Fin 2) (Fin 2) ℝ) = + κ • !![(α : ℝ), (β : ℝ) / hPart N; (hPart N : ℝ) * γ, (δ : ℝ)] := by + exact primitive_form_of_normalizer le_rfl (matT_mem N) (matU_mem N) + (hPart N) (hPart_pos N) hg + +end + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanVal.lean b/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanVal.lean new file mode 100644 index 000000000..41bfd5069 --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerLean/NewmanVal.lean @@ -0,0 +1,312 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanCond + +/-! +# Newman's theorem: valuations, the local constants, and the element γ_p of Lemma 3 + +* `vz p x` is the p-adic valuation of an integer (0 at 0); `vv B p x` is the same but equal to the + large value `B` at 0, so that zero entries can be handled by `omega` uniformly. +* the ultrametric relation for e = αδ − βγ in terms of `vv`; +* v_p(h), v_p(ε), v_p(n) in terms of ν = v_p(N); +* `exists_gamma_p`: for p ∣ N an element [[x, y], [N, t]] ∈ Γ₀(N) with min(v_p(t − x), ν) = v_p(ε) + (x ≡ 3 or 2 mod p^ν by the Chinese remainder theorem). +-/ + +@[expose] public section + +namespace CongruenceNormalizers + +/-- p-adic valuation of an integer (junk value 0 at 0). -/ +def vz (p : ℕ) (x : ℤ) : ℕ := x.natAbs.factorization p + +theorem vz_mul {p : ℕ} {x y : ℤ} (hx : x ≠ 0) (hy : y ≠ 0) : vz p (x * y) = vz p x + vz p y := by + simp [vz, Int.natAbs_mul, Nat.factorization_mul (Int.natAbs_ne_zero.2 hx) + (Int.natAbs_ne_zero.2 hy)] + +theorem vz_neg (p : ℕ) (x : ℤ) : vz p (-x) = vz p x := by simp [vz] + +theorem vz_natCast (p n : ℕ) : vz p n = n.factorization p := by simp [vz] + +theorem pow_dvd_iff_le_vz {p : ℕ} (hp : p.Prime) {x : ℤ} (hx : x ≠ 0) (m : ℕ) : + (p : ℤ) ^ m ∣ x ↔ m ≤ vz p x := by + rw [← Int.natAbs_dvd_natAbs, Int.natAbs_pow, Int.natAbs_natCast, + hp.pow_dvd_iff_le_factorization (Int.natAbs_ne_zero.2 hx)] + rfl + +theorem vz_le_of_dvd (p : ℕ) {x y : ℤ} (hy : y ≠ 0) (hxy : x ∣ y) : vz p x ≤ vz p y := by + have hx : x ≠ 0 := by rintro rfl; exact hy (zero_dvd_iff.1 hxy) + exact (Nat.factorization_le_iff_dvd (Int.natAbs_ne_zero.2 hx) (Int.natAbs_ne_zero.2 hy)).2 + (Int.natAbs_dvd_natAbs.2 hxy) p + +theorem vz_eq_zero_of_not_dvd {p : ℕ} {x : ℤ} (h : ¬ (p : ℤ) ∣ x) : vz p x = 0 := by + apply Nat.factorization_eq_zero_of_not_dvd + intro h' + exact h (Int.natCast_dvd.2 h') + +/-- Valuation with value `B` at 0. -/ +def vv (B p : ℕ) (x : ℤ) : ℕ := if x = 0 then B else vz p x + +theorem vv_of_ne {B p : ℕ} {x : ℤ} (hx : x ≠ 0) : vv B p x = vz p x := ite_eq_right hx + +theorem vv_neg (B p : ℕ) (x : ℤ) : vv B p (-x) = vv B p x := by + unfold vv + simp [vz_neg] + +/-- From `X ∣ K·x·y`: v(X) ≤ v(K) + v(x) + v(y). -/ +theorem le_vv2 {B p : ℕ} {X K x y : ℤ} (hK : K ≠ 0) (hB : vz p X ≤ B) (h : X ∣ K * (x * y)) : + vz p X ≤ vz p K + vv B p x + vv B p y := by + by_cases hx : x = 0 + · simp [vv, hx]; omega + by_cases hy : y = 0 + · simp [vv, hy]; omega + rw [vv_of_ne hx, vv_of_ne hy] + have := vz_le_of_dvd p (mul_ne_zero hK (mul_ne_zero hx hy)) h + rw [vz_mul hK (mul_ne_zero hx hy), vz_mul hx hy] at this + omega + +/-- From `X ∣ K·x²`: v(X) ≤ v(K) + 2v(x). -/ +theorem le_vv_sq {B p : ℕ} {X K x : ℤ} (hK : K ≠ 0) (hB : vz p X ≤ B) (h : X ∣ K * x ^ 2) : + vz p X ≤ vz p K + 2 * vv B p x := by + have := le_vv2 (x := x) (y := x) hK hB (by rwa [← pow_two]) + omega + +/-! ### The ultrametric inequality -/ + +theorem vz_sub_ge {p : ℕ} (hp : p.Prime) {A C : ℤ} (hAC : A - C ≠ 0) (hA : A ≠ 0) (hC : C ≠ 0) : + min (vz p A) (vz p C) ≤ vz p (A - C) := by + rw [← pow_dvd_iff_le_vz hp hAC] + exact dvd_sub ((pow_dvd_iff_le_vz hp hA _).2 (min_le_left _ _)) + ((pow_dvd_iff_le_vz hp hC _).2 (min_le_right _ _)) + +theorem vz_sub_eq {p : ℕ} (hp : p.Prime) {A C : ℤ} (hAC : A - C ≠ 0) (hA : A ≠ 0) (hC : C ≠ 0) + (hne : vz p A ≠ vz p C) : vz p (A - C) = min (vz p A) (vz p C) := by + apply le_antisymm _ (vz_sub_ge hp hAC hA hC) + by_contra hlt + push Not at hlt + have h1 := (pow_dvd_iff_le_vz hp hAC (min (vz p A) (vz p C) + 1)).2 hlt + rcases lt_or_gt_of_ne hne with h | h + · have h2 := (pow_dvd_iff_le_vz hp hC (vz p A + 1)).2 (by omega) + rw [min_eq_left h.le] at h1 + have h3 : (p : ℤ) ^ (vz p A + 1) ∣ A := by + have := dvd_add h1 h2 + simpa using this + have := (pow_dvd_iff_le_vz hp hA _).1 h3 + omega + · have h2 := (pow_dvd_iff_le_vz hp hA (vz p C + 1)).2 (by omega) + have h3 : (p : ℤ) ^ (vz p C + 1) ∣ C := by + rw [min_eq_right h.le] at h1 + have := dvd_sub h2 h1 + simpa using this + have := (pow_dvd_iff_le_vz hp hC _).1 h3 + omega + +/-- The ultrametric relation for e = αδ − βγ, in terms of `vv`. -/ +theorem ultra_vv {B p : ℕ} (hp : p.Prime) {α β γ δ : ℤ} (he : α * δ - β * γ ≠ 0) + (hB : vz p (α * δ - β * γ) < B) : + min (vv B p α + vv B p δ) (vv B p β + vv B p γ) ≤ vz p (α * δ - β * γ) ∧ + (vv B p α + vv B p δ ≠ vv B p β + vv B p γ → + vz p (α * δ - β * γ) = min (vv B p α + vv B p δ) (vv B p β + vv B p γ)) := by + by_cases had : α = 0 ∨ δ = 0 + · have hbg : β * γ ≠ 0 := by rcases had with rfl | rfl <;> simpa using he + have hβ : β ≠ 0 := left_ne_zero_of_mul hbg + have hγ : γ ≠ 0 := right_ne_zero_of_mul hbg + have hev : vz p (α * δ - β * γ) = vv B p β + vv B p γ := by + rcases had with rfl | rfl <;> + · simp only [zero_mul, mul_zero, zero_sub, vz_neg] + rw [vz_mul hβ hγ, vv_of_ne hβ, vv_of_ne hγ] + have hbig : B ≤ vv B p α + vv B p δ := by + rcases had with rfl | rfl <;> simp [vv] + constructor <;> [omega; (intro; omega)] + push Not at had + by_cases hbg' : β = 0 ∨ γ = 0 + · have hev : vz p (α * δ - β * γ) = vv B p α + vv B p δ := by + rcases hbg' with rfl | rfl <;> + · simp only [zero_mul, mul_zero, sub_zero] + rw [vz_mul had.1 had.2, vv_of_ne had.1, vv_of_ne had.2] + have hbig : B ≤ vv B p β + vv B p γ := by + rcases hbg' with rfl | rfl <;> simp [vv] + constructor <;> [omega; (intro; omega)] + push Not at hbg' + have hA : α * δ ≠ 0 := mul_ne_zero had.1 had.2 + have hC : β * γ ≠ 0 := mul_ne_zero hbg'.1 hbg'.2 + rw [vv_of_ne had.1, vv_of_ne had.2, vv_of_ne hbg'.1, vv_of_ne hbg'.2, ← vz_mul had.1 had.2, + ← vz_mul hbg'.1 hbg'.2] + exact ⟨vz_sub_ge hp he hA hC, vz_sub_eq hp he hA hC⟩ + +/-! ### The local constants -/ + +theorem factorization_24 (p : ℕ) : + (24 : ℕ).factorization p = if p = 2 then 3 else if p = 3 then 1 else 0 := by + rw [show (24 : ℕ) = 2 ^ 3 * 3 by norm_num, Nat.factorization_mul (by norm_num) (by norm_num), + Nat.prime_two.factorization_pow, Nat.prime_three.factorization] + simp only [Finsupp.add_apply, Finsupp.single_apply] + split_ifs <;> omega + +theorem factorization_two (p : ℕ) : (2 : ℕ).factorization p = if p = 2 then 1 else 0 := by + rw [Nat.prime_two.factorization, Finsupp.single_apply] + split_ifs <;> omega + +theorem factorization_hPart (N p : ℕ) : + (hPart N).factorization p = if p = 2 then min 3 (N.factorization 2 / 2) else + if p = 3 then min 1 (N.factorization 3 / 2) else 0 := by + unfold hPart + rw [Nat.factorization_mul (by positivity) (by positivity), Nat.prime_two.factorization_pow, + Nat.prime_three.factorization_pow] + simp only [Finsupp.add_apply, Finsupp.single_apply] + split_ifs <;> omega + +theorem factorization_epsPart {N : ℕ} (hN : N ≠ 0) (p : ℕ) : + (epsPart N).factorization p = min (N.factorization p) ((24 : ℕ).factorization p) := by + unfold epsPart + rw [Nat.factorization_gcd hN (by norm_num)] + rfl + +/-- The local data at p: ν = v_p(N), j = v_p(ε), k = v_p(h), e₂ = v_p(2). -/ +theorem local_constants {N p : ℕ} (hN : N ≠ 0) : + ((p = 2 ∧ (epsPart N).factorization p = min (N.factorization p) 3 ∧ + (2 : ℕ).factorization p = 1) ∨ + (p = 3 ∧ (epsPart N).factorization p = min (N.factorization p) 1 ∧ + (2 : ℕ).factorization p = 0) ∨ + ((epsPart N).factorization p = 0 ∧ (2 : ℕ).factorization p = 0)) ∧ + (hPart N).factorization p = min ((epsPart N).factorization p) (N.factorization p / 2) := by + rw [factorization_epsPart hN, factorization_24, factorization_two, factorization_hPart] + by_cases h2 : p = 2 + · subst h2; simp; omega + by_cases h3 : p = 3 + · subst h3; simp; omega + simp [h2, h3] + +theorem factorization_nPart {N p : ℕ} (hN : N ≠ 0) : + (nPart N).factorization p + 2 * (hPart N).factorization p = N.factorization p := by + have h := hPart_sq_mul_nPart N hN + have hn : nPart N ≠ 0 := by rintro h0; rw [h0, zero_mul] at h; exact hN h.symm + have := congrArg (fun m => m.factorization p) h + rw [Nat.factorization_mul hn (by have := hPart_pos N; positivity), Nat.factorization_pow] at this + simp only [Finsupp.add_apply, Finsupp.smul_apply, smul_eq_mul] at this + omega + +end CongruenceNormalizers + +namespace CongruenceNormalizers + +/-! ### The element γ_p of Lemma 3 -/ + +/-- If x t − y N = 1, p^ν ∣ N, x ≡ r (mod p^ν), p ∤ x, p^ρ ∥ 1 − r², then +either ν ≤ ρ, or t − x ≠ 0 with v_p(t − x) = ρ. -/ +theorem gamma_val {p ν ρ : ℕ} (hp : p.Prime) {N x y t r : ℤ} (hdet : x * t - y * N = 1) + (hN : (p : ℤ) ^ ν ∣ N) (hxr : (p : ℤ) ^ ν ∣ r - x) (hpx : IsCoprime (p : ℤ) x) + (hρ1 : (p : ℤ) ^ ρ ∣ 1 - r ^ 2) (hρ2 : ¬ (p : ℤ) ^ (ρ + 1) ∣ 1 - r ^ 2) : + ν ≤ ρ ∨ (ρ < ν ∧ t - x ≠ 0 ∧ vz p (t - x) = ρ) := by + rcases le_or_gt ν ρ with h | h + · exact Or.inl h + right + -- x (t − x) ≡ 1 − r² (mod p^ν) + have hcong : (p : ℤ) ^ ν ∣ x * (t - x) - (1 - r ^ 2) := by + have : x * (t - x) - (1 - r ^ 2) = y * N + (r - x) * (r + x) := by linear_combination hdet + rw [this] + exact dvd_add (dvd_mul_of_dvd_right hN _) (dvd_mul_of_dvd_left hxr _) + have hle : ∀ m ≤ ν, (p : ℤ) ^ m ∣ x * (t - x) ↔ (p : ℤ) ^ m ∣ 1 - r ^ 2 := by + intro m hm + have hm' : (p : ℤ) ^ m ∣ x * (t - x) - (1 - r ^ 2) := (pow_dvd_pow _ hm).trans hcong + constructor + · intro h1; have := dvd_sub h1 hm'; simpa using this + · intro h1; have := dvd_add hm' h1; simpa using this + have hcop : ∀ m, IsCoprime ((p : ℤ) ^ m) x := fun m => hpx.pow_left + have hnot : ¬ (p : ℤ) ^ (ρ + 1) ∣ t - x := by + intro h1 + exact hρ2 ((hle (ρ + 1) h).1 (dvd_mul_of_dvd_right h1 _)) + have hs : t - x ≠ 0 := by + intro h0 + rw [h0] at hnot + exact hnot (dvd_zero _) + have hyes : (p : ℤ) ^ ρ ∣ t - x := + (hcop ρ).dvd_of_dvd_mul_left ((hle ρ h.le).2 hρ1) + refine ⟨h, hs, le_antisymm ?_ ((pow_dvd_iff_le_vz hp hs ρ).1 hyes)⟩ + by_contra hc + exact hnot ((pow_dvd_iff_le_vz hp hs (ρ + 1)).2 (by omega)) + +/-- **Lemma 3, locally**: for p ∣ N there is [[x, y], [N, t]] ∈ Γ₀(N) with +min(v_p(t − x), v_p(N)) = v_p(ε). -/ +theorem exists_gamma_p {N p : ℕ} (hN : N ≠ 0) (hp : p.Prime) (hpN : p ∣ N) : + ∃ x y t : ℤ, x * t - y * N = 1 ∧ + (N.factorization p = (epsPart N).factorization p ∨ + (t - x ≠ 0 ∧ vz p (t - x) = (epsPart N).factorization p)) := by + set ν := N.factorization p with hν + set N' := N / p ^ ν + have hcopN' : Nat.Coprime (p ^ ν) N' := Nat.Coprime.pow_left _ (Nat.coprime_ordCompl hp hN) + have hNeq : p ^ ν * N' = N := Nat.ordProj_mul_ordCompl_eq_self N p + set r : ℕ := if p = 2 then 3 else 2 with hr + obtain ⟨x0, hx1, hx2⟩ := Nat.chineseRemainder hcopN' r 1 + have hrp : Nat.Coprime r p := by + by_cases h2 : p = 2 + · subst h2; simp only [↓reduceIte, Nat.coprime_two_right, r]; decide + · simp only [r, h2, ite_false] + exact (Nat.coprime_primes Nat.prime_two hp).2 (Ne.symm h2) + have hν0 : 0 < ν := hp.factorization_pos_of_dvd hN hpN + have hx0p : Nat.Coprime x0 p := by + have h1 : Nat.Coprime x0 (p ^ ν) := by + rw [Nat.Coprime, Nat.ModEq.gcd_eq hx1] + exact Nat.Coprime.pow_right _ hrp + exact Nat.Coprime.coprime_dvd_right (dvd_pow_self p hν0.ne') h1 + have hx0N : Nat.Coprime x0 N := by + have h1 : Nat.Coprime x0 (p ^ ν) := Nat.Coprime.pow_right _ hx0p + have h2 : Nat.Coprime x0 N' := by + rw [Nat.Coprime, Nat.ModEq.gcd_eq hx2] + simp + rw [← hNeq] + exact Nat.Coprime.mul_right h1 h2 + have hb := Int.gcd_eq_gcd_ab x0 N + rw [Int.gcd_natCast_natCast, hx0N] at hb + have hdet : (x0 : ℤ) * Int.gcdA x0 N - (-Int.gcdB x0 N) * N = 1 := by + push_cast at hb + linear_combination -hb + refine ⟨x0, -Int.gcdB x0 N, Int.gcdA x0 N, hdet, ?_⟩ + have hpν : (p : ℤ) ^ ν ∣ (N : ℤ) := by exact_mod_cast Nat.ordProj_dvd N p + have hxr : (p : ℤ) ^ ν ∣ (r : ℤ) - x0 := by + have := Nat.ModEq.dvd hx1 + push_cast at this + simpa using this + have hpx : IsCoprime (p : ℤ) (x0 : ℤ) := by + rw [Int.isCoprime_iff_gcd_eq_one, Int.gcd_natCast_natCast] + exact hx0p.symm + have hj := factorization_epsPart hN p + rw [factorization_24] at hj + by_cases h2 : p = 2 + · subst h2 + have hrv : (r : ℤ) = 3 := by simp [r] + rw [hrv] at hxr + rcases gamma_val (ρ := 3) Nat.prime_two hdet hpν hxr hpx (by norm_num) (by norm_num) with + h | h + · left; simp at hj; omega + · right; simp only [↓reduceIte] at hj; rw [hj, h.2.2]; exact ⟨h.2.1, by omega⟩ + by_cases h3 : p = 3 + · subst h3 + have hrv : (r : ℤ) = 2 := by simp [r] + rw [hrv] at hxr + rcases gamma_val (ρ := 1) Nat.prime_three hdet hpν hxr hpx (by norm_num) (by norm_num) with + h | h + · left; simp at hj; omega + · right; simp only [Nat.succ_ne_self, ↓reduceIte] at hj; rw [hj, h.2.2]; exact ⟨h.2.1, by omega⟩ + · have hrv : (r : ℤ) = 2 := by simp [r, h2] + rw [hrv] at hxr + have hp5 : ¬ (p : ℤ) ^ (0 + 1) ∣ 1 - 2 ^ 2 := by + intro hd + have : (p : ℤ) ∣ 3 := by + have := (dvd_neg).2 hd + simpa using this + have h' : p ∣ 3 := by exact_mod_cast this + rcases (Nat.dvd_prime Nat.prime_three).1 h' with h'' | h'' + · exact hp.one_lt.ne' h'' + · exact h3 h'' + rcases gamma_val (ρ := 0) hp hdet hpν hxr hpx (by simp) hp5 with h | h + · omega + · right; simp only [h2, ↓reduceIte, h3, zero_le, inf_of_le_right] at hj; rw [hj, h.2.2]; exact + ⟨h.2.1, rfl⟩ + +end CongruenceNormalizers diff --git a/LeanPool/CongruenceNormalizers/NormalizerLean/T1General.lean b/LeanPool/CongruenceNormalizers/NormalizerLean/T1General.lean new file mode 100644 index 000000000..1b47cda2b --- /dev/null +++ b/LeanPool/CongruenceNormalizers/NormalizerLean/T1General.lean @@ -0,0 +1,143 @@ +/- +Copyright (c) 2026 Filip Najman. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Filip Najman +-/ +module + +public import LeanPool.CongruenceNormalizers.NormalizerLean.AtkinLehner + +/-! +# T1 in general: matrices of Newman's form (8′) normalize Γ₀(N) ([Nw §1]) + +With N = e·m·h² (h = h(N), n = N/h² = e·m), g = (ε/√e)·G, G = [[ae, b/h], [Nc/h, de]], and +γ = [[x, y], [Nz, x + hf]] ∈ Γ₀(N) (t ≡ x mod h because units mod h ∣ 24 square to 1), +G γ adj(G) = e·M with M the explicit integer matrix below (checked in sympy first). +Also `conjGamma0n_le_normalizer`: D⁻¹Γ₀(n)D consists of (8′)-matrices with e = 1. +-/ + +@[expose] public section + +open Matrix MatrixGroups + +namespace CongruenceNormalizers + +noncomputable section + +theorem smul_mul_mul_smul_eq_of {s Q : ℝ} (hs : s * s * Q = 1) + {W γ A X : Matrix (Fin 2) (Fin 2) ℝ} (h : W * γ * A = Q • X) : + (s • W) * γ * (s • A) = X := by + rw [Matrix.smul_mul, Matrix.smul_mul, Matrix.mul_smul, smul_smul, h, smul_smul, hs, one_smul] + +theorem hPart_sq_mul_nPart (N : ℕ) (hN : N ≠ 0) : nPart N * hPart N ^ 2 = N := + Nat.div_mul_cancel (hPart_sq_dvd hN) + +theorem isNewmanForm_inv {N : ℕ} {g : SL(2, ℝ)} (hg : IsNewmanForm N g) : IsNewmanForm N g⁻¹ := by + obtain ⟨a, b, c, d, e, he0, he, hdet, ε, hε, hgm⟩ := hg + refine ⟨d, -b, -c, a, e, he0, he, by linear_combination hdet, ε, hε, ?_⟩ + rw [coe_inv_of_coe_eq_smul hgm] + congr 1 + ext i j + fin_cases i <;> fin_cases j <;> simp <;> ring + +theorem isNewmanForm_conj_mem {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (hg : IsNewmanForm N g) + {γ : SL(2, ℝ)} (hγ : γ ∈ Gamma0R N) : g * γ * g⁻¹ ∈ Gamma0R N := by + have hN0 := NeZero.ne N + obtain ⟨a, b, c, d, e, he0, ⟨m, hm⟩, hdet, ε, hε, hgm⟩ := hg + change nPart N = e * m at hm + obtain ⟨x, y, c', t, hγdet, ⟨z, rfl⟩, hγm⟩ := exists_entries_of_mem_Gamma0R hγ + have hNnh := hPart_sq_mul_nPart N hN0 + set h := hPart N with hh + have hh0 : h ≠ 0 := (hPart_pos N).ne' + -- t ≡ x (mod h) + have hxt : x * t ≡ 1 [ZMOD h] := by + apply Int.ModEq.symm + rw [Int.modEq_iff_dvd] + refine ⟨y * z * nPart N * h, ?_⟩ + have : (N : ℤ) = nPart N * h ^ 2 := by exact_mod_cast hNnh.symm + rw [this] at hγdet + linear_combination hγdet + obtain ⟨f, hf⟩ := Int.ModEq.dvd (modEq_of_mul_modEq_one (hPart_dvd_24 N) hxt) + have ht : t = x + h * f := by linarith + subst ht + have hNr : (N : ℝ) = e * m * h ^ 2 := by + rw [← hNnh, hm] + push_cast + ring + have her : (e : ℝ) ≠ 0 := Nat.cast_ne_zero.2 he0.ne' + have hhr : (h : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hh0 + have hε2 : ε / Real.sqrt e * (ε / Real.sqrt e) * e = 1 := by + have hs : Real.sqrt e * Real.sqrt e = e := Real.mul_self_sqrt (Nat.cast_nonneg _) + have hε1 : ε * ε = 1 := by rcases hε with rfl | rfl <;> norm_num + have hs0 : Real.sqrt e ≠ 0 := by + intro h0; rw [h0, zero_mul] at hs; exact her hs.symm + rw [div_mul_div_comm, hε1, hs, one_div_mul_cancel her] + refine mem_Gamma0R_of_entries + (-a * c * e * h * m * y + a * d * e * x - b * c * f * h * m - b * c * m * x + + b * d * e * h * m * z) + (a ^ 2 * e * y + a * b * f - b ^ 2 * m * z) + (N * (-c ^ 2 * m * y - c * d * f + d ^ 2 * e * z)) + (a * c * e * h * m * y + a * d * e * f * h + a * d * e * x - b * c * m * x - + b * d * e * h * m * z) ?_ (dvd_mul_right _ _) + rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.SpecialLinearGroup.coe_mul, hgm, hγm, + coe_inv_of_coe_eq_smul hgm] + apply smul_mul_mul_smul_eq_of hε2 + rw [mul_fin_two, mul_fin_two] + ext i j + fin_cases i <;> fin_cases j <;> simp [hNr] <;> field_simp <;> ring + +/-- **T1** in general. -/ +theorem newmanForm_mem_normalizer' {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (hg : IsNewmanForm N g) : + g ∈ Norm0 N := by + refine mem_Norm0_of (fun γ hγ => isNewmanForm_conj_mem hg hγ) (fun γ hγ => ?_) + have := isNewmanForm_conj_mem (isNewmanForm_inv hg) hγ + simpa using this + +/-! ### D⁻¹Γ₀(n)D -/ + +theorem coe_projSL (A : Matrix (Fin 2) (Fin 2) ℝ) (hA : 0 < A.det) : + ((projSL A : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) = (Real.sqrt A.det)⁻¹ • A := by + have : projSL A = ⟨(Real.sqrt A.det)⁻¹ • A, by + rw [det_smul, Fintype.card_fin, inv_pow, Real.sq_sqrt hA.le, inv_mul_cancel₀ hA.ne']⟩ := + dite_eq_left hA + rw [this] + +theorem coe_Dsl (N : ℕ) : + ((Dsl N : SL(2, ℝ)) : Matrix (Fin 2) (Fin 2) ℝ) = + (Real.sqrt (hPart N))⁻¹ • !![(hPart N : ℝ), 0; 0, 1] := by + have hpos : (0 : ℝ) < (!![(hPart N : ℝ), 0; 0, 1]).det := by + have : (0 : ℝ) < hPart N := Nat.cast_pos.2 (hPart_pos N) + simpa [det_fin_two_of] using this + rw [Dsl, coe_projSL _ hpos] + simp [det_fin_two_of] + +theorem conjGamma0n_isNewmanForm {N : ℕ} [NeZero N] {g : SL(2, ℝ)} (hg : g ∈ conjGamma0n N) : + IsNewmanForm N g := by + obtain ⟨γ, hγ, rfl⟩ := hg + obtain ⟨a, b, c', d, hdet, ⟨c, rfl⟩, hγm⟩ := exists_entries_of_mem_Gamma0R hγ + have hNnh := hPart_sq_mul_nPart N (NeZero.ne N) + have hh0 : (hPart N : ℝ) ≠ 0 := Nat.cast_ne_zero.2 (hPart_pos N).ne' + dsimp only [nPart] at hdet + refine ⟨a, b, c, d, 1, one_pos, one_dvd _, by linear_combination hdet, 1, Or.inl rfl, ?_⟩ + have hD := coe_Dsl N + have hDinv := coe_inv_of_coe_eq_smul hD + simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_ofClass, MulAut.conj_apply, inv_inv] + rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.SpecialLinearGroup.coe_mul, hDinv, hγm, hD] + have hs : Real.sqrt (hPart N) * Real.sqrt (hPart N) = hPart N := + Real.mul_self_sqrt (Nat.cast_nonneg _) + have hsq : (Real.sqrt (hPart N))⁻¹ * (Real.sqrt (hPart N))⁻¹ * (hPart N : ℝ) = 1 := by + rw [← mul_inv, hs, inv_mul_cancel₀ hh0] + have hNr : (N : ℝ) = nPart N * (hPart N) ^ 2 := by exact_mod_cast hNnh.symm + rw [smul_mul_mul_smul_eq_of hsq (X := !![(a : ℝ), b / hPart N; nPart N * c * hPart N, d])] + · ext i j + fin_cases i <;> fin_cases j <;> simp [hNr] ; field_simp + · rw [mul_fin_two, mul_fin_two] + ext i j + fin_cases i <;> fin_cases j <;> simp <;> field_simp + +theorem conjGamma0n_le_normalizer' (N : ℕ) [NeZero N] : conjGamma0n N ≤ Norm0 N := + fun _ hg => newmanForm_mem_normalizer' (conjGamma0n_isNewmanForm hg) + +end + +end CongruenceNormalizers diff --git a/LeanPool/projects/congruence-normalizers.yaml b/LeanPool/projects/congruence-normalizers.yaml new file mode 100644 index 000000000..a7a82ab11 --- /dev/null +++ b/LeanPool/projects/congruence-normalizers.yaml @@ -0,0 +1,61 @@ +slug: congruence-normalizers +title: Newman normalizer bounds for congruence subgroups +summary: >- + Characterizes the normalizer of Gamma0(N) in SL(2, R), for every positive + level N, by explicit integral matrices scaled by a square root. Extends the + necessary matrix form to GammaDelta(N) for every subgroup Delta of the units + modulo N. Preserves Atkin-Lehner elements, rational representatives, integral + matrix lattices, prime valuations and a generic normalizer argument. + The upstream finite presentations, group orders and modular-curve + automorphism classifications are outside this import's scope. +branch: modular forms and arithmetic groups +entry_module: LeanPool.CongruenceNormalizers +authors: +- Filip Najman +source: + title: The normalizer of Gamma0(N) in PSL(2, R) + authors: + - M. Akbas + - D. Singerman + doi: 10.1017/S001708950000940X + url: https://github.com/F-Najman/normalizer-lean/tree/ea4445c0d991a65d54fc77af0af559f2322e8660 + github_repo: F-Najman/normalizer-lean + commit: ea4445c0d991a65d54fc77af0af559f2322e8660 + public_release_date: '2026-10-12' + completed_snapshot_date: '2026-10-14' + completed_snapshot_url: https://github.com/F-Najman/normalizer-lean/commit/99e6fc82ca7a364776179d7c5452cf18593acf6f + provenance_url: https://github.com/F-Najman/normalizer-lean/blob/ea4445c0d991a65d54fc77af0af559f2322e8660/palomar/part1/formalization.yaml +license: Apache-2.0 +status: verified +provenance: AI +main_declarations: +- CongruenceNormalizers.newman_iff +- CongruenceNormalizers.newman_delta +main_results: +- declaration: CongruenceNormalizers.newman_iff + informal: >- + For N > 0, put h = 2^min(3, floor(v_2(N)/2)) times + 3^min(1, floor(v_3(N)/2)) and n = N/h^2. A real determinant-one matrix + normalizes Gamma0(N) exactly when it equals plus or minus 1/sqrt(e) + times [[a*e, b/h], [N*c/h, d*e]], for integers a, b, c, d and a positive + divisor e of n satisfying a*d*e^2 - b*c*n = e. +- declaration: CongruenceNormalizers.newman_delta + informal: >- + For N > 0 and Delta a subgroup of the units modulo N, let epsilon be + gcd(N, u^2 - 1 for representatives u in Delta), and let h be the product + over primes p dividing N of p^min(v_p(epsilon), floor(v_p(N)/2)). Every + determinant-one real matrix normalizing GammaDelta(N) has the same + integral Newman form with this h and n = N/h^2. This is a necessary + bound; no converse for GammaDelta(N) is asserted. +- declaration: CongruenceNormalizers.hPart_isGreatest' + informal: >- + At every positive level, h(N) is the greatest divisor of 24 whose square + divides N. +tags: +- modular-forms +- congruence-subgroups +- normalizers +- arithmetic-groups +msc: +- 11F06 +- 20H05