# mathlibdocumentation

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
@[instance]
def matrix.special_linear_group.coe_matrix {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
(matrix n n R)

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

Equations
def matrix.special_linear_group.to_lin' {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring 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
theorem matrix.special_linear_group.ext_iff {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : 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 : R) :
(∀ (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] :

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

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

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

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

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

@[simp]
theorem matrix.special_linear_group.mul_val {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : 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 : 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 : R) :
= 1

theorem matrix.special_linear_group.det_coe_fun {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : R) :
= 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 : R) :

@[simp]
theorem matrix.special_linear_group.to_lin'_one {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :

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

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

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

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

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

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

@[simp]
theorem matrix.special_linear_group.to_GL_one {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
1.to_GL = 1

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

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

Equations