Documentation

Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Congruence subgroups #

This defines congruence subgroups of SL(2, ℤ) such as Γ(N), Γ₀(N) and Γ₁(N) for N a natural number.

It also contains basic results about congruence subgroups.

source
@[simp]
theorem SL_reduction_mod_hom_val (N : ℕ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (i : Fin 2) (j : Fin 2) :
↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) i j = ↑(↑γ i j)
source
def Gamma (N : ℕ) :
Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)

The full level N congruence subgroup of SL(2, ℤ) of matrices that reduce to the identity modulo N.

Equations
Instances For
    source
    theorem Gamma_mem' (N : ℕ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
    γ ∈ Gamma N ↔ (Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
    source
    @[simp]
    theorem Gamma_mem (N : ℕ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
    γ ∈ Gamma N ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
    source
    theorem Gamma_normal (N : ℕ) :
    Subgroup.Normal (Gamma N)
    source
    theorem Gamma_one_top :
    Gamma 1 = ⊤
    source
    theorem Gamma_zero_bot :
    Gamma 0 = ⊥
    source
    def Gamma0 (N : ℕ) :
    Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)

    The congruence subgroup of SL(2, ℤ) of matrices whose lower left-hand entry reduces to zero modulo N.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Gamma0_mem (N : ℕ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
      A ∈ Gamma0 N ↔ ↑(↑A 1 0) = 0
      source
      theorem Gamma0_det (N : ℕ) (A : ↥(Gamma0 N)) :
      ↑(Matrix.det ↑↑A) = 1
      source
      def Gamma0Map (N : ℕ) :
      ↥(Gamma0 N) →* ZMod N

      The group homomorphism from Gamma0 to ZMod N given by mapping a matrix to its lower right-hand entry.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Gamma1' (N : ℕ) :
        Subgroup ↥(Gamma0 N)

        The congruence subgroup Gamma1 (as a subgroup of Gamma0) of matrices whose bottom row is congruent to (0,1) modulo N.

        Equations
        Instances For
          source
          @[simp]
          theorem Gamma1_mem' (N : ℕ) (γ : ↥(Gamma0 N)) :
          γ ∈ Gamma1' N ↔ (Gamma0Map N) γ = 1
          source
          theorem Gamma1_to_Gamma0_mem (N : ℕ) (A : ↥(Gamma0 N)) :
          A ∈ Gamma1' N ↔ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
          source
          def Gamma1 (N : ℕ) :
          Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)

          The congruence subgroup Gamma1 of SL(2, ℤ) consisting of matrices whose bottom row is congruent to (0,1) modulo N.

          Equations
          Instances For
            source
            @[simp]
            theorem Gamma1_mem (N : ℕ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) :
            A ∈ Gamma1 N ↔ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
            source
            theorem Gamma1_in_Gamma0 (N : ℕ) :
            Gamma1 N ≤ Gamma0 N
            source
            def IsCongruenceSubgroup (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) :
            Prop

            A congruence subgroup is a subgroup of SL(2, ℤ) which contains some Gamma N for some (N : ℕ+).

            Equations
            Instances For
              source
              theorem isCongruenceSubgroup_trans (H : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (K : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (h : H ≤ K) (h2 : IsCongruenceSubgroup H) :
              IsCongruenceSubgroup K
              source
              theorem Gamma_is_cong_sub (N : ℕ+) :
              IsCongruenceSubgroup (Gamma ↑N)
              source
              theorem Gamma1_is_congruence (N : ℕ+) :
              IsCongruenceSubgroup (Gamma1 ↑N)
              source
              theorem Gamma0_is_congruence (N : ℕ+) :
              IsCongruenceSubgroup (Gamma0 ↑N)
              source
              theorem Gamma_cong_eq_self (N : ℕ) (g : ConjAct (Matrix.SpecialLinearGroup (Fin 2) ℤ)) :
              g • Gamma N = Gamma N
              source
              theorem conj_cong_is_cong (g : ConjAct (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (h : IsCongruenceSubgroup Γ) :
              IsCongruenceSubgroup (g • Γ)