mathlib3 documentation

linear_algebra.matrix.special_linear_group

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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.

References #

Tags #

matrix group, group, matrix inverse

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) :
( (i j : n), A i j = B i j) A = B
@[simp]
theorem matrix.special_linear_group.coe_mk {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix n n R) (h : A.det = 1) :
A, h⟩ = A
@[simp]
@[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.coe_pow {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : matrix.special_linear_group n R) (m : ) :
(A ^ m) = A ^ m
@[protected, instance]
Equations
@[protected, instance]
Equations

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

Equations

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]

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

Equations
@[protected, instance]

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

Equations
@[protected, instance]
Equations
theorem matrix.special_linear_group.SL2_inv_expl {R : Type v} [comm_ring R] (A : matrix.special_linear_group (fin 2) R) :
A⁻¹ = ![![A.val 1 1, -A.val 0 1], ![-A.val 1 0, A.val 0 0]], _⟩
theorem matrix.special_linear_group.fin_two_induction {R : Type v} [comm_ring R] (P : matrix.special_linear_group (fin 2) R Prop) (h : (a b c d : R) (hdet : a * d - b * c = 1), P matrix.of ![![a, b], ![c, d]], _⟩) (g : matrix.special_linear_group (fin 2) R) :
P g
theorem matrix.special_linear_group.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero {R : Type u_1} [field R] (g : matrix.special_linear_group (fin 2) R) (hg : g 1 0 = 0) :
(a b : R) (h : a 0), g = matrix.of ![![a, b], ![0, a⁻¹]], _⟩
@[protected, instance]

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

Equations

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.

Equations

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

Equations