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
theorem
CongruenceNormalizers.newman_iff
{N : ℕ}
[NeZero N]
{g : Matrix.SpecialLinearGroup (Fin 2) ℝ}
:
Newman's integral matrix form characterizes the real normalizer of Γ₀(N).
theorem
CongruenceNormalizers.newman_delta
{N : ℕ}
[NeZero N]
(Δ : Subgroup (ZMod N)ˣ)
{g : Matrix.SpecialLinearGroup (Fin 2) ℝ}
(hg : g ∈ NormG (GammaDeltaR N Δ))
:
IsNewmanFormH N (hDelta N Δ) g
The corresponding necessary matrix form for the normalizer of Γ_Δ(N).