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) [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_inv_det_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : GL n R) : ↑(Matrix.GeneralLinearGroup.det A)⁻¹ = Matrix.det ↑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) = Matrix.det ↑A

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

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

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 (AlgEquiv.toMulEquiv Matrix.toLinAlgEquiv')

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

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

Equations

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

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

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

Equations

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

def Matrix.GeneralLinearGroup.mkOfDetNeZero {n : Type u} [DecidableEq n] [Fintype n] {K : Type u_1} [Field K] (A : Matrix n n K) (h : Matrix.det A ≠ 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 (RingEquiv.toMulEquiv (AlgEquiv.toRingEquiv Matrix.toLinAlgEquiv'))

@[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) = Matrix.mulVecLin ↑A

@[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) : (LinearMap.GeneralLinearGroup.toLinearEquiv (Matrix.GeneralLinearGroup.toLinear A)) v = (Matrix.mulVecLin ↑A) v

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 := (_ : ↑(A * A⁻¹) = ↑1), inv_val := (_ : ↑(A⁻¹ * A) = ↑1) }

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)) : Matrix.det ↑↑A ≠ 0

instance Matrix.instNegSubtypeGeneralLinearGroupToCommRingToStrictOrderedCommRingMemSubgroupInstGroupMatrixToMonoidToMonoidWithZeroSemiringToSemiringToCommSemiringInstMembershipInstSetLikeSubgroupGLPos {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

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

@[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.instHasDistribNegSubtypeGeneralLinearGroupToCommRingToStrictOrderedCommRingMemSubgroupInstGroupMatrixToMonoidToMonoidWithZeroSemiringToSemiringToCommSemiringInstMembershipInstSetLikeSubgroupGLPosMul {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [LinearOrderedCommRing R] [Fact (Even (Fintype.card n))] : HasDistribNeg ↥(Matrix.GLPos n R)

Equations

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

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

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

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

Equations

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

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]]) (_ : Matrix.det (Matrix.of ![![a, -b], ![b, a]]) ≠ 0)