# The General Linear group $GL(n, R)$ #

This file defines the elements of the General Linear group Matrix.GeneralLinearGroup n R, consisting of all invertible n by n R-matrices.

## Main definitions #

• Matrix.GeneralLinearGroup is the type of matrices over R which are units in the matrix ring.
• Matrix.GLPos gives the subgroup of matrices with positive determinant (over a linear ordered ring).

## Tags #

matrix group, group, matrix inverse

@[reducible, inline]
abbrev Matrix.GeneralLinearGroup (n : Type u) (R : Type v) [] [] [] :
Type (max v u)

GL n R is the group of n by n R-matrices with unit determinant. Defined as a subtype of matrices

Equations
Instances For

GL n R is the group of n by n R-matrices with unit determinant. Defined as a subtype of matrices

Equations
Instances For
instance Matrix.GeneralLinearGroup.instCoeFun {n : Type u} [] [] {R : Type v} [] :
CoeFun (GL n R) fun (x : GL n R) => nnR

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

Equations
• Matrix.GeneralLinearGroup.instCoeFun = { coe := fun (A : GL n R) => A }
@[simp]
theorem Matrix.GeneralLinearGroup.val_inv_det_apply {n : Type u} [] [] {R : Type v} [] (A : GL n R) :
(Matrix.GeneralLinearGroup.det A)⁻¹ = (A⁻¹).det
@[simp]
theorem Matrix.GeneralLinearGroup.val_det_apply {n : Type u} [] [] {R : Type v} [] (A : GL n R) :
(Matrix.GeneralLinearGroup.det A) = (A).det
def Matrix.GeneralLinearGroup.det {n : Type u} [] [] {R : Type v} [] :
GL n R →* Rˣ

The determinant of a unit matrix is itself a unit.

Equations
• Matrix.GeneralLinearGroup.det = { toFun := fun (A : GL n R) => { val := (A).det, inv := (A⁻¹).det, val_inv := , inv_val := }, map_one' := , map_mul' := }
Instances For
def Matrix.GeneralLinearGroup.toLin {n : Type u} [] [] {R : Type v} [] :

The GL n R and Matrix.GeneralLinearGroup R n groups are multiplicatively equivalent

Equations
• Matrix.GeneralLinearGroup.toLin = Units.mapEquiv Matrix.toLinAlgEquiv'.toMulEquiv
Instances For
def Matrix.GeneralLinearGroup.mk' {n : Type u} [] [] {R : Type v} [] (A : Matrix n n R) :
Invertible A.detGL n R

Given a matrix with invertible determinant we get an element of GL n R

Equations
• = A.unitOfDetInvertible
Instances For
noncomputable def Matrix.GeneralLinearGroup.mk'' {n : Type u} [] [] {R : Type v} [] (A : Matrix n n R) (h : IsUnit A.det) :
GL n R

Given a matrix with unit determinant we get an element of GL n R

Equations
• = A.nonsingInvUnit h
Instances For
def Matrix.GeneralLinearGroup.mkOfDetNeZero {n : Type u} [] [] {K : Type u_1} [] (A : Matrix n n K) (h : A.det 0) :
GL n K

Given a matrix with non-zero determinant over a field, we get an element of GL n K

Equations
Instances For
theorem Matrix.GeneralLinearGroup.ext_iff {n : Type u} [] [] {R : Type v} [] (A : GL n R) (B : GL n R) :
A = B ∀ (i j : n), A i j = B i j
theorem Matrix.GeneralLinearGroup.ext {n : Type u} [] [] {R : Type v} [] ⦃A : GL n R ⦃B : GL n R (h : ∀ (i j : n), A i j = B i j) :
A = B

Not marked @[ext] as the ext tactic already solves this.

@[simp]
theorem Matrix.GeneralLinearGroup.coe_mul {n : Type u} [] [] {R : Type v} [] (A : GL n R) (B : GL n R) :
(A * B) = A * B
@[simp]
theorem Matrix.GeneralLinearGroup.coe_one {n : Type u} [] [] {R : Type v} [] :
1 = 1
theorem Matrix.GeneralLinearGroup.coe_inv {n : Type u} [] [] {R : Type v} [] (A : GL n R) :
A⁻¹ = (A)⁻¹
def Matrix.GeneralLinearGroup.toLinear {n : Type u} [] [] {R : Type v} [] :

An element of the matrix general linear group on (n) [Fintype n] can be considered as an element of the endomorphism general linear group on n → R.

Equations
• Matrix.GeneralLinearGroup.toLinear = Units.mapEquiv Matrix.toLinAlgEquiv'.toRingEquiv.toMulEquiv
Instances For
@[simp]
theorem Matrix.GeneralLinearGroup.coe_toLinear {n : Type u} [] [] {R : Type v} [] (A : GL n R) :
(Matrix.GeneralLinearGroup.toLinear A) = (A).mulVecLin
@[simp]
theorem Matrix.GeneralLinearGroup.toLinear_apply {n : Type u} [] [] {R : Type v} [] (A : GL n R) (v : nR) :
(Matrix.GeneralLinearGroup.toLinear A).toLinearEquiv v = (A).mulVecLin v
def Matrix.SpecialLinearGroup.coeToGL {n : Type u} [] [] {R : Type v} [] (A : ) :
GL n R

The map from SL(n) to GL(n) underlying the coercion, forgetting the value of the determinant.

Equations
• A = { val := A, inv := A⁻¹, val_inv := , inv_val := }
Instances For
instance Matrix.SpecialLinearGroup.hasCoeToGeneralLinearGroup {n : Type u} [] [] {R : Type v} [] :
Coe (GL n R)
Equations
• Matrix.SpecialLinearGroup.hasCoeToGeneralLinearGroup = { coe := Matrix.SpecialLinearGroup.coeToGL }
@[simp]
theorem Matrix.SpecialLinearGroup.coeToGL_det {n : Type u} [] [] {R : Type v} [] (g : ) :
Matrix.GeneralLinearGroup.det g = 1
def Matrix.GLPos (n : Type u) (R : Type v) [] [] :
Subgroup (GL n R)

This is the subgroup of nxn matrices with entries over a linear ordered ring and positive determinant.

Equations
Instances For
@[simp]
theorem Matrix.mem_glpos {n : Type u} {R : Type v} [] [] (A : GL n R) :
A 0 < (Matrix.GeneralLinearGroup.det A)
theorem Matrix.GLPos.det_ne_zero {n : Type u} {R : Type v} [] [] (A : ()) :
(A).det 0
instance Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos {n : Type u} {R : Type v} [] [] [Fact (Even ())] :
Neg ()

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

Equations
• Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos = { neg := fun (g : ()) => -g, }
@[simp]
theorem Matrix.GLPos.coe_neg_GL {n : Type u} {R : Type v} [] [] [Fact (Even ())] (g : ()) :
(-g) = -g
@[simp]
theorem Matrix.GLPos.coe_neg {n : Type u} {R : Type v} [] [] [Fact (Even ())] (g : ()) :
(-g) = -g
@[simp]
theorem Matrix.GLPos.coe_neg_apply {n : Type u} {R : Type v} [] [] [Fact (Even ())] (g : ()) (i : n) (j : n) :
(-g) i j = -g i j
Equations
def Matrix.SpecialLinearGroup.toGLPos {n : Type u} [] [] {R : Type v} :
→* ()

Matrix.SpecialLinearGroup n R embeds into GL_pos n R

Equations
• Matrix.SpecialLinearGroup.toGLPos = { toFun := fun (A : ) => A, , map_one' := , map_mul' := }
Instances For
Equations
• Matrix.SpecialLinearGroup.instCoeSubtypeGeneralLinearGroupMemSubgroupGLPos = { coe := Matrix.SpecialLinearGroup.toGLPos }
theorem Matrix.SpecialLinearGroup.toGLPos_injective {n : Type u} [] [] {R : Type v} :
Function.Injective Matrix.SpecialLinearGroup.toGLPos
@[simp]
theorem Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix {n : Type u} [] [] {R : Type v} (g : ) :
(Matrix.SpecialLinearGroup.toGLPos g) = g

Coercing a Matrix.SpecialLinearGroup via GL_pos and GL is the same as coercing straight to a matrix.

@[simp]
theorem Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det {n : Type u} [] [] {R : Type v} (g : ) :
Matrix.GeneralLinearGroup.det (Matrix.SpecialLinearGroup.toGLPos g) = 1
theorem Matrix.SpecialLinearGroup.coe_GLPos_neg {n : Type u} [] [] {R : Type v} [Fact (Even ())] (g : ) :
Matrix.SpecialLinearGroup.toGLPos (-g) = -Matrix.SpecialLinearGroup.toGLPos g
@[simp]
theorem Matrix.val_planeConformalMatrix {R : Type u_1} [] (a : R) (b : R) (hab : a ^ 2 + b ^ 2 0) :
() = Matrix.of ![![a, -b], ![b, a]]
def Matrix.planeConformalMatrix {R : Type u_1} [] (a : R) (b : R) (hab : a ^ 2 + b ^ 2 0) :
GL (Fin 2) R

The matrix [a, -b; b, a] (inspired by multiplication by a complex number); it is an element of $GL_2(R)$ if a ^ 2 + b ^ 2 is nonzero.

Equations
Instances For