The center of a semisimple group is finite locally free

The scheme-theoretic center of a semisimple affine group over a field is a finite locally free commutative group scheme. In Hopf coordinates, its coordinate algebra is finite by the finiteness theorem for semisimple centers, projective because it is a vector space over a field, and cocommutative because the center is a central subgroup. It is also faithfully flat: the counit shows that the coordinate algebra is nonzero, and every nonzero vector space is faithfully flat.

This file packages those three facts in the category used by Cartier duality. It also records that the structure morphism from the center to the trivial group is a central isogeny. These are the finite-flat inputs needed when constructing the quotient of a semisimple group by its center.

Main declarations

• TauCeti.semisimpleCommHopfAlgProperty.centerFiniteLocallyFree: the center, packaged as a finite locally free bicommutative Hopf algebra.
• TauCeti.semisimpleCommHopfAlgProperty.isCentralIsogeny_centerStructureMorphism: the center's structure morphism to the trivial group is a central isogeny.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 2.21 and §21.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapters 2 and 6.

@[reducible, inline]

noncomputable abbrev TauCeti.semisimpleCommHopfAlgProperty.centerFiniteLocallyFree {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) : FiniteLocallyFreeBicommutativeHopfAlgCat k

The center of a semisimple affine group, packaged as a finite locally free bicommutative Hopf algebra. This is the form in which the center can be fed directly to Cartier duality.

Equations

• hH.centerFiniteLocallyFree = TauCeti.FiniteLocallyFreeBicommutativeHopfAlgCat.of k ↑(TauCeti.CommHopfAlgCat.centerCoordinateHopfAlgebra H.obj)

theorem TauCeti.semisimpleCommHopfAlgProperty.isCentralIsogeny_centerStructureMorphism {k : Type u} [Field k] {H : FiniteTypeCommHopfAlgCat k} (hH : semisimpleCommHopfAlgProperty k H) : CommHopfAlgCat.IsCentralIsogeny (CommHopfAlgCat.ofHom (Bialgebra.unitBialgHom k ↑(CommHopfAlgCat.centerCoordinateHopfAlgebra H.obj)))

The structure morphism from the center of a semisimple affine group to the trivial group is a central isogeny. Its kernel is the whole center, which is finite locally free and commutative.