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] [Semiring 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")

def Matrix.GeneralLinearGroup.scalar (n : Type u) [DecidableEq n] [Fintype n] {R : Type v} [Semiring R] : Rˣ →* GL n R

Scalar matrix as an element of GL n R.

Equations

• Matrix.GeneralLinearGroup.scalar n = Units.map ↑(Matrix.scalar n)

@[instance_reducible]

instance Matrix.GeneralLinearGroup.instCoeFun {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [Semiring R] : CoeFun (GL n R) fun (x : GL n R) => n → n → R

Equations

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

@[simp]

theorem Matrix.GeneralLinearGroup.coe_scalar {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [Semiring R] (u : Rˣ) : ↑((scalar n) u) = (Matrix.scalar n) ↑u

@[instance_reducible]

instance Matrix.GeneralLinearGroup.instSMul {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {m : Type u_1} : SMul (GL n R) (Matrix n m R)

Equations

• Matrix.GeneralLinearGroup.instSMul = { smul := fun (g : GL n R) (A : Matrix n m R) => ↑g * A }

@[simp]

theorem Matrix.GeneralLinearGroup.smul_def {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {m : Type u_1} (g : GL n R) (A : Matrix n m R) : g • A = ↑g * A

@[instance_reducible]

instance Matrix.GeneralLinearGroup.instDistribMulAction {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {m : Type u_2} : DistribMulAction (GL n R) (Matrix n m R)

Equations

• Matrix.GeneralLinearGroup.instDistribMulAction = { smul := fun (g : GL n R) (A : Matrix n m R) => ↑g * A, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

theorem Matrix.GeneralLinearGroup.scalar_commute {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (u : Rˣ) (A : GL n R) : (scalar n) u * A = A * (scalar n) u

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

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

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

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

@[simp]

theorem Matrix.GeneralLinearGroup.det_scalar {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (u : Rˣ) : det ((scalar n) u) = u ^ Fintype.card n

theorem Matrix.GeneralLinearGroup.det_surjective {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [Nonempty n] : Function.Surjective ⇑det

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

noncomputable def Matrix.GeneralLinearGroup.toLin' {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {V : Type u_1} [AddCommGroup V] [Module R V] (b : Module.Basis n R V) : GL n R ≃* LinearMap.GeneralLinearGroup R V

The isomorphism from GL n R to the general linear group of a module associated with a basis.

Equations

• Matrix.GeneralLinearGroup.toLin' b = Matrix.GeneralLinearGroup.toLin.trans (LinearMap.GeneralLinearGroup.congrLinearEquiv b.equivFun.symm)

theorem Matrix.GeneralLinearGroup.toLin'_apply {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {V : Type u_1} [AddCommGroup V] [Module R V] (b : Module.Basis n R V) (M : GL n R) (v : V) : ((toLin' b) M).toLinearEquiv v = (Fintype.linearCombination R ⇑b) ((↑M).mulVec ⇑(b.repr v))

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

@[simp]

theorem Matrix.GeneralLinearGroup.val_mk' {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) (x✝ : Invertible A.det) : ↑(mk' A x✝) = 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 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

@[simp]

theorem Matrix.GeneralLinearGroup.val_mk'' {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : Matrix n n R) (h : IsUnit A.det) : ↑(mk'' A h) = A

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)

@[simp]

theorem Matrix.GeneralLinearGroup.val_mkOfDetNeZero {n : Type u} [DecidableEq n] [Fintype n] {K : Type u_1} [Field K] (A : Matrix n n K) (h : A.det ≠ 0) : ↑(mkOfDetNeZero A h) = A

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

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.

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

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

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

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

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

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

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

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

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

def Matrix.GeneralLinearGroup.mapEquiv (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

The equivalence between GL n R and GL n S given by f : R ≃+* S.

Equations

• Matrix.GeneralLinearGroup.mapEquiv n f = Units.mapEquiv f.mapMatrix.toMulEquiv

@[simp]

theorem Matrix.GeneralLinearGroup.coe_mapEquiv_apply (n : Type u) [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R ≃+* S) (a : GL n R) : ↑((mapEquiv n f) a) = f.mapMatrix ↑a

@[simp]

theorem Matrix.GeneralLinearGroup.mapEquiv_refl (n : Type u) [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : mapEquiv n (RingEquiv.refl R) = MulEquiv.refl (GL n R)

@[simp]

theorem Matrix.GeneralLinearGroup.symm_mapEquiv (n : Type u) [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R ≃+* S) : (mapEquiv n f).symm = mapEquiv n f.symm

@[simp]

theorem Matrix.GeneralLinearGroup.mapEquiv_trans_mapEquiv (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 : R ≃+* S) (g : S ≃+* T) : (mapEquiv n f).trans (mapEquiv n g) = mapEquiv n (f.trans g)

@[simp]

theorem Matrix.GeneralLinearGroup.toMonoidHom_mapEquiv (n : Type u) [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R ≃+* S) : ↑(mapEquiv n f) = map ↑f

def Matrix.GeneralLinearGroup.transposeMulEquiv (n : Type u) [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : GL n R ≃* (GL n R)ᵐᵒᵖ

The equivalence between GL n R and (GL n R)ᵐᵒᵖ.

Equations

• Matrix.GeneralLinearGroup.transposeMulEquiv n = (Units.mapEquiv (Matrix.transposeRingEquiv n R).toMulEquiv).trans Units.opEquiv

@[simp]

theorem Matrix.GeneralLinearGroup.coe_unop_transposeMulEquiv (n : Type u) [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (a : GL n R) : ↑(MulOpposite.unop ((transposeMulEquiv n) a)) = (↑a).transpose

@[simp]

theorem Matrix.GeneralLinearGroup.transposeMulEquiv_symm_apply_op (n : Type u) [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (a : GL n R) : (transposeMulEquiv n).symm (MulOpposite.op a) = MulOpposite.unop ((transposeMulEquiv n) a)

def Matrix.GeneralLinearGroup.uliftMulEquiv (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] : GL n (ULift.{w, v} R) ≃* GL n R

The equivalence between GL n (ULift R) and GL n R.

Equations

• Matrix.GeneralLinearGroup.uliftMulEquiv n R = Matrix.GeneralLinearGroup.mapEquiv n ULift.ringEquiv

@[simp]

theorem Matrix.GeneralLinearGroup.uliftMulEquiv_apply (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] (a : GL n (ULift.{w, v} R)) : (uliftMulEquiv n R) a = (map ULift.ringEquiv.toRingHom) a

@[simp]

theorem Matrix.GeneralLinearGroup.uliftMulEquiv_symm (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] (a : GL n R) : (uliftMulEquiv n R).symm a = (map ULift.ringEquiv.symm.toRingHom) a

def Matrix.GeneralLinearGroup.reindex {n : Type u} [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] {m : Type u_3} [DecidableEq m] [Fintype m] (e : m ≃ n) : GL m R ≃* GL n R

The equivalence between GL m R and GL n R given by an equivalence e : m ≃ n.

Equations

• Matrix.GeneralLinearGroup.reindex R e = Units.mapEquiv ↑(Matrix.reindexRingEquiv R e)

@[simp]

theorem Matrix.GeneralLinearGroup.reindex_apply {n : Type u} [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] {m : Type u_3} [DecidableEq m] [Fintype m] (e : m ≃ n) (a✝ : (Matrix m m R)ˣ) : (reindex R e) a✝ = (Units.map ↑↑(reindexRingEquiv R e)) a✝

@[simp]

theorem Matrix.GeneralLinearGroup.symm_reindexMulEquiv {n : Type u} [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] {m : Type u_3} [DecidableEq m] [Fintype m] (e : m ≃ n) : (reindex R e).symm = reindex R e.symm

@[simp]

theorem Matrix.GeneralLinearGroup.reindexMulEquiv_trans_reindexMulEquiv {n : Type u} [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] {m : Type u_3} {o : Type u_4} [DecidableEq m] [Fintype m] [DecidableEq o] [Fintype o] (e : m ≃ n) (e' : n ≃ o) : (reindex R e).trans (reindex R e') = reindex R (e.trans e')

@[simp]

theorem Matrix.GeneralLinearGroup.reindexMulEquiv_refl {n : Type u} [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] : reindex R (Equiv.refl n) = MulEquiv.refl (GL n R)

def Matrix.GeneralLinearGroup.piEquiv {n : Type u} [DecidableEq n] [Fintype n] {ι : Type u_3} (R : ι → Type u_4) [(i : ι) → CommRing (R i)] : GL n ((i : ι) → R i) ≃* ((i : ι) → GL n (R i))

The monoid equivalence between GL n of a product of rings, and the product of the GL n of each ring.

Equations

• Matrix.GeneralLinearGroup.piEquiv R = (Units.mapEquiv Matrix.piRingEquiv.toMulEquiv).trans MulEquiv.piUnits

@[simp]

theorem Matrix.GeneralLinearGroup.piEquiv_apply {n : Type u} [DecidableEq n] [Fintype n] {ι : Type u_3} (R : ι → Type u_4) [(i : ι) → CommRing (R i)] (a✝ : (Matrix n n ((i : ι) → R i))ˣ) (i : ι) : (piEquiv R) a✝ i = MulEquiv.piUnits ((Units.mapEquiv ↑piRingEquiv) a✝) i

@[simp]

theorem Matrix.GeneralLinearGroup.piEquiv_symm_apply {n : Type u} [DecidableEq n] [Fintype n] {ι : Type u_3} (R : ι → Type u_4) [(i : ι) → CommRing (R i)] (a✝ : (i : ι) → GL n (R i)) : (piEquiv R).symm a✝ = (Units.mapEquiv (↑piRingEquiv).symm) (MulEquiv.piUnits.symm a✝)

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

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

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)⁻¹

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)

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

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

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

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

theorem Matrix.GeneralLinearGroup.map_scalar {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (u : Rˣ) : (map f) ((scalar n) u) = (scalar n) ((Units.map ↑f) u)

def Matrix.GeneralLinearGroup.kronecker {n : Type u} [DecidableEq n] [Fintype n] {R : Type u_3} {m : Type u_4} [CommSemiring R] [Fintype m] [DecidableEq m] (x : GL n R) (y : GL m R) : GL (n × m) R

The invertible kronecker matrix of invertible matrices.

Equations

• x.kronecker y = { val := Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ↑x ↑y, inv := Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) ↑x⁻¹ ↑y⁻¹, val_inv := ⋯, inv_val := ⋯ }

theorem Matrix.IsUnit.kronecker {n : Type u} [DecidableEq n] [Fintype n] {R : Type u_3} {m : Type u_4} [CommSemiring R] [Fintype m] [DecidableEq m] {x : Matrix n n R} {y : Matrix m m R} (hx : IsUnit x) (hy : IsUnit y) : IsUnit (kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y)

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

@[instance_reducible]

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

Equations

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

theorem Matrix.SpecialLinearGroup.toGL_injective {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : Function.Injective ⇑toGL

@[simp]

theorem Matrix.SpecialLinearGroup.toGL_inj {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (g g' : SpecialLinearGroup n R) : toGL g = toGL g' ↔ g = g'

@[simp]

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

@[simp]

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

theorem Matrix.SpecialLinearGroup.range_toGL_eq_ker_det {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : toGL.range = GeneralLinearGroup.det.ker

def Matrix.SpecialLinearGroup.toGLKerEquiv {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] : SpecialLinearGroup n R ≃* ↥GeneralLinearGroup.det.ker

Matrix.SpecialLinearGroup is isomorphic to GeneralLinearGroup.det.ker.

Equations

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

@[simp]

theorem Matrix.SpecialLinearGroup.toGLKerEquiv_symm_apply_coe {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (A : ↥GeneralLinearGroup.det.ker) : ↑(toGLKerEquiv.symm A) = ↑↑A

@[simp]

theorem Matrix.SpecialLinearGroup.toGLKerEquiv_apply_coe {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (g : SpecialLinearGroup n R) : ↑(toGLKerEquiv g) = toGL g

def Matrix.SpecialLinearGroup.mapGL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (S : Type u_1) [CommRing S] [Algebra R S] : SpecialLinearGroup n R →* GL n S

mapGL is the map from the special linear group over R to the general linear group over S, where S is an R-algebra.

Equations

• Matrix.SpecialLinearGroup.mapGL S = Matrix.SpecialLinearGroup.toGL.comp (Matrix.SpecialLinearGroup.map (algebraMap R S))

@[simp]

theorem Matrix.SpecialLinearGroup.mapGL_inj {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] [Algebra R S] [FaithfulSMul R S] (g g' : SpecialLinearGroup n R) : (mapGL S) g = (mapGL S) g' ↔ g = g'

theorem Matrix.SpecialLinearGroup.mapGL_injective {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] [Algebra R S] [FaithfulSMul R S] : Function.Injective ⇑(mapGL S)

@[simp]

theorem Matrix.SpecialLinearGroup.mapGL_coe_matrix {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] [Algebra R S] (g : SpecialLinearGroup n R) : ↑((mapGL S) g) = ↑((map (algebraMap R S)) g)

@[simp]

theorem Matrix.SpecialLinearGroup.map_mapGL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] [Algebra R S] {T : Type u_2} [CommRing T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (g : SpecialLinearGroup n R) : (GeneralLinearGroup.map (algebraMap S T)) ((mapGL S) g) = (mapGL T) g

@[simp]

theorem Matrix.SpecialLinearGroup.det_mapGL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] [Algebra R S] (g : SpecialLinearGroup n R) : GeneralLinearGroup.det ((mapGL S) g) = 1

def Matrix.GLPos (n : Type u) (R : Type v) [DecidableEq n] [Fintype n] [CommRing R] [LinearOrder R] [IsStrictOrderedRing 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)

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.

@[simp]

theorem Matrix.mem_glpos {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (A : GL n R) : A ∈ GLPos n R ↔ 0 < ↑(GeneralLinearGroup.det A)

theorem Matrix.GLPos.det_ne_zero {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (A : ↥(GLPos n R)) : (↑↑A).det ≠ 0

@[instance_reducible]

instance Matrix.instNegSubtypeGeneralLinearGroupMemSubgroupGLPos {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [Fact (Even (Fintype.card n))] : Neg ↥(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] [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [Fact (Even (Fintype.card n))] (g : ↥(GLPos n R)) : ↑(-g) = -↑g

@[simp]

theorem Matrix.GLPos.coe_neg {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [Fact (Even (Fintype.card n))] (g : ↥(GLPos n R)) : ↑↑(-g) = -↑↑g

@[simp]

theorem Matrix.GLPos.coe_neg_apply {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [Fact (Even (Fintype.card n))] (g : ↥(GLPos n R)) (i j : n) : ↑↑(-g) i j = -↑↑g i j

@[instance_reducible]

instance Matrix.instHasDistribNegSubtypeGeneralLinearGroupMemSubgroupGLPos {n : Type u} {R : Type v} [DecidableEq n] [Fintype n] [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] [Fact (Even (Fintype.card n))] : HasDistribNeg ↥(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} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] : SpecialLinearGroup n R →* ↥(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' := ⋯ }

@[instance_reducible]

instance Matrix.SpecialLinearGroup.instCoeSubtypeGeneralLinearGroupMemSubgroupGLPos {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] : Coe (SpecialLinearGroup n R) ↥(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} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] : Function.Injective ⇑toGLPos

@[simp]

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

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