Documentation

ClassificationOfSubgroups.Ch4_PGLIsoPSLOverAlgClosedField.ProjectiveGeneralLinearGroup

source
def MatrixGroups.termSL :
Lean.ParserDescr
Equations
source
def Matrix.transvection.toSL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {i j : n} (hij : i ≠ j) (c : R) :
SpecialLinearGroup n R
Equations
source
def Matrix.TransvectionStruct.toSL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (t : TransvectionStruct n R) :
SpecialLinearGroup n R
Equations
source
def Matrix.TransvectionStruct.toGL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (t : TransvectionStruct n R) :
GL n R
Equations
source
def GeneralLinearGroup.scalar {R : Type v} [CommRing R] (n : Type u_1) [DecidableEq n] [Fintype n] (r : Rˣ) :
GL n R
Equations
source
theorem GeneralLinearGroup.coe_scalar_matrix {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (r : Rˣ) :
(Matrix.scalar n) ↑r = ↑(scalar n r)

The scalar matrix r • 1 belongs to GL n R if and only if r is a unit

source
theorem GeneralLinearGroup.mem_range_unit_scalar_of_mem_range_scalar_and_mem_general_linear_group {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {M : GL n R} (hM : ↑M ∈ Set.range ⇑(Matrix.scalar n)) :
∃ (r : Rˣ), r • 1 = M
source
theorem GeneralLinearGroup.Center.mem_center_general_linear_group_iff {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {M : GL n R} :
M ∈ Subgroup.center (GL n R) ↔ ∃ (r : Rˣ), r • 1 = M
source
@[reducible, inline]
abbrev ProjectiveGeneralLinearGroup (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] :
Type (max (max u v) v u)

A projective general linear group is the quotient of a special linear group by its center.

Equations
Instances For
source
@[reducible, inline]
abbrev PGL (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] :
Type (max (max u_1 u_2) u_2 u_1)

PGL n R is the projective special linear group (GL n R)/ Z(GL(n R)).

Equations
source
@[reducible, inline]
abbrev ProjectiveSpecialLinearGroup (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R] :
Type (max (max u v) v u)

A projective special linear group is the quotient of a special linear group by its center.

Equations
source
@[reducible, inline]
abbrev PSL (n : Type u_1) [DecidableEq n] [Fintype n] (R : Type u_2) [CommRing R] :
Type (max (max u_1 u_2) u_2 u_1)

PSL(n, R) is the projective special linear group SL(n, R)/Z(SL(n, R)).

Equations
source
def SL_monoidHom_GL (n : Type u_1) [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] :
Matrix.SpecialLinearGroup n R →* GL n R
Equations
source
def SL_monoidHom_PSL (n : Type u_1) [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] :
Matrix.SpecialLinearGroup n R →* PSL n R
Equations
source
def GL_monoidHom_PGL (n : Type u_1) [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] :
GL n R →* PGL n R
Equations
source
def SL_monoidHom_PGL (n : Type u_1) [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] :
Matrix.SpecialLinearGroup n R →* PGL n R
Equations
source
theorem coe (R : Type v) [CommRing R] {n : Type u_1} [Fintype n] [DecidableEq n] (x : Matrix.SpecialLinearGroup n R) :
↑(Matrix.SpecialLinearGroup.toGL x) = ↑x
source
theorem scalar_eq_smul_one (n : Type u_1) [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] (r : R) :
(Matrix.scalar n) r = r • 1
source
theorem center_SL_le_ker (n : Type u_1) [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] :
Subgroup.center (Matrix.SpecialLinearGroup n R) ≤ (SL_monoidHom_PGL n R).ker
source
instance center_is_normal (n : Type u_1) (R : Type u_2) [Fintype n] [DecidableEq n] [CommRing R] :
(Subgroup.center (Matrix.SpecialLinearGroup n R)).Normal
source
instance PGL_is_monoid (n : Type u_1) (R : Type u_2) [Fintype n] [DecidableEq n] [CommRing R] :
Monoid (ProjectiveGeneralLinearGroup n R)
Equations
source
def PSL_monoidHom_PGL (n : Type u_1) (R : Type u_2) [Fintype n] [DecidableEq n] [CommRing R] :
PSL n R →* PGL n R
Equations
source
theorem exists_SL_eq_scaled_GL_of_IsAlgClosed {n : Type u_1} {F : Type u_2} [hn₁ : Fintype n] [DecidableEq n] [Field F] [IsAlgClosed F] (G : GL n F) :
∃ (α : Fˣ) (S : Matrix.SpecialLinearGroup n F), α • Matrix.SpecialLinearGroup.toGL S = G
source
theorem lift_scalar_matrix_eq_one {n : Type u_1} {F : Type u_2} [hn₁ : Fintype n] [DecidableEq n] [Field F] [IsAlgClosed F] (c : Fˣ) :
(GL_monoidHom_PGL n F) (c • 1) = 1
source
instance instIsScalarTowerUnitsGeneralLinearGroup_classificationOfSubgroups (n : Type u_1) (R : Type u_2) [Fintype n] [DecidableEq n] [CommRing R] :
IsScalarTower Rˣ (GL n R) (GL n R)
source
theorem Injective_PSL_monoidHom_PGL (n : Type u_1) (F : Type u_2) [hn₁ : Fintype n] [DecidableEq n] [Field F] [IsAlgClosed F] :
Function.Injective ⇑(PSL_monoidHom_PGL n F)
source
theorem SpecialLinearGroup.toGL_inj {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] :
Function.Injective ⇑Matrix.SpecialLinearGroup.toGL
source
theorem ker_SL_monoidHom_PGL_eq_center (R : Type v) [CommRing R] (n : Type u_1) (F : Type u_2) [hn₁ : Fintype n] [DecidableEq n] [Field F] [IsAlgClosed F] :
(SL_monoidHom_PGL n R).ker = Subgroup.center (Matrix.SpecialLinearGroup n R)
source
theorem Surjective_PSL_monoidHom_PGL (n : Type u_1) (F : Type u_2) [hn₁ : Fintype n] [DecidableEq n] [Field F] [IsAlgClosed F] :
Function.Surjective ⇑(PSL_monoidHom_PGL n F)
source
theorem Bijective_PSL_monoidHom_PGL (n : Type u_1) (F : Type u_2) [hn₁ : Fintype n] [DecidableEq n] [Field F] [IsAlgClosed F] :
Function.Bijective ⇑(PSL_monoidHom_PGL n F)
source
noncomputable def PGL_iso_PSL (n : Type u_1) (F : Type u_2) [Fintype n] [DecidableEq n] [Field F] [IsAlgClosed F] :
PSL n F ≃* PGL n F
Equations