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.

Tags #

matrix group, group, matrix inverse

def Matrix.SpecialLinearGroup (n : Type u) [] [] (R : Type v) [] :
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
instance Matrix.SpecialLinearGroup.hasCoeToMatrix {n : Type u} [] [] {R : Type v} [] :
Coe (Matrix n n R)
Equations
• Matrix.SpecialLinearGroup.hasCoeToMatrix = { coe := fun (A : ) => A }
instance Matrix.SpecialLinearGroup.instCoeFun {n : Type u} [] [] {R : Type v} [] :
CoeFun fun (x : ) => nnR

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

Equations
• Matrix.SpecialLinearGroup.instCoeFun = { coe := fun (A : ) => A }
theorem Matrix.SpecialLinearGroup.ext_iff {n : Type u} [] [] {R : Type v} [] (A : ) (B : ) :
A = B ∀ (i j : n), A i j = B i j
theorem Matrix.SpecialLinearGroup.ext {n : Type u} [] [] {R : Type v} [] (A : ) (B : ) :
(∀ (i j : n), A i j = B i j)A = B
Equations
• =
instance Matrix.SpecialLinearGroup.hasInv {n : Type u} [] [] {R : Type v} [] :
Equations
• Matrix.SpecialLinearGroup.hasInv = { inv := fun (A : ) => (A).adjugate, }
instance Matrix.SpecialLinearGroup.hasMul {n : Type u} [] [] {R : Type v} [] :
Equations
• Matrix.SpecialLinearGroup.hasMul = { mul := fun (A B : ) => A * B, }
instance Matrix.SpecialLinearGroup.hasOne {n : Type u} [] [] {R : Type v} [] :
Equations
• Matrix.SpecialLinearGroup.hasOne = { one := 1, }
instance Matrix.SpecialLinearGroup.instPowNat {n : Type u} [] [] {R : Type v} [] :
Equations
• Matrix.SpecialLinearGroup.instPowNat = { pow := fun (x : ) (n_1 : ) => x ^ n_1, }
instance Matrix.SpecialLinearGroup.instInhabited {n : Type u} [] [] {R : Type v} [] :
Equations
• Matrix.SpecialLinearGroup.instInhabited = { default := 1 }
def Matrix.SpecialLinearGroup.transpose {n : Type u} [] [] {R : Type v} [] (A : ) :

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

Equations
• A.transpose = (A).transpose,
Instances For

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

Equations
Instances For
theorem Matrix.SpecialLinearGroup.coe_mk {n : Type u} [] [] {R : Type v} [] (A : Matrix n n R) (h : A.det = 1) :
A, h = A
@[simp]
theorem Matrix.SpecialLinearGroup.coe_inv {n : Type u} [] [] {R : Type v} [] (A : ) :
@[simp]
theorem Matrix.SpecialLinearGroup.coe_mul {n : Type u} [] [] {R : Type v} [] (A : ) (B : ) :
(A * B) = A * B
@[simp]
theorem Matrix.SpecialLinearGroup.coe_one {n : Type u} [] [] {R : Type v} [] :
1 = 1
@[simp]
theorem Matrix.SpecialLinearGroup.det_coe {n : Type u} [] [] {R : Type v} [] (A : ) :
(A).det = 1
@[simp]
theorem Matrix.SpecialLinearGroup.coe_pow {n : Type u} [] [] {R : Type v} [] (A : ) (m : ) :
(A ^ m) = A ^ m
@[simp]
theorem Matrix.SpecialLinearGroup.coe_transpose {n : Type u} [] [] {R : Type v} [] (A : ) :
A.transpose = (A).transpose
theorem Matrix.SpecialLinearGroup.det_ne_zero {n : Type u} [] [] {R : Type v} [] [] (g : ) :
(g).det 0
theorem Matrix.SpecialLinearGroup.row_ne_zero {n : Type u} [] [] {R : Type v} [] [] (g : ) (i : n) :
g i 0
instance Matrix.SpecialLinearGroup.monoid {n : Type u} [] [] {R : Type v} [] :
Equations
instance Matrix.SpecialLinearGroup.instGroup {n : Type u} [] [] {R : Type v} [] :
Equations
• Matrix.SpecialLinearGroup.instGroup = let __src := Matrix.SpecialLinearGroup.monoid; let __src_1 := Matrix.SpecialLinearGroup.hasInv;
def Matrix.SpecialLinearGroup.toLin' {n : Type u} [] [] {R : Type v} [] :
→* (nR) ≃ₗ[R] nR

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} [] [] {R : Type v} [] (A : ) (v : nR) :
(Matrix.SpecialLinearGroup.toLin' A) v = (Matrix.toLin' A) v
theorem Matrix.SpecialLinearGroup.toLin'_to_linearMap {n : Type u} [] [] {R : Type v} [] (A : ) :
(Matrix.SpecialLinearGroup.toLin' A) = Matrix.toLin' A
theorem Matrix.SpecialLinearGroup.toLin'_symm_apply {n : Type u} [] [] {R : Type v} [] (A : ) (v : nR) :
(Matrix.SpecialLinearGroup.toLin' A).symm v = (Matrix.toLin' A⁻¹) v
theorem Matrix.SpecialLinearGroup.toLin'_symm_to_linearMap {n : Type u} [] [] {R : Type v} [] (A : ) :
(Matrix.SpecialLinearGroup.toLin' A).symm = Matrix.toLin' A⁻¹
theorem Matrix.SpecialLinearGroup.toLin'_injective {n : Type u} [] [] {R : Type v} [] :
Function.Injective Matrix.SpecialLinearGroup.toLin'
def Matrix.SpecialLinearGroup.toGL {n : Type u} [] [] {R : Type v} [] :

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

Equations
• Matrix.SpecialLinearGroup.toGL = ().symm.toMonoidHom.comp Matrix.SpecialLinearGroup.toLin'
Instances For
theorem Matrix.SpecialLinearGroup.coe_toGL {n : Type u} [] [] {R : Type v} [] (A : ) :
(Matrix.SpecialLinearGroup.toGL A) = (Matrix.SpecialLinearGroup.toLin' A)
@[simp]
theorem Matrix.SpecialLinearGroup.map_apply_coe {n : Type u} [] [] {R : Type v} [] {S : Type u_1} [] (f : R →+* S) (g : ) :
() = f.mapMatrix g
def Matrix.SpecialLinearGroup.map {n : Type u} [] [] {R : Type v} [] {S : Type u_1} [] (f : R →+* S) :

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

Equations
• = { toFun := fun (g : ) => f.mapMatrix g, , map_one' := , map_mul' := }
Instances For
@[simp]
theorem Matrix.SpecialLinearGroup.scalar_eq_self_of_mem_center {n : Type u} [] [] {R : Type v} [] {A : } (hA : ) (i : n) :
() (A i i) = A
theorem Matrix.SpecialLinearGroup.scalar_eq_coe_self_center {n : Type u} [] [] {R : Type v} [] (A : ) (i : n) :
() (A i i) = A
theorem Matrix.SpecialLinearGroup.mem_center_iff {n : Type u} [] [] {R : Type v} [] {A : } :
∃ (r : R), = 1 () 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.

@[simp]
theorem Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply {n : Type u} [] [] {R : Type v} [] (i : n) (A : ) :
@[simp]
theorem Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe {n : Type u} [] [] {R : Type v} [] (i : n) (a : (rootsOfUnity ().toPNat' R)) :
() = a 1
def Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' {n : Type u} [] [] {R : Type v} [] (i : n) :
≃* (rootsOfUnity ().toPNat' 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.
Instances For
noncomputable def Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity {n : Type u} [] [] {R : Type v} [] :
≃* (rootsOfUnity ().toPNat' 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.
Instances For
instance Matrix.SpecialLinearGroup.instCoeInt {n : Type u} [] [] {R : Type v} [] :

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

Equations
• Matrix.SpecialLinearGroup.instCoeInt = { coe := fun (x : ) => }
@[simp]
theorem Matrix.SpecialLinearGroup.coe_matrix_coe {n : Type u} [] [] {R : Type v} [] (g : ) :
() = (g).map ()
instance Matrix.SpecialLinearGroup.instNeg {n : Type u} [] [] {R : Type v} [] [Fact (Even ())] :

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

Equations
• Matrix.SpecialLinearGroup.instNeg = { neg := fun (g : ) => -g, }
@[simp]
theorem Matrix.SpecialLinearGroup.coe_neg {n : Type u} [] [] {R : Type v} [] [Fact (Even ())] (g : ) :
(-g) = -g
instance Matrix.SpecialLinearGroup.instHasDistribNeg {n : Type u} [] [] {R : Type v} [] [Fact (Even ())] :
Equations
@[simp]
theorem Matrix.SpecialLinearGroup.coe_int_neg {n : Type u} [] [] {R : Type v} [] [Fact (Even ())] (g : ) :
theorem Matrix.SpecialLinearGroup.SL2_inv_expl_det {R : Type v} [] (A : ) :
Matrix.det ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]] = 1
theorem Matrix.SpecialLinearGroup.SL2_inv_expl {R : Type v} [] (A : ) :
A⁻¹ = ![![A 1 1, -A 0 1], ![-A 1 0, A 0 0]],
theorem Matrix.SpecialLinearGroup.fin_two_induction {R : Type v} [] (P : Prop) (h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P Matrix.of ![![a, b], ![c, d]], ) (g : ) :
P g
theorem Matrix.SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero {R : Type u_2} [] (g : ) (hg : g 1 0 = 0) :
∃ (a : R) (b : R) (h : a 0), g = Matrix.of ![![a, b], ![0, a⁻¹]],
theorem Matrix.SpecialLinearGroup.isCoprime_row {R : Type v} [] (A : ) (i : Fin 2) :
IsCoprime (A i 0) (A i 1)
theorem Matrix.SpecialLinearGroup.isCoprime_col {R : Type v} [] (A : ) (j : Fin 2) :
IsCoprime (A 0 j) (A 1 j)
theorem IsCoprime.exists_SL2_col {R : Type u_1} [] {a : R} {b : R} (hab : ) (j : Fin 2) :
∃ (g : ), 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} [] {a : R} {b : R} (hab : ) (i : Fin 2) :
∃ (g : ), 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} [] {v : Fin 2R} (hab : IsCoprime (v 0) (v 1)) (A : ) :
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} [] {v : Fin 2R} (hab : IsCoprime (v 0) (v 1)) (A : ) :
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.

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 :
= Matrix.of ![![0, -1], ![1, 0]]
theorem ModularGroup.coe_T :
= Matrix.of ![![1, 1], ![0, 1]]
theorem ModularGroup.coe_T_inv :
= Matrix.of ![![1, -1], ![0, 1]]
theorem ModularGroup.coe_T_zpow (n : ) :
() = Matrix.of ![![1, n], ![0, 1]]
@[simp]
theorem ModularGroup.T_pow_mul_apply_one (n : ) (g : ) :
( * g) 1 = g 1
@[simp]
theorem ModularGroup.T_mul_apply_one (g : ) :
() 1 = g 1
@[simp]
theorem ModularGroup.T_inv_mul_apply_one (g : ) :
() 1 = g 1