Normalizers of congruence subgroups at mixed level: Γ_{H₁}(N₁) ∩ Γ_{H₂}(N₂)
Formal statements and proofs, in Lean 4 with Mathlib, about the normalizer in SL₂(ℝ) of Γ = Γ_{H₁}(N₁) ∩ Γ_{H₂}(N₂) for coprime N₁ and N₂, the group of the fibre product X_{H₁} ×_{X(1)} X_{H₂}, where H₁ ≤ SL₂(ℤ/N₁) is such that, at every p ∣ N₁, H₁ mod p fixes no line or H₁ mod p^{v_p(N₁)} lies in a split Cartan subgroup, and H₂ ≤ SL₂(ℤ/N₂) is arbitrary. Nor(Γ) ≤ Nor(Γ_{H₂}(N₂)); an element (det m)^{−1/2}·m of Nor(Γ_{H₂}(N₂)) normalizes Γ iff m mod N₁ normalizes H₁; and |Nor(Γ)/Γ| is [N(H₁) : H₁] times the number of classes of Nor(Γ_{H₂})/Γ_{H₂} whose determinant mod N₁ is the determinant of…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-20-000011
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-20-000011/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-20-000011/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'