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

source

@[reducible, inline]

abbrev Matrix.GeneralLinearGroup (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [CommRing R] :

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

GL n R = (Matrix n n R)ˣ

Instances For

source

def Matrix.termGL :

Lean.ParserDescr

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

Equations

Matrix.termGL = Lean.ParserDescr.node `Matrix.termGL 1024 (Lean.ParserDescr.symbol "GL")

Instances For

source

instance Matrix.GeneralLinearGroup.instCoeFun {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :

CoeFun (GL n R) fun (x : GL n R) => n → n → R

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

Equations

Matrix.GeneralLinearGroup.instCoeFun = { coe := fun (A : GL n R) => ↑A }

source

def Matrix.GeneralLinearGroup.det {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :

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

source

@[simp]

theorem Matrix.GeneralLinearGroup.val_inv_det_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) :

↑(Matrix.GeneralLinearGroup.det A)⁻¹ = (↑A⁻¹).det

source

@[simp]

theorem Matrix.GeneralLinearGroup.val_det_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) :

↑(Matrix.GeneralLinearGroup.det A) = (↑A).det

source

def Matrix.GeneralLinearGroup.toLin {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :

GL n R ≃* LinearMap.GeneralLinearGroup R (n → R)

The groups GL n R (notation for Matrix.GeneralLinearGroup n R) and LinearMap.GeneralLinearGroup R (n → R) are multiplicatively equivalent

Equations

Matrix.GeneralLinearGroup.toLin = Units.mapEquiv Matrix.toLinAlgEquiv'.toMulEquiv

Instances For

source

def Matrix.GeneralLinearGroup.mk' {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) :

Invertible A.det → GL n R

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

Equations

Matrix.GeneralLinearGroup.mk' A x = A.unitOfDetInvertible

Instances For

source

noncomputable def Matrix.GeneralLinearGroup.mk'' {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (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

Matrix.GeneralLinearGroup.mk'' A h = A.nonsingInvUnit h

Instances For

source

def Matrix.GeneralLinearGroup.mkOfDetNeZero {n : Type u} [DecidableEq n] [Fintype n] {K : Type u_1} [Field K] (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

Matrix.GeneralLinearGroup.mkOfDetNeZero A h = Matrix.GeneralLinearGroup.mk' A (invertibleOfNonzero h)

Instances For

source

theorem Matrix.GeneralLinearGroup.ext_iff {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A B : GL n R) :

A = B ↔ ∀ (i j : n), ↑A i j = ↑B i j

source

theorem Matrix.GeneralLinearGroup.ext {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] ⦃A 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.

source

@[simp]

theorem Matrix.GeneralLinearGroup.coe_mul {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A B : GL n R) :

↑(A * B) = ↑A * ↑B

source

@[simp]

theorem Matrix.GeneralLinearGroup.coe_one {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :

↑1 = 1

source

theorem Matrix.GeneralLinearGroup.coe_inv {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) :

↑A⁻¹ = (↑A)⁻¹

source

@[deprecated Matrix.GeneralLinearGroup.toLin]

def Matrix.GeneralLinearGroup.toLinear {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :

GL n R ≃* LinearMap.GeneralLinearGroup R (n → R)

Alias of Matrix.GeneralLinearGroup.toLin.

The groups GL n R (notation for Matrix.GeneralLinearGroup n R) and LinearMap.GeneralLinearGroup R (n → R) are multiplicatively equivalent

Equations

@Matrix.GeneralLinearGroup.toLinear = @Matrix.GeneralLinearGroup.toLin

Instances For

source

@[simp]

theorem Matrix.GeneralLinearGroup.coe_toLin {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) :

↑(Matrix.GeneralLinearGroup.toLin A) = (↑A).mulVecLin

source

@[simp]

theorem Matrix.GeneralLinearGroup.toLin_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) (v : n → R) :

(Matrix.GeneralLinearGroup.toLin A).toLinearEquiv v = (↑A).mulVecLin v

source

def Matrix.GeneralLinearGroup.map {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) :

GL n R →* GL n S

A ring homomorphism f : R →+* S induces a homomorphism GLₙ(f) : GLₙ(R) →* GLₙ(S).

Equations

Matrix.GeneralLinearGroup.map f = Units.map ↑f.mapMatrix

Instances For

source

@[simp]

theorem Matrix.GeneralLinearGroup.map_id {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :

Matrix.GeneralLinearGroup.map (RingHom.id R) = MonoidHom.id (GL n R)

source

@[simp]

theorem Matrix.GeneralLinearGroup.map_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (i j : n) (g : GL n R) :

↑((Matrix.GeneralLinearGroup.map f) g) i j = f (↑g i j)

source

@[simp]

theorem Matrix.GeneralLinearGroup.map_comp {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} {T : Type u_2} [CommRing S] [CommRing T] (f : T →+* R) (g : R →+* S) :

Matrix.GeneralLinearGroup.map (g.comp f) = (Matrix.GeneralLinearGroup.map g).comp (Matrix.GeneralLinearGroup.map f)

source

@[simp]

theorem Matrix.GeneralLinearGroup.map_comp_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} {T : Type u_2} [CommRing S] [CommRing T] (f : T →+* R) (g : R →+* S) (x : GL n T) :

((Matrix.GeneralLinearGroup.map g).comp (Matrix.GeneralLinearGroup.map f)) x = (Matrix.GeneralLinearGroup.map g) ((Matrix.GeneralLinearGroup.map f) x)

source

@[simp]

theorem Matrix.GeneralLinearGroup.map_one {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) :

(Matrix.GeneralLinearGroup.map f) 1 = 1

source

theorem Matrix.GeneralLinearGroup.map_mul {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g h : GL n R) :

(Matrix.GeneralLinearGroup.map f) (g * h) = (Matrix.GeneralLinearGroup.map f) g * (Matrix.GeneralLinearGroup.map f) h

source

theorem Matrix.GeneralLinearGroup.map_inv {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) :

(Matrix.GeneralLinearGroup.map f) g⁻¹ = ((Matrix.GeneralLinearGroup.map f) g)⁻¹

source

theorem Matrix.GeneralLinearGroup.map_det {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) :

Matrix.GeneralLinearGroup.det ((Matrix.GeneralLinearGroup.map f) g) = (Units.map ↑f) (Matrix.GeneralLinearGroup.det g)

source

theorem Matrix.GeneralLinearGroup.map_mul_map_inv {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) :

(Matrix.GeneralLinearGroup.map f) g * (Matrix.GeneralLinearGroup.map f) g⁻¹ = 1

source

theorem Matrix.GeneralLinearGroup.map_inv_mul_map {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) :

(Matrix.GeneralLinearGroup.map f) g⁻¹ * (Matrix.GeneralLinearGroup.map f) g = 1

source

@[simp]

theorem Matrix.GeneralLinearGroup.coe_map_mul_map_inv {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) :

(↑g).map ⇑f * (↑g)⁻¹.map ⇑f = 1

source

@[simp]

theorem Matrix.GeneralLinearGroup.coe_map_inv_mul_map {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) :

(↑g)⁻¹.map ⇑f * (↑g).map ⇑f = 1

source

def Matrix.SpecialLinearGroup.toGL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :

Matrix.SpecialLinearGroup n R →* GL n R

toGL is the map from the special linear group to the general linear group.

Equations

Matrix.SpecialLinearGroup.toGL = { toFun := fun (A : Matrix.SpecialLinearGroup n R) => { val := ↑A, inv := ↑A⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

@[deprecated Matrix.SpecialLinearGroup.toGL]

def Matrix.SpecialLinearGroup.coeToGL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :

Matrix.SpecialLinearGroup n R →* GL n R

Alias of Matrix.SpecialLinearGroup.toGL.

toGL is the map from the special linear group to the general linear group.

Equations

@Matrix.SpecialLinearGroup.coeToGL = @Matrix.SpecialLinearGroup.toGL

Instances For

source

instance Matrix.SpecialLinearGroup.hasCoeToGeneralLinearGroup {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] :

Coe (Matrix.SpecialLinearGroup n R) (GL n R)

Equations

Matrix.SpecialLinearGroup.hasCoeToGeneralLinearGroup = { coe := ⇑Matrix.SpecialLinearGroup.toGL }

source

@[simp]

theorem Matrix.SpecialLinearGroup.coeToGL_det {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (g : Matrix.SpecialLinearGroup n R) :

Matrix.GeneralLinearGroup.det (Matrix.SpecialLinearGroup.toGL g) = 1

source

def Matrix.GLPos (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] :

Subgroup (GL n R)

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

Equations

Matrix.GLPos n R = Subgroup.comap Matrix.GeneralLinearGroup.det (Units.posSubgroup R)

Instances For

source

def MatrixGroups.«termGL(_,_)⁺» :

Lean.ParserDescr

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Matrix.mem_glpos {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] (A : GL n R) :

A ∈ Matrix.GLPos n R ↔ 0 < ↑(Matrix.GeneralLinearGroup.det A)

source

theorem Matrix.GLPos.det_ne_zero {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] (A : ↥(Matrix.GLPos n R)) :

(↑↑A).det ≠ 0

source

instance Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] :

Neg ↥(Matrix.GLPos n R)

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

Equations

Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos = { neg := fun (g : ↥(Matrix.GLPos n R)) => ⟨-↑g, ⋯⟩ }

source

@[simp]

theorem Matrix.GLPos.coe_neg_GL {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] (g : ↥(Matrix.GLPos n R)) :

↑(-g) = -↑g

source

@[simp]

theorem Matrix.GLPos.coe_neg {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] (g : ↥(Matrix.GLPos n R)) :

↑↑(-g) = -↑↑g

source

@[simp]

theorem Matrix.GLPos.coe_neg_apply {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] (g : ↥(Matrix.GLPos n R)) (i j : n) :

↑↑(-g) i j = -↑↑g i j

source

instance Matrix.instHasDistribNegSubtypeGeneralLinearGroupMemSubgroupGLPos {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] :

HasDistribNeg ↥(Matrix.GLPos n R)

Equations

Matrix.instHasDistribNegSubtypeGeneralLinearGroupMemSubgroupGLPos = Function.Injective.hasDistribNeg (fun (a : ↥(Matrix.GLPos n R)) => ↑a) ⋯ ⋯ ⋯

source

def Matrix.SpecialLinearGroup.toGLPos {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] :

Matrix.SpecialLinearGroup n R →* ↥(Matrix.GLPos n R)

Matrix.SpecialLinearGroup n R embeds into GL_pos n R

Equations

Matrix.SpecialLinearGroup.toGLPos = { toFun := fun (A : Matrix.SpecialLinearGroup n R) => ⟨Matrix.SpecialLinearGroup.toGL A, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }