{"id":"palomar/PALOMAR-2026-10-20-000007","url":"https://github.com/F-Najman/normalizer-lean/tree/a077781321ca0d52ba3a972a42e081f30534c4d2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-20-000007-v1.json","repo":"https://github.com/F-Najman/normalizer-lean","tags":["math.NT","math.GR","msc:11F06","msc:20H05","msc:14G35","msc:14H37","msc:68V20","modular-forms","congruence-subgroups","group-theory"],"score":0,"title":"The normalizer of Γ_Δ(N) for every N and every Δ","trust":"high","domain":"math.NT","source":"palomar","authors":["Filip Najman"],"reviews":0,"subject":"math.NT","summary":"Formal statements and proofs, in Lean 4 with Mathlib, about the normalizer in SL₂(ℝ) of Γ_Δ(N) for every N ≥ 1 and every subgroup Δ ≤ (ℤ/N)ˣ, with or without −1. Let h* be the largest h with h² ∣ N, d² ≡ 1 (mod h) for every d ∈ Δ, and Δ ⊇ ker((ℤ/N)ˣ → (ℤ/(N/h))ˣ); let n* = N/h*² and D* = diag(h*, 1). Then D*⁻¹Γ₀(n*)D* ≤ Nor(Γ_Δ(N)) ≤ D*⁻¹Γ₀(n*)⁺D*; an Atkin–Lehner element w_Q of level n* (conjugated by D*) normalizes Γ_Δ(N) iff ι*_Q(Δ̄) = Δ̄, where ι*_Q inverts the components of (ℤ/(N/h*))ˣ at the primes of Q; so Nor(Γ_Δ(N)) is described exactly, its index over Γ_Δ(N) is [(ℤ/N)ˣ :…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true}