Documentation

LeanPool.CongruenceNormalizers.NormalizerLean.Basic

Basic API for Γ₀(N) ≤ SL₂(ℝ), its normalizer, B(N), S_k and h(N) #

Membership in Γ₀(N) #

source
@[reducible, inline]
abbrev CongruenceNormalizers.castM (M : Matrix (Fin 2) (Fin 2) ℤ) :
Matrix (Fin 2) (Fin 2) ℝ

The real matrix of an integer matrix.

Equations
Instances For
    source
    theorem CongruenceNormalizers.mem_Gamma0R_iff {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} :
    g ∈ Gamma0R N ↔ ∃ (M : Matrix (Fin 2) (Fin 2) ℤ), ↑N ∣ M 1 0 ∧ ↑g = castM M
    source
    theorem CongruenceNormalizers.mem_Gamma0R_of_entries {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (a b c d : ℤ) (hg : ↑g = !![↑a, ↑b; ↑c, ↑d]) (hc : ↑N ∣ c) :
    g ∈ Gamma0R N

    Membership in Γ₀(N) from explicit integer entries.

    source
    theorem CongruenceNormalizers.exists_entries_of_mem_Gamma0R {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Gamma0R N) :
    ∃ (a : ℤ) (b : ℤ) (c : ℤ) (d : ℤ), a * d - b * c = 1 ∧ ↑N ∣ c ∧ ↑g = !![↑a, ↑b; ↑c, ↑d]

    Elements of Γ₀(N) have integer entries, lower-left divisible by N, determinant 1.

    The normalizer #

    source
    theorem CongruenceNormalizers.mem_Norm0_of {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (h₁ : ∀ γ ∈ Gamma0R N, g * γ * g⁻¹ ∈ Gamma0R N) (h₂ : ∀ γ ∈ Gamma0R N, g⁻¹ * γ * g ∈ Gamma0R N) :
    g ∈ Norm0 N

    Normalizer criterion: g Γ g⁻¹ ⊆ Γ and g⁻¹ Γ g ⊆ Γ.

    source
    theorem CongruenceNormalizers.Gamma0R_le_Norm0 (N : ℕ) :
    Gamma0R N ≤ Norm0 N

    B(N) #

    source
    theorem CongruenceNormalizers.B.isClassOf_mk {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Norm0 N) :
    IsClassOf (↑⟨g, hg⟩) g
    source
    theorem CongruenceNormalizers.B.mk_eq_mk_iff {N : ℕ} {g g' : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Norm0 N) (hg' : g' ∈ Norm0 N) :
    ↑⟨g, hg⟩ = ↑⟨g', hg'⟩ ↔ g⁻¹ * g' ∈ Gamma0R N
    source
    theorem CongruenceNormalizers.B.mk_eq_one_iff {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Norm0 N) :
    ↑⟨g, hg⟩ = 1 ↔ g ∈ Gamma0R N
    source
    theorem CongruenceNormalizers.mul_inv_mem_iff_inv_mul_mem {N : ℕ} {a b : Matrix.SpecialLinearGroup (Fin 2) ℝ} (ha : a ∈ Norm0 N) :
    a * b⁻¹ ∈ Gamma0R N ↔ a⁻¹ * b ∈ Gamma0R N

    In the normalizer, a * b⁻¹ ∈ Γ ↔ a⁻¹ * b ∈ Γ.

    Translations S_k #

    source
    theorem CongruenceNormalizers.coe_S (k : ℕ) :
    ↑(S k) = !![1, (↑k)⁻¹; 0, 1]
    source
    theorem CongruenceNormalizers.coe_S_pow (k m : ℕ) :
    ↑(S k ^ m) = !![1, ↑m * (↑k)⁻¹; 0, 1]
    source
    theorem CongruenceNormalizers.coe_S_inv (k : ℕ) :
    ↑(S k)⁻¹ = !![1, -(↑k)⁻¹; 0, 1]
    source
    theorem CongruenceNormalizers.S_one_mem (N : ℕ) :
    S 1 ∈ Gamma0R N

    h(N) #

    source
    theorem CongruenceNormalizers.hPart_pos (N : ℕ) :
    0 < hPart N
    source
    theorem CongruenceNormalizers.hPart_dvd_24 (N : ℕ) :
    hPart N ∣ 24
    source
    theorem CongruenceNormalizers.dvd_hPart_of_sq_dvd {N : ℕ} (hN : N ≠ 0) {α β : ℕ} (hα : α ≤ 3) (hβ : β ≤ 1) (h : (2 ^ α * 3 ^ β) ^ 2 ∣ N) :
    2 ^ α * 3 ^ β ∣ hPart N

    Key divisibility: if (2^α 3^β)² ∣ N with α ≤ 3, β ≤ 1, then 2^α 3^β ∣ h(N).

    source
    theorem CongruenceNormalizers.hPart_sq_dvd {N : ℕ} (hN : N ≠ 0) :
    hPart N ^ 2 ∣ N
    source
    theorem CongruenceNormalizers.dvd_hPart_iff {N : ℕ} (hN : N ≠ 0) {d : ℕ} (hd : d ∣ 24) (hsq : d ^ 2 ∣ N) :
    d ∣ hPart N
    source
    theorem CongruenceNormalizers.hPart_isGreatest' (N : ℕ) [NeZero N] :
    IsGreatest {d : ℕ | d ∣ 24 ∧ d ^ 2 ∣ N} (hPart N)

    Units modulo divisors of 24 square to 1 #

    source
    theorem CongruenceNormalizers.modEq_of_mul_modEq_one {k : ℕ} (hk : k ∣ 24) {a d : ℤ} (h : a * d ≡ 1 [ZMOD ↑k]) :
    a ≡ d [ZMOD ↑k]