The component group is finite etale

Let H be the coordinate Hopf algebra of a finite-type affine group over an algebraically closed field. The existing group-object representation of the fppf quotient by the identity component uses the constant group scheme on the finite group of connected components of Spec H. Here that scheme is named and its affineness, finiteness, and etaleness are recorded explicitly. The underlying sheaf of the quotient is also compared with the sheafification of the scheme's Yoneda functor of points on affine schemes.

Main declarations

• TauCeti.FiniteTypeCommHopfAlgCat.componentGroupScheme: the constant group scheme on the connected components of Spec H.
• TauCeti.FiniteTypeCommHopfAlgCat.isFinite_componentGroupScheme: the component group scheme is finite.
• TauCeti.FiniteTypeCommHopfAlgCat.etale_componentGroupScheme: the component group scheme is etale.
• TauCeti.FiniteTypeCommHopfAlgCat.componentGroupFppfSheafIsoSheafifiedSchemePoints: the underlying component quotient sheaf is isomorphic to the sheafified functor of points.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 2.37 and Section 5.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Sections 6.7 and 14.

This completes the algebraically closed-field case of the finite etale component-group target in Layer 3, "Identity component G° and component group π₀(G)", of the ReductiveGroups roadmap.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupScheme {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧k))

The constant group scheme on the connected components of the spectrum of a finite-type commutative Hopf algebra over an algebraically closed field.

Equations

• H.componentGroupScheme = TauCeti.ConstantGroup.groupScheme k (ConnectedComponents (PrimeSpectrum ↑H.obj))

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupScheme_def {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : H.componentGroupScheme = ConstantGroup.groupScheme k (ConnectedComponents (PrimeSpectrum ↑H.obj))

The component group scheme is the constant group scheme on the connected components.

instance TauCeti.FiniteTypeCommHopfAlgCat.isAffine_componentGroupScheme {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : AlgebraicGeometry.IsAffine H.componentGroupScheme.X.left

The component group scheme is affine.

instance TauCeti.FiniteTypeCommHopfAlgCat.isFinite_componentGroupScheme {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : AlgebraicGeometry.IsFinite H.componentGroupScheme.X.hom

The structural morphism of the component group scheme is finite.

instance TauCeti.FiniteTypeCommHopfAlgCat.etale_componentGroupScheme {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : AlgebraicGeometry.Etale H.componentGroupScheme.X.hom

The structural morphism of the component group scheme is etale.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupSchemePointsFppfSheaf {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : CategoryTheory.Sheaf (CommAlgCat.fppfTopology k) (Type (u + 1))

The sheafification of the universe-lifted Yoneda functor of points of the component group scheme on the affine fppf site.

Equations

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

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupFppfSheafIsoSheafifiedSchemePoints {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : H.componentGroupFppfSheaf.X ≅ H.componentGroupSchemePointsFppfSheaf

The underlying fppf component quotient sheaf is isomorphic to the sheafification of the component group scheme's universe-lifted Yoneda functor of points on affine schemes.

Equations

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