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.

Instances For
    instance Matrix.SpecialLinearGroup.instCoeFun {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :
    CoeFun (Matrix.SpecialLinearGroup n R) fun x => nnR

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

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

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

    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

      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)
        @[simp]
        theorem Matrix.SpecialLinearGroup.map_apply_coe {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : Matrix.SpecialLinearGroup n R) :

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

        Instances For

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

          @[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
          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 := (_ : Matrix.det ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] = 1) }
          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 := (_ : Matrix.det (Matrix.of ![![a, b], ![c, d]]) = 1) }) (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 b h, g = { val := Matrix.of ![![a, b], ![0, a⁻¹]], property := (_ : Matrix.det (Matrix.of ![![a, b], ![0, a⁻¹]]) = 1) }

          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.

          Instances For

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

            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]]