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 // A.det = 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 (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 (SpecialLinearGroup n R) fun (x : 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 B : 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 B : SpecialLinearGroup n R) : (∀ (i j : n), ↑A i j = ↑B i j) → A = B

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

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

Equations

• Matrix.SpecialLinearGroup.hasInv = { inv := fun (A : Matrix.SpecialLinearGroup n R) => ⟨(↑A).adjugate, ⋯⟩ }

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

Equations

• Matrix.SpecialLinearGroup.hasMul = { mul := fun (A B : Matrix.SpecialLinearGroup n R) => ⟨↑A * ↑B, ⋯⟩ }

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

Equations

• Matrix.SpecialLinearGroup.hasOne = { one := ⟨1, ⋯⟩ }

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

Equations

• Matrix.SpecialLinearGroup.instPowNat = { pow := fun (x : Matrix.SpecialLinearGroup n R) (n_1 : ℕ) => ⟨↑x ^ n_1, ⋯⟩ }

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

Equations

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

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

Equations

• Matrix.SpecialLinearGroup.instFintypeOfDecidableEq = Subtype.fintype fun (A : Matrix n n R) => A.det = 1

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

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

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

Equations

• A.transpose = ⟨(↑A).transpose, ⋯⟩

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 : A.det = 1) : ↑⟨A, h⟩ = A

@[simp]

theorem Matrix.SpecialLinearGroup.coe_inv {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : SpecialLinearGroup n R) : ↑A⁻¹ = (↑A).adjugate

@[simp]

theorem Matrix.SpecialLinearGroup.coe_mul {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A B : 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 : SpecialLinearGroup n R) : (↑A).det = 1

@[simp]

theorem Matrix.SpecialLinearGroup.coe_pow {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : 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 : SpecialLinearGroup n R) : ↑A.transpose = (↑A).transpose

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

theorem Matrix.SpecialLinearGroup.row_ne_zero {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Nontrivial R] (g : 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 (SpecialLinearGroup n R)

Equations

• Matrix.SpecialLinearGroup.monoid = Function.Injective.monoid (fun (a : { A : Matrix n n R // A.det = 1 }) => ↑a) ⋯ ⋯ ⋯ ⋯

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

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

theorem Matrix.SpecialLinearGroup.toLin'_injective {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Function.Injective ⇑toLin'

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) : SpecialLinearGroup n R →* SpecialLinearGroup n S

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

Equations

• Matrix.SpecialLinearGroup.map f = { toFun := fun (g : Matrix.SpecialLinearGroup n R) => ⟨f.mapMatrix ↑g, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[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 : SpecialLinearGroup n R) : ↑((map f) g) = f.mapMatrix ↑g

@[simp]

theorem Matrix.SpecialLinearGroup.center_eq_bot_of_subsingleton {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Subsingleton n] : Subgroup.center (SpecialLinearGroup n R) = ⊥

theorem Matrix.SpecialLinearGroup.scalar_eq_self_of_mem_center {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {A : SpecialLinearGroup n R} (hA : A ∈ Subgroup.center (SpecialLinearGroup n R)) (i : n) : (scalar n) (↑A i i) = ↑A

theorem Matrix.SpecialLinearGroup.scalar_eq_coe_self_center {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : ↥(Subgroup.center (SpecialLinearGroup n R))) (i : n) : (scalar n) (↑↑A i i) = ↑↑A

theorem Matrix.SpecialLinearGroup.mem_center_iff {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {A : SpecialLinearGroup n R} : A ∈ Subgroup.center (SpecialLinearGroup n R) ↔ ∃ (r : R), r ^ Fintype.card n = 1 ∧ (scalar n) r = ↑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.

def Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (i : n) : ↥(Subgroup.center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (Fintype.card n) R)

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.

@[simp]

theorem Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (i : n) (A : ↥(Subgroup.center (SpecialLinearGroup n R))) : (center_equiv_rootsOfUnity' i) A = rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯

@[simp]

theorem Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (i : n) (a : ↥(rootsOfUnity (Fintype.card n) R)) : ↑↑((center_equiv_rootsOfUnity' i).symm a) = a • 1

noncomputable def Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : ↥(Subgroup.center (SpecialLinearGroup n R)) ≃* ↥(rootsOfUnity (max (Fintype.card n) 1) R)

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.

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

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

Equations

• Matrix.SpecialLinearGroup.instCoeInt = { coe := fun (x : Matrix.SpecialLinearGroup n ℤ) => (Matrix.SpecialLinearGroup.map (Int.castRingHom R)) x }

@[simp]

theorem Matrix.SpecialLinearGroup.coe_matrix_coe {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (g : SpecialLinearGroup n ℤ) : ↑((map (Int.castRingHom R)) g) = (↑g).map ⇑(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 (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) => ⟨-↑g, ⋯⟩ }

@[simp]

theorem Matrix.SpecialLinearGroup.coe_neg {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Fact (Even (Fintype.card n))] (g : SpecialLinearGroup n R) : ↑(-g) = -↑g

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

Equations

• Matrix.SpecialLinearGroup.instHasDistribNeg = Function.Injective.hasDistribNeg (fun (a : { A : Matrix n n R // A.det = 1 }) => ↑a) ⋯ ⋯ ⋯

@[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 : SpecialLinearGroup n ℤ) : (map (Int.castRingHom R)) (-g) = -(map (Int.castRingHom R)) g

theorem Matrix.SpecialLinearGroup.SL2_inv_expl_det {R : Type v} [CommRing R] (A : SpecialLinearGroup (Fin 2) R) : 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 : SpecialLinearGroup (Fin 2) R) : A⁻¹ = ⟨![![↑A 1 1, -↑A 0 1], ![-↑A 1 0, ↑A 0 0]], ⋯⟩

theorem Matrix.SpecialLinearGroup.fin_two_induction {R : Type v} [CommRing R] (P : SpecialLinearGroup (Fin 2) R → Prop) (h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩) (g : 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 : SpecialLinearGroup (Fin 2) R) (hg : ↑g 1 0 = 0) : ∃ (a : R) (b : R) (h : a ≠ 0), g = ⟨!![a, b; 0, a⁻¹], ⋯⟩

theorem Matrix.SpecialLinearGroup.isCoprime_row {R : Type v} [CommRing R] (A : 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 : 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 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 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 ((↑A).mulVec v 0) ((↑A).mulVec 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 = ⟨!![0, -1; 1, 0], ModularGroup.S._proof_49⟩

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

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

Equations

• ModularGroup.T = ⟨!![1, 1; 0, 1], ModularGroup.T._proof_50⟩

theorem ModularGroup.coe_S : ↑S = !![0, -1; 1, 0]

theorem ModularGroup.coe_T : ↑T = !![1, 1; 0, 1]

theorem ModularGroup.coe_T_inv : ↑T⁻¹ = !![1, -1; 0, 1]

theorem ModularGroup.coe_T_zpow (n : ℤ) : ↑(T ^ n) = !![1, n; 0, 1]

@[simp]

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

@[simp]

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

@[simp]

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

theorem ModularGroup.S_mul_S_eq : ↑S * ↑S = -1

theorem ModularGroup.T_S_rel : S • S • S • T • S • T • S = T⁻¹