Documentation

Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

The Special Linear group $SL(n, R)$ #

This file defines the elements of the Special Linear group SpecialLinearGroup n R, consisting of all square R-matrices with determinant 1 on the fintype n by n. In addition, we define the group structure on SpecialLinearGroup n R and the embedding into the general linear group GeneralLinearGroup R (n → R).

Main definitions #

Notation #

For m : ℕ, we introduce the notation SL(m,R) for the special linear group on the fintype n = Fin m, in the locale MatrixGroups.

Implementation notes #

The inverse operation in the SpecialLinearGroup is defined to be the adjugate matrix, so that SpecialLinearGroup n R has a group structure for all CommRing R.

We define the elements of SpecialLinearGroup to be matrices, since we need to compute their determinant. This is in contrast with GeneralLinearGroup R M, which consists of invertible R-linear maps on M.

We provide Matrix.SpecialLinearGroup.hasCoeToFun for convenience, but do not state any lemmas about it, and use Matrix.SpecialLinearGroup.coeFn_eq_coe to eliminate it in favor of a regular coercion.

References #

Tags #

matrix group, group, matrix inverse

def Matrix.SpecialLinearGroup (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] :
Type (max 0 u v)

SpecialLinearGroup n R is the group of n by n R-matrices with determinant equal to 1.

Equations
Instances For

    SpecialLinearGroup n R is the group of n by n R-matrices with determinant equal to 1.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations

      This instance is here for convenience, but is literally the same as the coercion from hasCoeToMatrix.

      Equations
      theorem Matrix.SpecialLinearGroup.ext_iff {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) (B : Matrix.SpecialLinearGroup n R) :
      A = B ∀ (i j : n), A i j = B i j
      theorem Matrix.SpecialLinearGroup.ext {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) (B : Matrix.SpecialLinearGroup n R) :
      (∀ (i j : n), A i j = B i j)A = B
      Equations
      Equations
      Equations
      • Matrix.SpecialLinearGroup.hasOne = { one := { val := 1, property := } }
      Equations
      • Matrix.SpecialLinearGroup.instPowSpecialLinearGroupNat = { pow := fun (x : Matrix.SpecialLinearGroup n R) (n_1 : ) => { val := x ^ n_1, property := } }
      Equations
      • Matrix.SpecialLinearGroup.instInhabitedSpecialLinearGroup = { default := 1 }

      The transpose of a matrix in SL(n, R)

      Equations
      Instances For

        The transpose of a matrix in SL(n, R)

        Equations
        Instances For
          theorem Matrix.SpecialLinearGroup.coe_mk {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) (h : Matrix.det A = 1) :
          { val := A, property := h } = A
          @[simp]
          theorem Matrix.SpecialLinearGroup.coe_mul {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) (B : Matrix.SpecialLinearGroup n R) :
          (A * B) = A * B
          @[simp]
          theorem Matrix.SpecialLinearGroup.coe_one {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :
          1 = 1
          @[simp]
          theorem Matrix.SpecialLinearGroup.coe_pow {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) (m : ) :
          (A ^ m) = A ^ m
          Equations
          Equations
          • Matrix.SpecialLinearGroup.instGroupSpecialLinearGroup = let __src := Matrix.SpecialLinearGroup.monoid; let __src_1 := Matrix.SpecialLinearGroup.hasInv; Group.mk

          A version of Matrix.toLin' A that produces linear equivalences.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem Matrix.SpecialLinearGroup.toLin'_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) (v : nR) :
            (Matrix.SpecialLinearGroup.toLin' A) v = (Matrix.toLin' A) v
            theorem Matrix.SpecialLinearGroup.toLin'_to_linearMap {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) :
            (Matrix.SpecialLinearGroup.toLin' A) = Matrix.toLin' A
            theorem Matrix.SpecialLinearGroup.toLin'_symm_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) (v : nR) :
            (LinearEquiv.symm (Matrix.SpecialLinearGroup.toLin' A)) v = (Matrix.toLin' A⁻¹) v
            theorem Matrix.SpecialLinearGroup.toLin'_symm_to_linearMap {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) :
            (LinearEquiv.symm (Matrix.SpecialLinearGroup.toLin' A)) = Matrix.toLin' A⁻¹
            theorem Matrix.SpecialLinearGroup.toLin'_injective {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :
            Function.Injective Matrix.SpecialLinearGroup.toLin'

            toGL is the map from the special linear group to the general linear group

            Equations
            Instances For
              theorem Matrix.SpecialLinearGroup.coe_toGL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) :
              (Matrix.SpecialLinearGroup.toGL A) = (Matrix.SpecialLinearGroup.toLin' A)

              A ring homomorphism from R to S induces a group homomorphism from SpecialLinearGroup n R to SpecialLinearGroup n S.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem Matrix.SpecialLinearGroup.scalar_eq_coe_self_center {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : (Subgroup.center (Matrix.SpecialLinearGroup n R))) (i : n) :
                (Matrix.scalar n) (A i i) = A

                The center of a special linear group of degree n is the subgroup of scalar matrices, for which the scalars are the n-th roots of unity.

                An equivalence of groups, from the center of the special linear group to the roots of unity.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  An equivalence of groups, from the center of the special linear group to the roots of unity.

                  See also center_equiv_rootsOfUnity'.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Coercion of SL n to SL n R for a commutative ring R.

                    Equations
                    • One or more equations did not get rendered due to their size.

                    Formal operation of negation on special linear group on even cardinality n given by negating each element.

                    Equations
                    @[simp]
                    theorem Matrix.SpecialLinearGroup.coe_neg {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Fact (Even (Fintype.card n))] (g : Matrix.SpecialLinearGroup n R) :
                    (-g) = -g
                    Equations
                    theorem Matrix.SpecialLinearGroup.SL2_inv_expl_det {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup (Fin 2) R) :
                    Matrix.det ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] = 1
                    theorem Matrix.SpecialLinearGroup.SL2_inv_expl {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup (Fin 2) R) :
                    A⁻¹ = { val := ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]], property := }
                    theorem Matrix.SpecialLinearGroup.fin_two_induction {R : Type v} [CommRing R] (P : Matrix.SpecialLinearGroup (Fin 2) RProp) (h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P { val := Matrix.of ![![a, b], ![c, d]], property := }) (g : Matrix.SpecialLinearGroup (Fin 2) R) :
                    P g
                    theorem Matrix.SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero {R : Type u_2} [Field R] (g : Matrix.SpecialLinearGroup (Fin 2) R) (hg : g 1 0 = 0) :
                    ∃ (a : R) (b : R) (h : a 0), g = { val := Matrix.of ![![a, b], ![0, a⁻¹]], property := }
                    theorem Matrix.SpecialLinearGroup.isCoprime_row {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup (Fin 2) R) (i : Fin 2) :
                    IsCoprime (A i 0) (A i 1)
                    theorem Matrix.SpecialLinearGroup.isCoprime_col {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup (Fin 2) R) (j : Fin 2) :
                    IsCoprime (A 0 j) (A 1 j)
                    theorem IsCoprime.exists_SL2_col {R : Type u_1} [CommRing R] {a : R} {b : R} (hab : IsCoprime a b) (j : Fin 2) :
                    ∃ (g : Matrix.SpecialLinearGroup (Fin 2) R), g 0 j = a g 1 j = b

                    Given any pair of coprime elements of R, there exists a matrix in SL(2, R) having those entries as its left or right column.

                    theorem IsCoprime.exists_SL2_row {R : Type u_1} [CommRing R] {a : R} {b : R} (hab : IsCoprime a b) (i : Fin 2) :
                    ∃ (g : Matrix.SpecialLinearGroup (Fin 2) R), g i 0 = a g i 1 = b

                    Given any pair of coprime elements of R, there exists a matrix in SL(2, R) having those entries as its top or bottom row.

                    theorem IsCoprime.vecMulSL {R : Type u_1} [CommRing R] {v : Fin 2R} (hab : IsCoprime (v 0) (v 1)) (A : Matrix.SpecialLinearGroup (Fin 2) R) :
                    IsCoprime (Matrix.vecMul v (A) 0) (Matrix.vecMul v (A) 1)

                    A vector with coprime entries, right-multiplied by a matrix in SL(2, R), has coprime entries.

                    theorem IsCoprime.mulVecSL {R : Type u_1} [CommRing R] {v : Fin 2R} (hab : IsCoprime (v 0) (v 1)) (A : Matrix.SpecialLinearGroup (Fin 2) R) :
                    IsCoprime (Matrix.mulVec (A) v 0) (Matrix.mulVec (A) v 1)

                    A vector with coprime entries, left-multiplied by a matrix in SL(2, R), has coprime entries.

                    The matrix S = [[0, -1], [1, 0]] as an element of SL(2, ℤ).

                    This element acts naturally on the Euclidean plane as a rotation about the origin by π / 2.

                    This element also acts naturally on the hyperbolic plane as rotation about i by π. It represents the Mobiüs transformation z ↦ -1/z and is an involutive elliptic isometry.

                    Equations
                    Instances For

                      The matrix T = [[1, 1], [0, 1]] as an element of SL(2, ℤ)

                      Equations
                      Instances For
                        theorem ModularGroup.coe_S :
                        ModularGroup.S = Matrix.of ![![0, -1], ![1, 0]]
                        theorem ModularGroup.coe_T :
                        ModularGroup.T = Matrix.of ![![1, 1], ![0, 1]]
                        theorem ModularGroup.coe_T_inv :
                        ModularGroup.T⁻¹ = Matrix.of ![![1, -1], ![0, 1]]
                        theorem ModularGroup.coe_T_zpow (n : ) :
                        (ModularGroup.T ^ n) = Matrix.of ![![1, n], ![0, 1]]