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

• Matrix.SpecialLinearGroup is the type of matrices with determinant 1
• Matrix.SpecialLinearGroup.group gives the group structure (under multiplication)
• Matrix.SpecialLinearGroup.toGL is the embedding SLₙ(R) → GLₙ(R)

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

• https://en.wikipedia.org/wiki/Special_linear_group

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

• Matrix.SpecialLinearGroup n R = { A : Matrix n n R // Matrix.det A = 1 }

def MatrixGroups.«termSL(_,_)» : Lean.ParserDescr

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.

instance Matrix.SpecialLinearGroup.hasCoeToMatrix {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Coe (Matrix.SpecialLinearGroup n R) (Matrix n n R)

Equations

• Matrix.SpecialLinearGroup.hasCoeToMatrix = { coe := fun (A : Matrix.SpecialLinearGroup n R) => ↑A }

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

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

Equations

• Matrix.SpecialLinearGroup.instCoeFun = { coe := fun (A : Matrix.SpecialLinearGroup n R) => ↑A }

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

instance Matrix.SpecialLinearGroup.hasInv {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Inv (Matrix.SpecialLinearGroup n R)

Equations

• Matrix.SpecialLinearGroup.hasInv = { inv := fun (A : Matrix.SpecialLinearGroup n R) => { val := Matrix.adjugate ↑A, property := (_ : Matrix.det (Matrix.adjugate ↑A) = 1) } }

instance Matrix.SpecialLinearGroup.hasMul {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Mul (Matrix.SpecialLinearGroup n R)

Equations

• Matrix.SpecialLinearGroup.hasMul = { mul := fun (A B : Matrix.SpecialLinearGroup n R) => { val := ↑A * ↑B, property := (_ : Matrix.det (↑A * ↑B) = 1) } }

instance Matrix.SpecialLinearGroup.hasOne {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : One (Matrix.SpecialLinearGroup n R)

Equations

• Matrix.SpecialLinearGroup.hasOne = { one := { val := 1, property := (_ : Matrix.det 1 = 1) } }

instance Matrix.SpecialLinearGroup.instPowSpecialLinearGroupNat {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Pow (Matrix.SpecialLinearGroup n R) ℕ

Equations

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

instance Matrix.SpecialLinearGroup.instInhabitedSpecialLinearGroup {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Inhabited (Matrix.SpecialLinearGroup n R)

Equations

• Matrix.SpecialLinearGroup.instInhabitedSpecialLinearGroup = { default := 1 }

def Matrix.SpecialLinearGroup.transpose {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) : Matrix.SpecialLinearGroup n R

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

Equations

• Matrix.SpecialLinearGroup.transpose A = { val := Matrix.transpose ↑A, property := (_ : Matrix.det (Matrix.transpose ↑A) = 1) }

def Matrix.SpecialLinearGroup.«term_ᵀ» : Lean.TrailingParserDescr

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

Equations

• Matrix.SpecialLinearGroup.«term_ᵀ» = Lean.ParserDescr.trailingNode `Matrix.SpecialLinearGroup.term_ᵀ 1024 1024 (Lean.ParserDescr.symbol "ᵀ")

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_inv {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) : ↑A⁻¹ = Matrix.adjugate ↑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.det_coe {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) : Matrix.det ↑A = 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

@[simp]

theorem Matrix.SpecialLinearGroup.coe_transpose {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) : ↑(Matrix.SpecialLinearGroup.transpose A) = Matrix.transpose ↑A

theorem Matrix.SpecialLinearGroup.det_ne_zero {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Nontrivial R] (g : Matrix.SpecialLinearGroup n R) : Matrix.det ↑g ≠ 0

theorem Matrix.SpecialLinearGroup.row_ne_zero {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Nontrivial R] (g : Matrix.SpecialLinearGroup n R) (i : n) : ↑g i ≠ 0

instance Matrix.SpecialLinearGroup.monoid {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Monoid (Matrix.SpecialLinearGroup n R)

Equations

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

instance Matrix.SpecialLinearGroup.instGroupSpecialLinearGroup {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Group (Matrix.SpecialLinearGroup n R)

Equations

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

def Matrix.SpecialLinearGroup.toLin' {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Matrix.SpecialLinearGroup n R →* (n → R) ≃ₗ[R] n → R

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

Equations

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

theorem Matrix.SpecialLinearGroup.toLin'_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) (v : n → R) : (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 : n → R) : (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'

def Matrix.SpecialLinearGroup.toGL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Matrix.SpecialLinearGroup n R →* LinearMap.GeneralLinearGroup R (n → R)

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

Equations

• Matrix.SpecialLinearGroup.toGL = MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm (LinearMap.GeneralLinearGroup.generalLinearEquiv R (n → R)))) Matrix.SpecialLinearGroup.toLin'

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) : ↑((Matrix.SpecialLinearGroup.map f) g) = (RingHom.mapMatrix f) ↑g

def Matrix.SpecialLinearGroup.map {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) : Matrix.SpecialLinearGroup n R →* Matrix.SpecialLinearGroup n S

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.

instance Matrix.SpecialLinearGroup.instCoeSpecialLinearGroupIntInstCommRingIntSpecialLinearGroup {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Coe (Matrix.SpecialLinearGroup n ℤ) (Matrix.SpecialLinearGroup n R)

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.

@[simp]

theorem Matrix.SpecialLinearGroup.coe_matrix_coe {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (g : Matrix.SpecialLinearGroup n ℤ) : ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom R)) g) = Matrix.map ↑g ⇑(Int.castRingHom R)

instance Matrix.SpecialLinearGroup.instNeg {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Fact (Even (Fintype.card n))] : Neg (Matrix.SpecialLinearGroup n R)

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

Equations

• Matrix.SpecialLinearGroup.instNeg = { neg := fun (g : Matrix.SpecialLinearGroup n R) => { val := -↑g, property := (_ : Matrix.det (-↑g) = 1) } }

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

instance Matrix.SpecialLinearGroup.instHasDistribNegSpecialLinearGroupHasMul {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Fact (Even (Fintype.card n))] : HasDistribNeg (Matrix.SpecialLinearGroup n R)

Equations

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

@[simp]

theorem Matrix.SpecialLinearGroup.coe_int_neg {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Fact (Even (Fintype.card n))] (g : Matrix.SpecialLinearGroup n ℤ) : (Matrix.SpecialLinearGroup.map (Int.castRingHom R)) (-g) = -(Matrix.SpecialLinearGroup.map (Int.castRingHom R)) 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) R → Prop) (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 : R) (b : R) (h : a ≠ 0), g = { val := Matrix.of ![![a, b], ![0, a⁻¹]], property := (_ : Matrix.det (Matrix.of ![![a, b], ![0, a⁻¹]]) = 1) }

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 2 → R} (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 2 → R} (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.

def ModularGroup.S : Matrix.SpecialLinearGroup (Fin 2) ℤ

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

• ModularGroup.S = { val := Matrix.of ![![0, -1], ![1, 0]], property := ModularGroup.S.proof_1 }

def ModularGroup.T : Matrix.SpecialLinearGroup (Fin 2) ℤ

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

Equations

• ModularGroup.T = { val := Matrix.of ![![1, 1], ![0, 1]], property := ModularGroup.T.proof_1 }

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

@[simp]

theorem ModularGroup.T_pow_mul_apply_one (n : ℤ) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ↑(ModularGroup.T ^ n * g) 1 = ↑g 1

@[simp]

theorem ModularGroup.T_mul_apply_one (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ↑(ModularGroup.T * g) 1 = ↑g 1

@[simp]

theorem ModularGroup.T_inv_mul_apply_one (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ↑(ModularGroup.T⁻¹ * g) 1 = ↑g 1