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 #

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

Instances For

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

Lean.ParserDescr

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

Instances For

@[implicit_reducible]

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

Coe (SpecialLinearGroup n R) (Matrix n n R)

@[implicit_reducible]

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.

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)

@[implicit_reducible]

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

Inv (SpecialLinearGroup n R)

@[implicit_reducible]

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

Mul (SpecialLinearGroup n R)

@[implicit_reducible]

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

One (SpecialLinearGroup n R)

@[implicit_reducible]

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

Pow (SpecialLinearGroup n R) ℕ

@[implicit_reducible]

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

Inhabited (SpecialLinearGroup n R)

@[implicit_reducible]

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

Fintype (SpecialLinearGroup n R)

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)

Instances For

def Matrix.SpecialLinearGroup.«term_ᵀ» :

Lean.TrailingParserDescr

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

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

@[implicit_reducible]

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

Monoid (SpecialLinearGroup n R)

@[implicit_reducible]

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

Group (SpecialLinearGroup n R)

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.

Instances For

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.

Instances For

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

Instances For

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

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

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

Instances For

theorem Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : ↥(Subgroup.center (SpecialLinearGroup n R))) :

↑↑A = (scalar n) ↑↑(center_equiv_rootsOfUnity A)

@[implicit_reducible]

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.

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

theorem Matrix.SpecialLinearGroup.map_intCast_injective {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [CharZero R] :

Function.Injective ⇑(map (Int.castRingHom R))

@[simp]

theorem Matrix.SpecialLinearGroup.map_intCast_inj {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [CharZero R] {x y : SpecialLinearGroup n ℤ} :

(map (Int.castRingHom R)) x = (map (Int.castRingHom R)) y ↔ x = y

@[implicit_reducible]

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.

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

@[implicit_reducible]

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)

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

Instances For

def ModularGroup.T :

Matrix.SpecialLinearGroup (Fin 2) ℤ

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

Instances For

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