Finiteness of the components of an affine group scheme

An affine group scheme of finite type over a Noetherian commutative ring has finitely many connected components. This is the scheme-side form of the corresponding coordinate-ring fact: its structural morphism is locally of finite type over the Noetherian scheme Spec R, so its source is locally Noetherian; affineness makes the source compact, hence Noetherian.

Main declaration

• TauCeti.FiniteTypeAffineGroupSchemeCat.instFiniteConnectedComponents: the connected components of the underlying scheme form a finite type.

References

• J. S. Milne, Algebraic Groups (2017), Section 2.a.
• The Stacks Project, Tag 01T6, Properties of schemes, more on morphisms.

This is the scheme-side finiteness prerequisite for the identity component and component group in Layer 3 of the ReductiveGroups roadmap. Constructing the finite group scheme π₀ and proving it étale under the roadmap's smoothness hypotheses remain later steps.

instance TauCeti.FiniteTypeAffineGroupSchemeCat.instFiniteConnectedComponents {R : Type u} [CommRing R] [IsNoetherianRing R] (G : FiniteTypeAffineGroupSchemeCat ↧R) : Finite (ConnectedComponents ↥G.obj.obj.X.left)

The underlying scheme of a finite-type affine group scheme over a Noetherian commutative ring has finitely many connected components.