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).

Scalar bookkeeping

theorem CongruenceNormalizers.inv_mul_inv_mul_eq_one {Q s : ℝ} (hs : s * s = Q) (hQ : Q ≠ 0) : s⁻¹ * s⁻¹ * Q = 1

theorem CongruenceNormalizers.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

theorem CongruenceNormalizers.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

theorem CongruenceNormalizers.coe_inv_of_coe_eq_smul {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} {s a b c d : ℝ} (h : ↑g = s • !![a, b; c, d]) : ↑g⁻¹ = s • !![d, -b; -c, a]

Translations

theorem CongruenceNormalizers.S_conj_mem {N k : ℕ} (hN : N ≠ 0) (hk : k ∣ hPart N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hγ : γ ∈ Gamma0R N) : S k * γ * (S k)⁻¹ ∈ Gamma0R N ∧ (S k)⁻¹ * γ * S k ∈ Gamma0R N

theorem CongruenceNormalizers.S_mem_normalizer' {N k : ℕ} [NeZero N] (hk : k ∣ hPart N) : S k ∈ Norm0 N

T1 for translations.

Atkin–Lehner elements

theorem CongruenceNormalizers.isAtkinLehner_conj_mem {N Q : ℕ} (hQ : Q ∣ N) (hQ0 : Q ≠ 0) {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : IsAtkinLehner N Q g) {γ : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hγ : γ ∈ Gamma0R N) : g * γ * g⁻¹ ∈ Gamma0R N ∧ g⁻¹ * γ * g ∈ Gamma0R N

theorem CongruenceNormalizers.isAtkinLehner_mem_normalizer' {N Q : ℕ} [NeZero N] (hQ : Q ∣ N) {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : IsAtkinLehner N Q g) : g ∈ Norm0 N

T1 for Atkin–Lehner elements.

noncomputable def CongruenceNormalizers.alElt (N Q : ℕ) (x y z w : ℤ) (h : ↑Q ^ 2 * x * w - ↑N * y * z = ↑Q) (hQ : Q ≠ 0) : Matrix.SpecialLinearGroup (Fin 2) ℝ

The AL element with explicit integer data.

Equations

• CongruenceNormalizers.alElt N Q x y z w h hQ = ⟨(√↑Q)⁻¹ • !![↑Q * ↑x, ↑y; ↑N * ↑z, ↑Q * ↑w], ⋯⟩

theorem CongruenceNormalizers.alElt_isAtkinLehner {N Q : ℕ} {x y z w : ℤ} (h : ↑Q ^ 2 * x * w - ↑N * y * z = ↑Q) (hQ : Q ≠ 0) : IsAtkinLehner N Q (alElt N Q x y z w h hQ)

theorem CongruenceNormalizers.exists_isAtkinLehner' {N Q : ℕ} [NeZero N] (hQ : Q ∣ N) (hcop : Q.Coprime (N / Q)) : ∃ (g : Matrix.SpecialLinearGroup (Fin 2) ℝ), IsAtkinLehner N Q g

Atkin–Lehner elements exist for Q ∥ N.

theorem CongruenceNormalizers.isAtkinLehner_mul_inv_mem' {N Q : ℕ} [NeZero N] (hQ : Q ∣ N) {g g' : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : IsAtkinLehner N Q g) (hg' : IsAtkinLehner N Q g') : g * g'⁻¹ ∈ Gamma0R N