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) [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)ˣ

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")

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 }

@[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

@[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

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' := ⋯ }

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 GL n R and Matrix.GeneralLinearGroup R n groups are multiplicatively equivalent

Equations

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

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

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

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)

theorem Matrix.GeneralLinearGroup.ext_iff {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (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} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] ⦃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} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) (B : GL n R) : ↑(A * B) = ↑A * ↑B

@[simp]

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

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

def Matrix.GeneralLinearGroup.toLinear {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : GL n R ≃* LinearMap.GeneralLinearGroup R (n → R)

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

@[simp]

theorem Matrix.GeneralLinearGroup.coe_toLinear {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) : ↑(Matrix.GeneralLinearGroup.toLinear A) = (↑A).mulVecLin

@[simp]

theorem Matrix.GeneralLinearGroup.toLinear_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) (v : n → R) : (Matrix.GeneralLinearGroup.toLinear A).toLinearEquiv v = (↑A).mulVecLin v

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

@[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)

@[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)

@[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)

def Matrix.SpecialLinearGroup.coeToGL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix.SpecialLinearGroup n R) : 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 := ⋯ }

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.coeToGL }

@[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 ↑g = 1

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)

@[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)

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

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, ⋯⟩ }

@[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

@[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

@[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 : n) (j : n) : ↑↑(-g) i j = -↑↑g i j

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) ⋯ ⋯ ⋯

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) => ⟨↑A, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

instance Matrix.SpecialLinearGroup.instCoeSubtypeGeneralLinearGroupMemSubgroupGLPos {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] : Coe (Matrix.SpecialLinearGroup n R) ↥(Matrix.GLPos n R)

Equations

• Matrix.SpecialLinearGroup.instCoeSubtypeGeneralLinearGroupMemSubgroupGLPos = { coe := ⇑Matrix.SpecialLinearGroup.toGLPos }

theorem Matrix.SpecialLinearGroup.toGLPos_injective {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] : Function.Injective ⇑Matrix.SpecialLinearGroup.toGLPos

@[simp]

theorem Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] (g : Matrix.SpecialLinearGroup n R) : ↑↑(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} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] (g : Matrix.SpecialLinearGroup n R) : Matrix.GeneralLinearGroup.det ↑(Matrix.SpecialLinearGroup.toGLPos g) = 1

theorem Matrix.SpecialLinearGroup.coe_GLPos_neg {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] (g : Matrix.SpecialLinearGroup n R) : Matrix.SpecialLinearGroup.toGLPos (-g) = -Matrix.SpecialLinearGroup.toGLPos g

@[simp]

theorem Matrix.val_planeConformalMatrix {R : Type u_1} [Field R] (a : R) (b : R) (hab : a ^ 2 + b ^ 2 ≠ 0) : ↑(Matrix.planeConformalMatrix a b hab) = Matrix.of ![![a, -b], ![b, a]]

def Matrix.planeConformalMatrix {R : Type u_1} [Field R] (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

• Matrix.planeConformalMatrix a b hab = Matrix.GeneralLinearGroup.mkOfDetNeZero (Matrix.of ![![a, -b], ![b, a]]) ⋯