Finite groups with trivial identity component

Let H be the coordinate Hopf algebra of a finite-type affine group over an algebraically closed field. If its identity component is the trivial subgroup scheme, then the canonical component morphism identifies the group with the finite constant group of connected components. In particular, H is finite-dimensional over the ground field.

The proof uses the existing description of the component morphism. It is surjective on points over every commutative test algebra, and its scheme-theoretic kernel is the identity component. When that kernel is trivial, the point map is also injective. Full faithfulness of the functor of points then promotes the pointwise isomorphism to an isomorphism of coordinate Hopf algebras.

Main declarations

• componentCoordinateIsoOfIdentityComponentHopfIdealEqAugmentation: a finite-type affine group with trivial identity component is the constant group on its connected components.
• moduleFinite_of_identityComponentHopfIdeal_eq_augmentation: its coordinate algebra is finite-dimensional.
• algebraEtale_of_identityComponentHopfIdeal_eq_augmentation: its coordinate algebra is etale.

References

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

This is the component-group input for the Layer 6 theorem that the center of a semisimple affine group is finite. Applied to the reduced center, it turns the vanishing of that smooth group's identity component into finiteness; finiteness of the original center then follows by controlling its nilpotent thickening.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateIsoOfIdentityComponentHopfIdealEqAugmentation {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (hH : HopfAlgebra.identityComponentHopfIdeal = HopfIdeal.augmentation k ↑H.obj) : { X := ConstantGroup.coordinateRing k (ConnectedComponents (PrimeSpectrum ↑H.obj)), commRing := LinearMap.convCommRing, hopfAlgebra := ConvolutionDual.instHopfAlgebra k (MonoidAlgebra k (ConnectedComponents (PrimeSpectrum ↑H.obj))) } ≅ H.obj

A finite-type affine group over an algebraically closed field with trivial identity component is canonically the constant group on the connected components of its spectrum.

Equations

• H.componentCoordinateIsoOfIdentityComponentHopfIdealEqAugmentation hH = CategoryTheory.asIso H.componentCoordinateHom

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentCoordinateIsoOfIdentityComponentHopfIdealEqAugmentation_hom {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (hH : HopfAlgebra.identityComponentHopfIdeal = HopfIdeal.augmentation k ↑H.obj) : (H.componentCoordinateIsoOfIdentityComponentHopfIdealEqAugmentation hH).hom = H.componentCoordinateHom

The forward morphism of the component-coordinate isomorphism is the canonical component coordinate morphism.

theorem TauCeti.FiniteTypeCommHopfAlgCat.moduleFinite_of_identityComponentHopfIdeal_eq_augmentation {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (hH : HopfAlgebra.identityComponentHopfIdeal = HopfIdeal.augmentation k ↑H.obj) : Module.Finite k ↑H.obj

The coordinate algebra of a finite-type affine group over an algebraically closed field is finite-dimensional when its identity component is the trivial subgroup scheme.

theorem TauCeti.FiniteTypeCommHopfAlgCat.algebraEtale_of_identityComponentHopfIdeal_eq_augmentation {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (hH : HopfAlgebra.identityComponentHopfIdeal = HopfIdeal.augmentation k ↑H.obj) : Algebra.Etale k ↑H.obj

The coordinate algebra of a finite-type affine group over an algebraically closed field is etale when its identity component is the trivial subgroup scheme.