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

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

Instances For

source

def Matrix.termGL :

Lean.ParserDescr

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 => n → n → R

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

Equations

Matrix.GeneralLinearGroup.instCoeFun = { coe := fun A => ↑A }

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) = Matrix.det ↑A

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)⁻¹ = Matrix.det ↑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

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

Instances For

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

Equations

Matrix.GeneralLinearGroup.toLin = Units.mapEquiv (AlgEquiv.toMulEquiv Matrix.toLinAlgEquiv')

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 (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

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 (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

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

Instances For

source

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

source

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.

source

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

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

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

Instances For

source

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

source

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

source

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

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

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 ↑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

@[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 : { x // x ∈ Matrix.GLPos n R }) :

Matrix.det ↑↑A ≠ 0

source

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

Neg { x // x ∈ 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.

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 : { x // x ∈ 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 : { x // x ∈ 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 : { x // x ∈ Matrix.GLPos n R }) (i : n) (j : n) :

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

source

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

HasDistribNeg { x // x ∈ Matrix.GLPos n R }

Equations

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

source

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

Matrix.SpecialLinearGroup n R →* { x // x ∈ 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.

Instances For

source

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

Coe (Matrix.SpecialLinearGroup n R) { x // x ∈ Matrix.GLPos n R }

Equations

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

source

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

Function.Injective ↑Matrix.SpecialLinearGroup.toGLPos

source

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

source

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

source

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

source

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

source

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)

Instances For