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_groupis the type of matrices with determinant 1matrix.special_linear_group.groupgives the group structure (under multiplication)matrix.special_linear_group.embedding_GLis the embeddingSLₙ(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] :
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] :
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) :
@[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) :
@[instance]
def
matrix.special_linear_group.has_inv
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring 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] :
Equations
- matrix.special_linear_group.has_mul = {mul := λ (A B : matrix.special_linear_group n R), ⟨A.val.mul B.val, _⟩}
@[instance]
def
matrix.special_linear_group.has_one
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring 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] :
Equations
@[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) :
@[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) :
@[simp]
theorem
matrix.special_linear_group.one_val
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R] :
@[simp]
theorem
matrix.special_linear_group.one_apply
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R] :
@[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) :
@[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
- 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] :
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.
def
matrix.special_linear_group.to_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)
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 : matrix.special_linear_group n R) :
@[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) :
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' := _}