Finite flatness of the center of the special linear group

For a positive integer n, the center of SLₙ is the finite diagonalizable group μₙ. The preceding center calculation identifies its coordinate Hopf algebra with the group algebra k[Multiplicative (ZMod n)]. The standard group-algebra basis therefore makes this coordinate ring finite free of rank n over k.

This file transports the standard group-algebra basis across SpecialLinear.centerCoordinateIsoGroupAlgebra to the represented center of SLₙ. It follows that the center coordinate ring is finite free and faithfully flat of rank n. In particular, the structure morphism from that center to the trivial group is a central isogeny. This is the finite-kernel input for the standard central isogeny from SLₙ to its adjoint form.

No reducedness or smoothness assertion is made: when the characteristic divides n, μₙ is finite flat but nonreduced, exactly as the group-scheme statement requires.

Main declarations

• TauCeti.SpecialLinear.moduleFinite_centerCoordinate: the represented center of SLₙ is finite over the ground field.
• TauCeti.SpecialLinear.moduleFaithfullyFlat_centerCoordinate: it is faithfully flat.
• TauCeti.SpecialLinear.finrank_centerCoordinate: its rank is n.
• TauCeti.SpecialLinear.isCentralIsogeny_centerStructureMorphism: the center's structure morphism is a central isogeny.

References

• J. S. Milne, Algebraic Groups (2017), Examples 2.4 and 5.49, and §21.4.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 3.

This advances Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap: it supplies the finite flat center needed for the SLₙ central-isogeny and adjoint-form example.

theorem TauCeti.SpecialLinear.moduleFree_centerCoordinate {k : Type u} [Field k] (n : ℕ) (hn : 0 < n) : Module.Free k ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)))

The represented center coordinate algebra of SLₙ is a free module over the ground field.

theorem TauCeti.SpecialLinear.moduleFinite_centerCoordinate {k : Type u} [Field k] (n : ℕ) (hn : 0 < n) : Module.Finite k ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)))

The represented center coordinate algebra of SLₙ is finite as a module over the ground field.

theorem TauCeti.SpecialLinear.finiteType_centerCoordinate {k : Type u} [Field k] (n : ℕ) (hn : 0 < n) : Algebra.FiniteType k ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)))

The represented center coordinate algebra of SLₙ is a finite-type algebra over the ground field.

theorem TauCeti.SpecialLinear.moduleFaithfullyFlat_centerCoordinate {k : Type u} [Field k] (n : ℕ) (hn : 0 < n) : Module.FaithfullyFlat k ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)))

The represented center coordinate algebra of SLₙ is faithfully flat over the ground field.

theorem TauCeti.SpecialLinear.finrank_centerCoordinate {k : Type u} [Field k] (n : ℕ) (hn : 0 < n) : Module.finrank k ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n))) = n

The represented center coordinate algebra of SLₙ has rank n over the ground field.

theorem TauCeti.SpecialLinear.isCentralIsogeny_centerStructureMorphism {k : Type u} [Field k] (n : ℕ) (hn : 0 < n) : CommHopfAlgCat.IsCentralIsogeny (CommHopfAlgCat.ofHom (Bialgebra.unitBialgHom k ↑(CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)))))

The structure morphism from the represented center of SLₙ to the trivial group is a central isogeny. The kernel is the center itself, identified with the finite flat group μₙ.