The General Linear group $G L (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)ˣ

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

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

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

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

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

↑(det A) = (↑A).det

source

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

(↑g).det ≠ 0

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

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

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

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)

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 (since := "2024-11-26")]

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

source

@[simp]

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

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

↑(toLin A) 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

source

@[simp]

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

↑((map f) u) = (↑u).map ⇑f

source

@[simp]

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

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

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

map (g.comp f) = (map g).comp (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) :

((map g).comp (map f)) x = (map g) ((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) :

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

(map f) (g * h) = (map f) g * (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) :

(map f) g⁻¹ = ((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) :

det ((map f) g) = (Units.map ↑f) (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) :

(map f) g * (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) :

(map f) g⁻¹ * (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] :

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