# 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, consisting of all square R-matrices with determinant 1 on the fintype n by n. 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).

## 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.to_GL 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 matrix_groups.

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

We provide matrix.special_linear_group.has_coe_to_fun for convenience, but do not state any lemmas about it, and use matrix.special_linear_group.coe_fn_eq_coe to eliminate it ⇑ in favor of a regular ↑ coercion.

## 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
Instances for matrix.special_linear_group
@[protected, instance]
def matrix.special_linear_group.has_coe_to_matrix {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
(matrix n n R)
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
@[protected, instance]
def matrix.special_linear_group.has_inv {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
Equations
@[protected, instance]
def matrix.special_linear_group.has_mul {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
Equations
@[protected, instance]
def matrix.special_linear_group.has_one {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
Equations
@[protected, instance]
def matrix.special_linear_group.nat.has_pow {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
Equations
@[protected, 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.coe_mk {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : n R) (h : A.det = 1) :
A, h⟩ = A
@[simp]
theorem matrix.special_linear_group.coe_inv {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : R) :
@[simp]
theorem matrix.special_linear_group.coe_mul {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : R) :
(A * B) = A.mul B
@[simp]
theorem matrix.special_linear_group.coe_one {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
1 = 1
@[simp]
theorem matrix.special_linear_group.det_coe {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : R) :
A.det = 1
@[simp]
theorem matrix.special_linear_group.coe_pow {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : R) (m : ) :
(A ^ m) = A ^ m
theorem matrix.special_linear_group.det_ne_zero {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] [nontrivial R] (g : R) :
theorem matrix.special_linear_group.row_ne_zero {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] [nontrivial R] (g : R) (i : n) :
g i 0
@[protected, instance]
def matrix.special_linear_group.monoid {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
Equations
• matrix.special_linear_group.monoid = matrix.special_linear_group.monoid._proof_1 matrix.special_linear_group.monoid._proof_2 matrix.special_linear_group.monoid._proof_3 matrix.special_linear_group.monoid._proof_4
@[protected, 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_lin' {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
→* (n → R) ≃ₗ[R] n → R

A version of matrix.to_lin' A that produces linear equivalences.

Equations
theorem matrix.special_linear_group.to_lin'_apply {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : R) (v : n → R) :
theorem matrix.special_linear_group.to_lin'_to_linear_map {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : R) :
theorem matrix.special_linear_group.to_lin'_symm_apply {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : R) (v : n → R) :
theorem matrix.special_linear_group.to_lin'_symm_to_linear_map {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : R) :
theorem matrix.special_linear_group.to_lin'_injective {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
def matrix.special_linear_group.to_GL {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring 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.map_apply_coe {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] {S : Type u_1} [comm_ring S] (f : R →+* S) (g : R) :
def matrix.special_linear_group.map {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] {S : Type u_1} [comm_ring S] (f : R →+* S) :

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

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

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

Equations
@[simp]
theorem matrix.special_linear_group.coe_matrix_coe {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (g : ) :
@[protected, instance]
def matrix.special_linear_group.has_neg {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] [fact (even (fintype.card n))] :

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

Equations
@[simp]
theorem matrix.special_linear_group.coe_neg {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] [fact (even (fintype.card n))] (g : R) :
@[protected, instance]
def matrix.special_linear_group.has_distrib_neg {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] [fact (even (fintype.card n))] :
Equations
@[simp]
theorem matrix.special_linear_group.coe_int_neg {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] [fact (even (fintype.card n))] (g : ) :
@[protected, instance]
def matrix.special_linear_group.has_coe_to_fun {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
(λ (_x : , n → n → R)

This instance is here for convenience, but is not the simp-normal form.

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