The projective special linear point functor

For positive n, the represented center of SLₙ maps isomorphically onto the ordinary center of its group of points. Consequently, its pointwise center quotient is Mathlib's projective special linear group PSL(Fin n, A) over every commutative value algebra A. This file proves that identification and packages it naturally in A.

Over an algebraically closed field, Mathlib's canonical inclusion from PSLₙ to PGLₙ is bijective. Composing it with the pointwise quotient identification gives the expected SLₙ / Z(SLₙ) ≅ PGLₙ on field-valued points.

These are identifications of pointwise quotients before fppf sheafification. They do not assert that the pointwise quotient is already an fppf sheaf, or construct a representing Hopf algebra.

Main declarations

• TauCeti.SpecialLinear.centerPointwiseQuotientIsoPSL: the objectwise group isomorphism.
• TauCeti.SpecialLinear.pslPointsFunctor: projective special linear groups under extension of scalars.
• TauCeti.SpecialLinear.centerPointwiseQuotientNatIsoPSL: the natural pointwise identification.
• TauCeti.SpecialLinear.centerPointwiseQuotientIsoPGLOfAlgClosed: the resulting identification with PGLₙ over an algebraically closed field.

References

• J. S. Milne, Algebraic Groups (2017), Examples 5.49 and 21.4.
• The quotient equivalence, point functor, naturality proof, and natural isomorphism adapt the corresponding constructions in TauCeti.Algebra.AlgebraicGroup.GeneralLinear.Projective.

theorem TauCeti.SpecialLinear.map_centerPointsSubgroup_pointsMulEquiv_eq_center (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) : Subgroup.map (↑(pointsMulEquiv k n)) (CommHopfAlgCat.centerPointsSubgroup (coordinateHopfAlgebra k n) A) = Subgroup.center (Matrix.SpecialLinearGroup (Fin n) ↑A)

Under the standard equivalence between SLₙ-points and determinant-one matrices, the represented center maps onto the ordinary group-theoretic center.

noncomputable def TauCeti.SpecialLinear.centerPointwiseQuotientIsoPSL (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) : CommHopfAlgCat.centerPointwiseQuotient (coordinateHopfAlgebra k n) A ≅ ↧(Matrix.ProjectiveSpecialLinearGroup (Fin n) ↑A)

The pointwise quotient of SLₙ by its represented center is the projective special linear group over the same value algebra.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.centerPointwiseQuotientIsoPSL_hom_mk (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (q : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientIsoPSL n hn A).hom) ↑q = ↑((pointsMulEquiv k n) q)

The quotient equivalence sends the class of an SLₙ-point to the class of its associated determinant-one matrix.

@[simp]

theorem TauCeti.SpecialLinear.centerPointwiseQuotientIsoPSL_inv_mk (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (g : Matrix.SpecialLinearGroup (Fin n) ↑A) : (CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientIsoPSL n hn A).inv) ↑g = ↑((pointsMulEquiv k n).symm g)

The inverse quotient equivalence sends the class of a determinant-one matrix to the class of its associated SLₙ-point.

noncomputable def TauCeti.SpecialLinear.pslPointsFunctor (n : ℕ) {R : Type u} [CommRing R] : CategoryTheory.Functor (CommAlgCat R) GrpCat

The presheaf A ↦ PSL(Fin n, A), with maps induced by entrywise extension of scalars.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.pslPointsFunctor_obj (n : ℕ) {R : Type u} [CommRing R] (A : CommAlgCat R) : (pslPointsFunctor n).obj A = ↧(Matrix.ProjectiveSpecialLinearGroup (Fin n) ↑A)

The objects of pslPointsFunctor are Mathlib's projective special linear groups.

@[simp]

theorem TauCeti.SpecialLinear.pslPointsFunctor_map (n : ℕ) {R : Type u} [CommRing R] {A B : CommAlgCat R} (φ : A ⟶ B) : (pslPointsFunctor n).map φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GrpCat.ofHom (projectiveMap n ↑(CommAlgCat.Hom.hom φ))) (CategoryTheory.eqToHom ⋯))

The maps of pslPointsFunctor are induced by entrywise extension of scalars.

theorem TauCeti.SpecialLinear.centerPointwiseQuotientIsoPSL_hom_naturality (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) {A B : CommAlgCat k} (φ : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.mapPointwiseQuotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)) ⋯ φ) (centerPointwiseQuotientIsoPSL n hn B).hom = CategoryTheory.CategoryStruct.comp (centerPointwiseQuotientIsoPSL n hn A).hom (GrpCat.ofHom (projectiveMap n (CommAlgCat.Hom.hom φ).toRingHom))

The quotient equivalence commutes with extension of scalars in the value algebra.

noncomputable def TauCeti.SpecialLinear.centerPointwiseQuotientNatIsoPSL (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) : CommHopfAlgCat.pointwiseQuotientFunctor (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)) ⋯ ≅ pslPointsFunctor n

The pointwise center quotient of SLₙ is naturally isomorphic to the presheaf with values Mathlib's projective special linear groups.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.centerPointwiseQuotientNatIsoPSL_hom_app (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((centerPointwiseQuotientNatIsoPSL n hn).hom.app A) (CategoryTheory.eqToHom ⋯)) = (centerPointwiseQuotientIsoPSL n hn A).hom

After transport to the concrete quotient groups, the hom component of the natural identification is the objectwise quotient isomorphism.

@[simp]

theorem TauCeti.SpecialLinear.centerPointwiseQuotientNatIsoPSL_inv_app (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((centerPointwiseQuotientNatIsoPSL n hn).inv.app A) (CategoryTheory.eqToHom ⋯)) = (centerPointwiseQuotientIsoPSL n hn A).inv

After transport to the concrete quotient groups, the inverse component of the natural identification is the inverse objectwise quotient isomorphism.

@[simp]

theorem TauCeti.SpecialLinear.centerPointwiseQuotientNatIsoPSL_hom_app_mk (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (q : ↑(HopfAlgebra.points A)) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((centerPointwiseQuotientNatIsoPSL n hn).hom.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ↑q)) = ↑((pointsMulEquiv k n) q)

After transport to the concrete quotient groups, the hom component of the natural identification sends a quotient class to the class of its associated determinant-one matrix.

@[simp]

theorem TauCeti.SpecialLinear.centerPointwiseQuotientNatIsoPSL_inv_app_mk (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (g : Matrix.SpecialLinearGroup (Fin n) ↑A) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((centerPointwiseQuotientNatIsoPSL n hn).inv.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ↑g)) = ↑((pointsMulEquiv k n).symm g)

After transport to the concrete quotient groups, the inverse component of the natural identification sends the class of a determinant-one matrix to its associated quotient class.

noncomputable def TauCeti.SpecialLinear.centerPointwiseQuotientIsoPGLOfAlgClosed (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (F : Type u) [Field F] [IsAlgClosed F] [Algebra k F] : CommHopfAlgCat.centerPointwiseQuotient (coordinateHopfAlgebra k n) ↧F ≅ ↧(Matrix.ProjGenLinGroup (Fin n) F)

Over an algebraically closed field, the pointwise center quotient of SLₙ is PGLₙ. This uses Mathlib's canonical isomorphism between projective general and special linear groups.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.centerPointwiseQuotientIsoPGLOfAlgClosed_hom_mk (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (F : Type u) [Field F] [IsAlgClosed F] [Algebra k F] (q : ↑(HopfAlgebra.points ↧F)) : (CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientIsoPGLOfAlgClosed n hn F).hom) ↑q = Matrix.ProjGenLinGroup.mk (Matrix.SpecialLinearGroup.toGL ((pointsMulEquiv k n) q))

The algebraically closed-field identification sends an SLₙ-point to the projective class of its underlying invertible matrix.

@[simp]

theorem TauCeti.SpecialLinear.centerPointwiseQuotientIsoPGLOfAlgClosed_inv_mk_toGL (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (F : Type u) [Field F] [IsAlgClosed F] [Algebra k F] (g : Matrix.SpecialLinearGroup (Fin n) F) : (CategoryTheory.ConcreteCategory.hom (centerPointwiseQuotientIsoPGLOfAlgClosed n hn F).inv) (Matrix.ProjGenLinGroup.mk (Matrix.SpecialLinearGroup.toGL g)) = ↑((pointsMulEquiv k n).symm g)

The inverse algebraically closed-field identification sends the projective class of a determinant-one matrix to the quotient class of its associated SLₙ-point.