def MatrixGroups.termSL : Lean.ParserDescr

Equations

• MatrixGroups.termSL = Lean.ParserDescr.node `MatrixGroups.termSL 1024 (Lean.ParserDescr.symbol "SL")

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

• Matrix.transvection.toSL hij c = ⟨Matrix.transvection i j c, ⋯⟩

def Matrix.TransvectionStruct.toSL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (t : TransvectionStruct n R) : SpecialLinearGroup n R

Equations

• t.toSL = Matrix.transvection.toSL ⋯ t.c

def Matrix.TransvectionStruct.toGL {n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (t : TransvectionStruct n R) : GL n R

Equations

• t.toGL = Matrix.SpecialLinearGroup.toGL (Matrix.transvection.toSL ⋯ t.c)

def GeneralLinearGroup.scalar {R : Type v} [CommRing R] (n : Type u_1) [DecidableEq n] [Fintype n] (r : Rˣ) : GL n R

Equations

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

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

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

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

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

• ProjectiveGeneralLinearGroup n R = (GL n R ⧸ Subgroup.center (GL n R))

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

• PGL = ProjectiveGeneralLinearGroup

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

• ProjectiveSpecialLinearGroup n R = (Matrix.SpecialLinearGroup n R ⧸ Subgroup.center (Matrix.SpecialLinearGroup n R))

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

• PSL = ProjectiveSpecialLinearGroup

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

• SL_monoidHom_GL n R = Matrix.SpecialLinearGroup.toGL

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

• SL_monoidHom_PSL n R = QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup n R))

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

• GL_monoidHom_PGL n R = QuotientGroup.mk' (Subgroup.center (GL n R))

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

• SL_monoidHom_PGL n R = (GL_monoidHom_PGL n R).comp (SL_monoidHom_GL n R)

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

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

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

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

instance PGL_is_monoid (n : Type u_1) (R : Type u_2) [Fintype n] [DecidableEq n] [CommRing R] : Monoid (ProjectiveGeneralLinearGroup n R)

Equations

• PGL_is_monoid n R = RightCancelMonoid.toMonoid

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

• PSL_monoidHom_PGL n R = QuotientGroup.lift (Subgroup.center (Matrix.SpecialLinearGroup n R)) (SL_monoidHom_PGL n R) ⋯

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

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

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)

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)

theorem SpecialLinearGroup.toGL_inj {n : Type u_1} [DecidableEq n] [Fintype n] {R : Type u_2} [CommRing R] : Function.Injective ⇑Matrix.SpecialLinearGroup.toGL

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)

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)

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)

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

• PGL_iso_PSL n F = MulEquiv.ofBijective (PSL_monoidHom_PGL n F) ⋯