Finiteness and centrality of SLₙ → PGLₙ

The conjugation homomorphism SLₙ → PGLₙ is the map underlying the expected central isogeny from the simply connected form to the adjoint form of type Aₙ₋₁ (for n ≥ 1). This file does not prove that it is a central isogeny. Over every commutative base ring, and in every rank, it proves:

• its coordinate morphism O(PGLₙ) → O(SLₙ) is finite;
• its scheme-theoretic kernel is central.

Over a field, it also reduces the central-isogeny property to injectivity of the coordinate morphism, as explained below.

Finiteness and centrality are two of the three conditions in TauCeti.CommHopfAlgCat.IsCentralIsogeny. Over a field, the third, faithful flatness, follows from injectivity of the coordinate morphism. Thus SLₙ → PGLₙ is a central isogeny exactly when its coordinate morphism is injective, that is, when the homomorphism is schematically dominant. That injectivity is not proved in this file.

Main declarations

• TauCeti.SpecialLinear.finite_conjugationMap: the coordinate morphism of SLₙ → PGLₙ is finite.
• TauCeti.SpecialLinear.isCentral_kernelHopfIdeal_conjugationMap: the kernel of SLₙ → PGLₙ is central.
• TauCeti.SpecialLinear.isCentralIsogeny_conjugationMap_iff_injective: over a field, SLₙ → PGLₙ is a central isogeny exactly when its coordinate morphism is injective.

References

• J. S. Milne, Algebraic Groups (2017), Examples 5.49 and 21.4, and Proposition 1.70.

theorem TauCeti.SpecialLinear.finite_conjugationMap (n : ℕ) (R : Type u) [CommRing R] : (↑(CommHopfAlgCat.Hom.hom (conjugationMap n R))).Finite

SLₙ → PGLₙ is finite: the special-linear coordinate Hopf algebra is a finite module over the coordinate Hopf algebra of PGLₙ, over every commutative ring and in every rank.

theorem TauCeti.SpecialLinear.isCentral_kernelHopfIdeal_conjugationMap (n : ℕ) (R : Type u) [CommRing R] : (CommHopfAlgCat.kernelHopfIdeal (conjugationMap n R)).IsCentral

The kernel of SLₙ → PGLₙ is central, over every commutative ring and in every rank: its points are central special-linear matrices, and this persists under extension of values.

@[simp]

theorem TauCeti.SpecialLinear.isCentralIsogeny_conjugationMap_iff_injective (n : ℕ) (k : Type u) [Field k] : CommHopfAlgCat.IsCentralIsogeny (conjugationMap n k) ↔ Function.Injective ⇑(CommHopfAlgCat.Hom.hom (conjugationMap n k))

SLₙ → PGLₙ is a central isogeny exactly when it is schematically dominant, that is, when its coordinate morphism is injective. Over a field, finiteness and centrality always hold, and once the coordinate morphism is injective, PGLₙ inherits geometric reducedness from the smooth group SLₙ, which makes the morphism faithfully flat.