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 #

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.

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}

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

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

Equations

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

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

@[protected, 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), ⟨↑A.adjugate, _⟩}

@[protected, 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.mul B.val, _⟩}

@[protected, 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, _⟩}

@[protected, instance]

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

has_pow (matrix.special_linear_group n R) ℕ

Equations

matrix.special_linear_group.nat.has_pow = {pow := λ (x : matrix.special_linear_group n R) (n_1 : ℕ), ⟨↑x ^ n_1, _⟩}

@[protected, 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.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]

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

↑A⁻¹ = ↑A.adjugate

@[simp]

theorem matrix.special_linear_group.coe_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) = ↑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 : matrix.special_linear_group n R) :

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

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 : matrix.special_linear_group n 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 : matrix.special_linear_group n 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] :

monoid (matrix.special_linear_group n R)

Equations

matrix.special_linear_group.monoid = function.injective.monoid coe 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] :

group (matrix.special_linear_group n R)

Equations

matrix.special_linear_group.group = {mul := monoid.mul matrix.special_linear_group.monoid, mul_assoc := _, one := monoid.one matrix.special_linear_group.monoid, one_mul := _, mul_one := _, npow := monoid.npow matrix.special_linear_group.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv matrix.special_linear_group.has_inv, div := div_inv_monoid.div._default monoid.mul matrix.special_linear_group.group._proof_6 monoid.one matrix.special_linear_group.group._proof_7 matrix.special_linear_group.group._proof_8 monoid.npow matrix.special_linear_group.group._proof_9 matrix.special_linear_group.group._proof_10 has_inv.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default monoid.mul matrix.special_linear_group.group._proof_12 monoid.one matrix.special_linear_group.group._proof_13 matrix.special_linear_group.group._proof_14 monoid.npow matrix.special_linear_group.group._proof_15 matrix.special_linear_group.group._proof_16 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

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

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

Equations

matrix.special_linear_group.to_lin' = {to_fun := λ (A : matrix.special_linear_group n R), linear_equiv.of_linear (⇑matrix.to_lin' ↑A) (⇑matrix.to_lin' ↑A⁻¹) _ _, map_one' := _, map_mul' := _}

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

⇑(⇑matrix.special_linear_group.to_lin' A) v = ⇑(⇑matrix.to_lin' ↑A) v

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 : matrix.special_linear_group n R) :

↑(⇑matrix.special_linear_group.to_lin' A) = ⇑matrix.to_lin' ↑A

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

⇑((⇑matrix.special_linear_group.to_lin' A).symm) v = ⇑(⇑matrix.to_lin' ↑A⁻¹) v

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 : matrix.special_linear_group n R) :

↑((⇑matrix.special_linear_group.to_lin' A).symm) = ⇑matrix.to_lin' ↑A⁻¹

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

function.injective ⇑matrix.special_linear_group.to_lin'

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

matrix.special_linear_group.to_GL = (linear_map.general_linear_group.general_linear_equiv R (n → R)).symm.to_monoid_hom.comp matrix.special_linear_group.to_lin'

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) :

↑(⇑matrix.special_linear_group.to_GL A) = (⇑matrix.special_linear_group.to_lin' A).to_linear_map

@[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 : matrix.special_linear_group n R) :

↑(⇑(matrix.special_linear_group.map f) g) = ⇑(f.map_matrix) ↑g

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) :

matrix.special_linear_group n R →* matrix.special_linear_group n 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

matrix.special_linear_group.map f = {to_fun := λ (g : matrix.special_linear_group n R), ⟨⇑(f.map_matrix) ↑g, _⟩, map_one' := _, map_mul' := _}

@[protected, instance]

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

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

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

Equations

matrix.special_linear_group.has_coe = {coe := λ (x : matrix.special_linear_group n ℤ), ⇑(matrix.special_linear_group.map (int.cast_ring_hom R)) x}

@[simp]

theorem matrix.special_linear_group.coe_matrix_coe {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (g : matrix.special_linear_group n ℤ) :

↑↑g = ↑g.map ⇑(int.cast_ring_hom R)

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

has_neg (matrix.special_linear_group n R)

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

Equations

matrix.special_linear_group.has_neg = {neg := λ (g : matrix.special_linear_group n R), ⟨-↑g, _⟩}

@[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 : matrix.special_linear_group n 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))] :

has_distrib_neg (matrix.special_linear_group n R)

Equations

matrix.special_linear_group.has_distrib_neg = function.injective.has_distrib_neg coe matrix.special_linear_group.has_distrib_neg._proof_1 matrix.special_linear_group.has_distrib_neg._proof_2 matrix.special_linear_group.has_distrib_neg._proof_3

@[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 : matrix.special_linear_group n ℤ) :

theorem matrix.special_linear_group.SL2_inv_expl_det {R : Type v} [comm_ring R] (A : matrix.special_linear_group (fin 2) R) :

matrix.det ![![A.val 1 1, -A.val 0 1], ![-A.val 1 0, A.val 0 0]] = 1

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]

def matrix.special_linear_group.has_coe_to_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) (λ (_x : matrix.special_linear_group n R), n → n → R)

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

Equations

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

@[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 : matrix.special_linear_group n R) :

def modular_group.S :

matrix.special_linear_group (fin 2) ℤ

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

modular_group.S = ⟨⇑matrix.of ![![0, -1], ![1, 0]], modular_group.S._proof_1⟩

def modular_group.T :

matrix.special_linear_group (fin 2) ℤ

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

Equations

modular_group.T = ⟨⇑matrix.of ![![1, 1], ![0, 1]], modular_group.T._proof_1⟩

theorem modular_group.coe_S :

↑modular_group.S = ⇑matrix.of ![![0, -1], ![1, 0]]

theorem modular_group.coe_T :

↑modular_group.T = ⇑matrix.of ![![1, 1], ![0, 1]]

theorem modular_group.coe_T_inv :

↑modular_group.T ⁻¹ = ⇑matrix.of ![![1, -1], ![0, 1]]

theorem modular_group.coe_T_zpow (n : ℤ) :

↑(modular_group.T ^ n) = ⇑matrix.of ![![1, n], ![0, 1]]

@[simp]

theorem modular_group.T_pow_mul_apply_one (n : ℤ) (g : matrix.special_linear_group (fin 2) ℤ) :

↑(modular_group.T ^ n * g) 1 = ↑g 1

@[simp]

theorem modular_group.T_mul_apply_one (g : matrix.special_linear_group (fin 2) ℤ) :

↑(modular_group.T * g) 1 = ↑g 1

@[simp]

theorem modular_group.T_inv_mul_apply_one (g : matrix.special_linear_group (fin 2) ℤ) :

↑(modular_group.T ⁻¹ * g) 1 = ↑g 1