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

Main definitions

• Matrix.SpecialLinearGroup.toPGL is the natural map from SL(n, R) to PGL(n, R).

• Matrix.ProjectiveSpecialLinearGroup.toPGL is the natural inclusion from PSL(n, R) to PGL(n, R).

• Matrix.ProjectiveSpecialLinearGroup.isoPSLOfAlgClosed is an isomorphism between PGL(n, F) and PSL(n, F) in the case of an algebraically closed field.

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_one {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : mk 1 = 1

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

@[reducible, inline]

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

The natural map from SL(n, R) to PGL(n, R) by composing the maps from SL to GL and the quotient map from GL to PGL.

Equations

• Matrix.SpecialLinearGroup.toPGL = Matrix.ProjGenLinGroup.mk.comp Matrix.SpecialLinearGroup.toGL

theorem Matrix.SpecialLinearGroup.toPGL_ker {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : toPGL.ker = Subgroup.center (SpecialLinearGroup n R)

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.SpecialLinearGroup.toPGL ⋯

@[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.ProjectiveSpecialLinearGroup.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.ProjectiveSpecialLinearGroup.isoPSLOfAlgClosedOfNonempty = (MulEquiv.ofBijective Matrix.ProjectiveSpecialLinearGroup.toPGL ⋯).symm

noncomputable def Matrix.ProjectiveSpecialLinearGroup.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.map {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {S : Type u_4} [CommRing S] (f : R →+* S) : ProjGenLinGroup n R →* ProjGenLinGroup n S

The monoid hom between PGL(n, R) and PGL(n, S) induced by a ring homomorphism f : R →+* S.

Equations

• Matrix.ProjGenLinGroup.map f = QuotientGroup.map (Subgroup.center (GL n R)) (Subgroup.center (GL n S)) (Matrix.GeneralLinearGroup.map f) ⋯

@[simp]

theorem Matrix.ProjGenLinGroup.map_id {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : map (RingHom.id R) = MonoidHom.id (ProjGenLinGroup n R)

@[simp]

theorem Matrix.ProjGenLinGroup.map_mk {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {S : Type u_4} [CommRing S] (f : R →+* S) (g : GL n R) : (map f) (mk g) = mk ((GeneralLinearGroup.map f) g)

theorem Matrix.ProjGenLinGroup.map_comp {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {S : Type u_4} {T : Type u_5} [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) : map (g.comp f) = (map g).comp (map f)

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)