Projective general linear group

In this file we define Matrix.ProjGenLinGroup n R as the quotient of GL n R by its center. We introduce notation PGL(n, R) for this group, which works if n is either a finite type or a natural number. If n is a number, then PGL(n, R) is interpreted as PGL(Fin n, R).

def Matrix.ProjGenLinGroup (n : Type u_1) [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] : Type (max (max u_1 u_2) u_2 u_1)

Projective general linear group $PGL(n, R)$ defined as the quotient of the general linear group by its center.

Equations

• Matrix.ProjGenLinGroup n R = (GL n R ⧸ Subgroup.center (GL n R))

@[implicit_reducible]

instance Matrix.instGroupProjGenLinGroup (n : Type u_1) [Fintype n] [DecidableEq n] (R : Type u_2) [CommRing R] : Group (ProjGenLinGroup n R)

Equations

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

def MatrixGroups.«termPGL(_,_)» : Lean.ParserDescr

Projective general linear group $PGL(n, R)$ defined as the quotient of the general linear group by its center.

Equations

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

def MatrixGroups.«termPGL(_,_)_1» : Lean.ParserDescr

Projective general linear group $PGL(n, R)$ defined as the quotient of the general linear group by its center.

Equations

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

def Matrix.ProjGenLinGroup.mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : GL n R →* ProjGenLinGroup n R

The natural projection from GL n R to PGL n R.

Equations

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

theorem Matrix.ProjGenLinGroup.mk_surjective {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : Function.Surjective ⇑mk

theorem Matrix.ProjGenLinGroup.mk_eq_mk_iff' {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {g₁ g₂ : GL n R} : mk g₁ = mk g₂ ↔ ∃ z ∈ Subgroup.center (GL n R), g₁ * z = g₂

theorem Matrix.ProjGenLinGroup.mk_eq_mk_iff {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {g₁ g₂ : GL n R} : mk g₁ = mk g₂ ↔ ∃ (u : Rˣ), g₁ * (GeneralLinearGroup.scalar n) u = g₂

@[simp]

theorem Matrix.ProjGenLinGroup.ker_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : mk.ker = Subgroup.center (GL n R)

@[simp]

theorem Matrix.ProjGenLinGroup.mk_eq_one {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {g : GL n R} : mk g = 1 ↔ g ∈ Subgroup.center (GL n R)

@[simp]

theorem Matrix.ProjGenLinGroup.mk_scalar {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (u : Rˣ) : mk ((GeneralLinearGroup.scalar n) u) = 1

theorem Matrix.ProjGenLinGroup.induction_on {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {motive : ProjGenLinGroup n R → Prop} (g : ProjGenLinGroup n R) (mk : ∀ (g : GL n R), motive (mk g)) : motive g

def Matrix.ProjectiveSpecialLinearGroup.toPGL {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : ProjectiveSpecialLinearGroup n R →* ProjGenLinGroup n R

The natural inclusion map from PSL(n, R) to PGL(n, R) induced by the inclusion map from SL(n, R) to GL(n, R).

Equations

• Matrix.ProjectiveSpecialLinearGroup.toPGL = QuotientGroup.lift (Subgroup.center (Matrix.SpecialLinearGroup n R)) (Matrix.ProjGenLinGroup.mk.comp Matrix.SpecialLinearGroup.toGL) ⋯

@[simp]

theorem Matrix.ProjectiveSpecialLinearGroup.toPGL_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (g : SpecialLinearGroup n R) : toPGL ↑g = ProjGenLinGroup.mk (SpecialLinearGroup.toGL g)

theorem Matrix.ProjectiveSpecialLinearGroup.toPGL_injective {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : Function.Injective ⇑toPGL

theorem Matrix.ProjectiveSpecialLinearGroup.toPGL_surj_of_roots {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (hR : ∀ (r : Rˣ), ∃ (k : Rˣ), k ^ Fintype.card n = r) : Function.Surjective ⇑toPGL

theorem Matrix.ProjectiveSpecialLinearGroup.toPGL_surj_iff {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [Nonempty n] : Function.Surjective ⇑toPGL ↔ ∀ (r : Rˣ), ∃ (k : Rˣ), k ^ Fintype.card n = r

noncomputable def Matrix.ProjGenLinGroup.isoPSLOfAlgClosedOfNonempty {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {F : Type u_3} [Field F] [IsAlgClosed F] : ProjGenLinGroup n F ≃* ProjectiveSpecialLinearGroup n F

An isomorphism between PGL(n, F) and PSL(n, F) in the case of an algebraically closed field induced from the natural inclusion map.

Equations

• Matrix.ProjGenLinGroup.isoPSLOfAlgClosedOfNonempty = (MulEquiv.ofBijective Matrix.ProjectiveSpecialLinearGroup.toPGL ⋯).symm

noncomputable def Matrix.ProjGenLinGroup.isoPSLOfAlgClosed {n : Type u_1} [Fintype n] [DecidableEq n] {F : Type u_3} [Field F] [IsAlgClosed F] : ProjGenLinGroup n F ≃* ProjectiveSpecialLinearGroup n F

An isomorphism between PGL(n, F) and PSL(n, F) in the case of an algebraically closed field induced from the natural inclusion map where when n is empty it gives a junk isomorphism.

Equations

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

def Matrix.ProjGenLinGroup.lift {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {M : Type u_3} [Monoid M] (f : GL n R →* M) (hf : f.comp (GeneralLinearGroup.scalar n) = 1) : ProjGenLinGroup n R →* M

Lift a monoid homomorphism f : GL n R →* M that vanishes on all scalar matrices to a homomorphism from PGL(n, R).

Equations

• Matrix.ProjGenLinGroup.lift f hf = QuotientGroup.lift (Subgroup.center (GL n R)) f ⋯

@[simp]

theorem Matrix.ProjGenLinGroup.lift_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {M : Type u_3} [Monoid M] {f : GL n R →* M} (hf : f.comp (GeneralLinearGroup.scalar n) = 1) (g : GL n R) : (lift f hf) (mk g) = f g

@[simp]

theorem Matrix.ProjGenLinGroup.lift_comp_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {M : Type u_3} [Monoid M] {f : GL n R →* M} (hf : f.comp (GeneralLinearGroup.scalar n) = 1) : (lift f hf).comp mk = f

@[implicit_reducible]

def Matrix.ProjGenLinGroup.mulActionOfGL {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {α : Type u_4} [MulAction (GL n R) α] (h : ∀ (u : Rˣ) (a : α), (GeneralLinearGroup.scalar n) u • a = a) : MulAction (ProjGenLinGroup n R) α

Given an action of GL n R such that the scalar matrices act trivially, define an action of PGL n R.

Equations

• Matrix.ProjGenLinGroup.mulActionOfGL h = MulAction.ofEndHom (Matrix.ProjGenLinGroup.lift MulAction.toEndHom ⋯)

theorem Matrix.ProjGenLinGroup.mk_smul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {α : Type u_4} [MulAction (GL n R) α] (h : ∀ (u : Rˣ) (a : α), (GeneralLinearGroup.scalar n) u • a = a) (g : GL n R) (a : α) : mk g • a = g • a

def Matrix.ProjGenLinGroup.signDet {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [Fact (Even (Fintype.card n))] [LinearOrder R] [IsStrictOrderedRing R] : ProjGenLinGroup n R →* SignTypeˣ

In case of an even dimension, the sign of the determinant of g : PGL(n, R) is well-defined.

Equations

• Matrix.ProjGenLinGroup.signDet = Matrix.ProjGenLinGroup.lift ((Units.map ↑signHom).comp Matrix.GeneralLinearGroup.det) ⋯

theorem Matrix.ProjGenLinGroup.signDet_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [Fact (Even (Fintype.card n))] [LinearOrder R] [IsStrictOrderedRing R] (g : GL n R) : signDet (mk g) = (Units.map ↑signHom) (GeneralLinearGroup.det g)

@[simp]

theorem Matrix.ProjGenLinGroup.val_signDet_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] [Fact (Even (Fintype.card n))] [LinearOrder R] [IsStrictOrderedRing R] (g : GL n R) : ↑(signDet (mk g)) = SignType.sign ↑(GeneralLinearGroup.det g)