The Special Linear group $SL(n, R)$ #
This file defines the elements of the Special Linear group SpecialLinearGroup 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 SpecialLinearGroup n R
and the embedding into the general linear group
GeneralLinearGroup R (n → R)
.
Main definitions #
Matrix.SpecialLinearGroup
is the type of matrices with determinant 1Matrix.SpecialLinearGroup.group
gives the group structure (under multiplication)Matrix.SpecialLinearGroup.toGL
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 MatrixGroups
.
Implementation notes #
The inverse operation in the SpecialLinearGroup
is defined to be the adjugate
matrix, so that SpecialLinearGroup n R
has a group structure for all CommRing R
.
We define the elements of SpecialLinearGroup
to be matrices, since we need to
compute their determinant. This is in contrast with GeneralLinearGroup R M
,
which consists of invertible R
-linear maps on M
.
We provide Matrix.SpecialLinearGroup.hasCoeToFun
for convenience, but do not state any
lemmas about it, and use Matrix.SpecialLinearGroup.coeFn_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
SpecialLinearGroup n R
is the group of n
by n
R
-matrices with determinant equal to 1.
Instances For
This instance is here for convenience, but is literally the same as the coercion from
hasCoeToMatrix
.
A version of Matrix.toLin' A
that produces linear equivalences.
Instances For
toGL
is the map from the special linear group to the general linear group
Instances For
A ring homomorphism from R
to S
induces a group homomorphism from
SpecialLinearGroup n R
to SpecialLinearGroup n S
.
Instances For
Coercion of SL n
ℤ
to SL n
R
for a commutative ring R
.
Formal operation of negation on special linear group on even cardinality n
given by negating
each element.
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.
Instances For
The matrix T = [[1, 1], [0, 1]]
as an element of SL(2, ℤ)