# Documentation

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup

# 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

@[inline, reducible]
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

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

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

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

The determinant of a unit matrix is itself a unit.

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

Instances For
def Matrix.GeneralLinearGroup.mk' {n : Type u} [] [] {R : Type v} [] (A : Matrix n n R) :
GL n R

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

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

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

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

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

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.

Instances For
@[simp]
theorem Matrix.GeneralLinearGroup.coe_toLinear {n : Type u} [] [] {R : Type v} [] (A : GL n R) :
↑(Matrix.GeneralLinearGroup.toLinear A) =
@[simp]
theorem Matrix.GeneralLinearGroup.toLinear_apply {n : Type u} [] [] {R : Type v} [] (A : GL n R) (v : nR) :
↑(LinearMap.GeneralLinearGroup.toLinearEquiv (Matrix.GeneralLinearGroup.toLinear A)) v = ↑() 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.

Instances For
instance Matrix.SpecialLinearGroup.hasCoeToGeneralLinearGroup {n : Type u} [] [] {R : Type v} [] :
Coe () (GL n R)
@[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.

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 : { x // x }) :
Matrix.det A 0

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

@[simp]
theorem Matrix.GLPos.coe_neg_GL {n : Type u} {R : Type v} [] [] [Fact (Even ())] (g : { x // x }) :
↑(-g) = -g
@[simp]
theorem Matrix.GLPos.coe_neg {n : Type u} {R : Type v} [] [] [Fact (Even ())] (g : { x // x }) :
↑(-g) = -g
@[simp]
theorem Matrix.GLPos.coe_neg_apply {n : Type u} {R : Type v} [] [] [Fact (Even ())] (g : { x // x }) (i : n) (j : n) :
↑(-g) i j = -g i j
def Matrix.SpecialLinearGroup.toGLPos {n : Type u} [] [] {R : Type v} :
→* { x // x }

Matrix.SpecialLinearGroup n R embeds into GL_pos n R

Instances For
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.

Instances For