Normalizers of Γ_Δ(N), Γ(N) and ±Γ₁(N)
Formal statements and proofs, in Lean 4 with Mathlib, about the normalizers in SL₂(ℝ) of the groups Γ_Δ(N) between Γ₁(N) and Γ₀(N), and the quotients Nor(Γ)/Γ, the modular automorphism groups of the curves X_Δ(N): a generalization of Newman's description of the normalizer to Γ_Δ(N); Nor(Γ(N)) = SL₂(ℤ), so the modular automorphism group of X(N) is SL₂(ℤ/N)/{±1}; and, for N ≠ 4, Nor(±Γ₁(N)) is generated by Γ₀(N) and the Atkin–Lehner elements, so X₁(N) has 2^ω(N) φ(N)/2 modular automorphisms for N ≥ 3 (N = 4 is an exception). 34 theorems, no sorry, only the axioms propext, Classical.choice and…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-18-000010
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-18-000010/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-18-000010/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'