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 1matrix.special_linear_group.group
gives the group structure (under multiplication)matrix.special_linear_group.to_GL
is the embeddingSLₙ(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 #
Tags #
matrix group, group, matrix inverse
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
- matrix.special_linear_group.has_coe_to_matrix
- matrix.special_linear_group.has_inv
- matrix.special_linear_group.has_mul
- matrix.special_linear_group.has_one
- matrix.special_linear_group.nat.has_pow
- matrix.special_linear_group.inhabited
- matrix.special_linear_group.monoid
- matrix.special_linear_group.group
- matrix.special_linear_group.has_coe
- matrix.special_linear_group.has_neg
- matrix.special_linear_group.has_distrib_neg
- matrix.special_linear_group.has_coe_to_fun
- matrix.special_linear_group.has_coe_to_general_linear_group
- matrix.special_linear_group.matrix.GL_pos.has_coe
- upper_half_plane.SL_action
- upper_half_plane.matrix.GL_pos.has_coe
- upper_half_plane.SL_on_GL_pos
- upper_half_plane.SL_to_GL_tower
- upper_half_plane.subgroup_SL
- upper_half_plane.subgroup_to_SL_tower
- modular_forms.SL_action
Equations
- matrix.special_linear_group.has_coe_to_matrix = {coe := λ (A : matrix.special_linear_group n R), A.val}
Equations
- matrix.special_linear_group.has_inv = {inv := λ (A : matrix.special_linear_group n R), ⟨↑A.adjugate, _⟩}
Equations
- matrix.special_linear_group.has_mul = {mul := λ (A B : matrix.special_linear_group n R), ⟨A.val.mul B.val, _⟩}
Equations
- matrix.special_linear_group.has_one = {one := ⟨1, _⟩}
Equations
- matrix.special_linear_group.nat.has_pow = {pow := λ (x : matrix.special_linear_group n R) (n_1 : ℕ), ⟨↑x ^ n_1, _⟩}
Equations
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
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 := _}
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' := _}
to_GL
is the map from the special linear group to the general linear group
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' := _}
Coercion of SL n
ℤ
to SL n
R
for a commutative ring R
.
Equations
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, _⟩}
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
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}