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.

@[simp]
theorem SL_reduction_mod_hom_val (N : ) (γ : Matrix.SpecialLinearGroup (Fin 2) ) (i j : Fin 2) :
((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) i j = (γ i j)

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

Instances For
    def CongruenceSubgroup.«termΓ(_)» :
    Lean.ParserDescr

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

    Instances For
      @[simp]
      theorem CongruenceSubgroup.Gamma_mem {N : } {γ : Matrix.SpecialLinearGroup (Fin 2) } :
      γ Gamma N (γ 0 0) = 1 (γ 0 1) = 0 (γ 1 0) = 0 (γ 1 1) = 1
      theorem CongruenceSubgroup.ModularGroup_T_pow_mem_Gamma (N M : ) (hNM : N M) :
      ModularGroup.T ^ M Gamma N.natAbs

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

      Instances For
        @[simp]
        theorem CongruenceSubgroup.Gamma0_mem {N : } {A : Matrix.SpecialLinearGroup (Fin 2) } :
        A Gamma0 N (A 1 0) = 0

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

        Instances For

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

          Instances For
            @[simp]
            theorem CongruenceSubgroup.Gamma1_mem' {N : } {γ : (Gamma0 N)} :
            γ Gamma1' N (Gamma0Map N) γ = 1
            theorem CongruenceSubgroup.Gamma1_to_Gamma0_mem {N : } (A : (Gamma0 N)) :
            A Gamma1' N (A 0 0) = 1 (A 1 1) = 1 (A 1 0) = 0

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

            Instances For
              @[simp]
              theorem CongruenceSubgroup.Gamma1_mem (N : ) (A : Matrix.SpecialLinearGroup (Fin 2) ) :
              A Gamma1 N (A 0 0) = 1 (A 1 1) = 1 (A 1 0) = 0

              A congruence subgroup is a subgroup of SL(2, ℤ) which contains some Gamma N for some N ≠ 0.

              Instances For

                The subgroup SL(2, ℤ) ∩ g⁻¹ Γ g, for Γ a subgroup of SL(2, ℤ) and g ∈ GL(2, ℝ).

                Instances For
                  theorem CongruenceSubgroup.exists_Gamma_le_conj (g : GL (Fin 2) ) (M : ) [NeZero M] :
                  ∃ (N : ), N 0 xGamma N, g * (Matrix.SpecialLinearGroup.mapGL ) x * g⁻¹ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ) (Gamma M)

                  For any g ∈ GL(2, ℚ) and M ≠ 0, there exists N such that g x g⁻¹ ∈ Γ(M) for all x ∈ Γ(N).

                  For any g ∈ GL(2, ℚ) and M ≠ 0, there exists N such that g Γ(N) g⁻¹ ≤ Γ(M).

                  If Γ has finite index in SL(2, ℤ), then so does g⁻¹ Γ g ∩ SL(2, ℤ) for any g ∈ GL(2, ℚ).

                  Conjugates of SL(2, ℤ) by GL(2, ℚ) are arithmetic subgroups.

                  Conjugation by GL(2, ℚ) preserves arithmetic subgroups.

                  If Γ is a congruence subgroup, then so is g⁻¹ Γ g ∩ SL(2, ℤ) for any g ∈ GL(2, ℚ).