mathlib documentation

linear_algebra.special_linear_group

The Special Linear group $SL(n, R)$

This file defines the elements of the Special Linear group special_linear_group n R, also written SL(n, R) or SLₙ(R), consisting of all n by n R-matrices with determinant 1. In addition, we define the group structure on special_linear_group n R and the embedding into the general linear group general_linear_group R (n → R) (i.e. GL(n, R) or GLₙ(R)).

Main definitions

matrix.special_linear_group is the type of matrices with determinant 1
matrix.special_linear_group.group gives the group structure (under multiplication)
matrix.special_linear_group.embedding_GL is the embedding SLₙ(R) → GLₙ(R)

Implementation notes

The inverse operation in the special_linear_group is defined to be the adjugate matrix, so that special_linear_group n R has a group structure for all comm_ring R.

We define the elements of special_linear_group to be matrices, since we need to compute their determinant. This is in contrast with general_linear_group R M, which consists of invertible R-linear maps on M.

References

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

Tags

matrix group, group, matrix inverse

def matrix.special_linear_group (n : Type u) [decidable_eq n] [fintype n] (R : Type v) [comm_ring R] :

Type (max u v)

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

Equations

matrix.special_linear_group n R = {A // A.det = 1}

@[instance]

def matrix.special_linear_group.coe_matrix {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

has_coe (matrix.special_linear_group n R) (matrix n n R)

Equations

matrix.special_linear_group.coe_matrix = {coe := λ (A : matrix.special_linear_group n R), A.val}

@[instance]

def matrix.special_linear_group.coe_fun {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

has_coe_to_fun (matrix.special_linear_group n R)

Equations

matrix.special_linear_group.coe_fun = {F := λ (_x : matrix.special_linear_group n R), n → n → R, coe := λ (A : matrix.special_linear_group n R), A.val}

def matrix.special_linear_group.to_lin {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix.special_linear_group n R) :

(n → R) →ₗ[R] n → R

to_lin A is matrix multiplication of vectors by A, as a linear map.

After the group structure on special_linear_group n R is defined, we show in to_linear_equiv that this gives a linear equivalence.

Equations

A.to_lin = matrix.to_lin ⇑A

theorem matrix.special_linear_group.ext_iff {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : matrix.special_linear_group n R) :

A = B ↔ ∀ (i j : n), ⇑A i j = ⇑B i j

@[ext]

theorem matrix.special_linear_group.ext {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : matrix.special_linear_group n R) (a : ∀ (i j : n), ⇑A i j = ⇑B i j) :

A = B

@[instance]

def matrix.special_linear_group.has_inv {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

has_inv (matrix.special_linear_group n R)

Equations

matrix.special_linear_group.has_inv = {inv := λ (A : matrix.special_linear_group n R), ⟨matrix.adjugate ⇑A, _⟩}

@[instance]

def matrix.special_linear_group.has_mul {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

has_mul (matrix.special_linear_group n R)

Equations

matrix.special_linear_group.has_mul = {mul := λ (A B : matrix.special_linear_group n R), ⟨A.val ⬝ B.val, _⟩}

@[instance]

def matrix.special_linear_group.has_one {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

has_one (matrix.special_linear_group n R)

Equations

matrix.special_linear_group.has_one = {one := ⟨1, _⟩}

@[instance]

def matrix.special_linear_group.inhabited {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

inhabited (matrix.special_linear_group n R)

Equations

matrix.special_linear_group.inhabited = {default := 1}

@[simp]

theorem matrix.special_linear_group.inv_val {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix.special_linear_group n R) :

↑A⁻¹ = matrix.adjugate ⇑A

@[simp]

theorem matrix.special_linear_group.inv_apply {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix.special_linear_group n R) :

⇑A⁻¹ = matrix.adjugate ⇑A

@[simp]

theorem matrix.special_linear_group.mul_val {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : matrix.special_linear_group n R) :

↑A * B = ⇑A ⬝ ⇑B

@[simp]

theorem matrix.special_linear_group.mul_apply {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : matrix.special_linear_group n R) :

⇑A * B = ⇑A ⬝ ⇑B

@[simp]

theorem matrix.special_linear_group.one_val {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

↑1 = 1

@[simp]

theorem matrix.special_linear_group.one_apply {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

⇑1 = 1

@[simp]

theorem matrix.special_linear_group.det_coe_matrix {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix.special_linear_group n R) :

matrix.det ⇑A = 1

theorem matrix.special_linear_group.det_coe_fun {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix.special_linear_group n R) :

matrix.det ⇑A = 1

@[simp]

theorem matrix.special_linear_group.to_lin_mul {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : matrix.special_linear_group n R) :

(A * B).to_lin = A.to_lin.comp B.to_lin

@[simp]

theorem matrix.special_linear_group.to_lin_one {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

1.to_lin = linear_map.id

@[instance]

def matrix.special_linear_group.group {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

group (matrix.special_linear_group n R)

Equations

matrix.special_linear_group.group = {mul := has_mul.mul matrix.special_linear_group.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, inv := has_inv.inv matrix.special_linear_group.has_inv, mul_left_inv := _}

def matrix.special_linear_group.to_linear_equiv {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix.special_linear_group n R) :

(n → R) ≃ₗ[R] n → R

to_linear_equiv A is matrix multiplication of vectors by A, as a linear equivalence.

Equations

A.to_linear_equiv = {to_fun := (matrix.to_lin ⇑A).to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑(A⁻¹.to_lin), left_inv := _, right_inv := _}

def matrix.special_linear_group.to_GL {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix.special_linear_group n R) :

linear_map.general_linear_group R (n → R)

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

Equations

A.to_GL = linear_map.general_linear_group.of_linear_equiv A.to_linear_equiv

theorem matrix.special_linear_group.coe_to_GL {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix.special_linear_group n R) :

↑(A.to_GL) = A.to_lin

@[simp]

theorem matrix.special_linear_group.to_GL_one {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

@[simp]

theorem matrix.special_linear_group.to_GL_mul {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : matrix.special_linear_group n R) :

(A * B).to_GL = (A.to_GL) * B.to_GL

def matrix.special_linear_group.embedding_GL {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

matrix.special_linear_group n R →* linear_map.general_linear_group R (n → R)

special_linear_group.embedding_GL is the embedding from special_linear_group n R to general_linear_group n R.

Equations

matrix.special_linear_group.embedding_GL = {to_fun := λ (A : matrix.special_linear_group n R), A.to_GL, map_one' := _, map_mul' := _}