The component group of an affine group

Let H be the coordinate Hopf algebra of a finite-type affine group over an algebraically closed field. Its identity component is a normal closed subgroup, so the fppf quotient construction defines the component group sheaf π₀(H) = H / H⁰.

On rational points, the corresponding pointwise quotient is canonically equivalent to the connected components of Spec H. The proof uses translation to identify two rational points modulo H⁰ exactly when their kernel points lie in the same connected component. Every connected component contains a rational point: its component idempotent is non-nilpotent, so the affine Nullstellensatz detects it at an algebraically closed point. Consequently the rational component group is finite.

No representability is asserted here. Showing that the fppf quotient is represented by a finite étale group scheme is the remaining scheme-theoretic part of the component-group construction.

Main declarations

• TauCeti.FiniteTypeCommHopfAlgCat.componentGroupFppfSheaf: the fppf quotient by the identity component.
• TauCeti.FiniteTypeCommHopfAlgCat.componentGroupFppfProjection: its locally surjective quotient projection.
• TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPoints: its pointwise precursor on rational points.
• TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsEquivConnectedComponents: the canonical equivalence between that quotient and the connected components of Spec H.
• TauCeti.FiniteTypeCommHopfAlgCat.instFiniteComponentGroupPoints: finiteness of the rational component group.

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 advances Layer 3, "Identity component G° and component group π₀(G)", of the ReductiveGroups roadmap.

@[reducible, inline]

abbrev TauCeti.FiniteTypeCommHopfAlgCat.rationalKernelPoint {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) : PrimeSpectrum ↑H.obj

The prime-spectrum point underlying a rational point of a finite-type affine group.

The explicit PrimeSpectrum return type bridges the scheme-point spelling of AlgHom.kernelPoint to the connected-component API.

Equations

• H.rationalKernelPoint g = TauCeti.AlgHom.kernelPoint g.ofConv

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.rationalKernelPoint_one {k : Type u} [Field k] (H : FiniteTypeCommHopfAlgCat k) : H.rationalKernelPoint 1 = Bialgebra.augmentationPoint k ↑H.obj

The prime-spectrum point underlying the identity rational point is the augmentation point.

theorem TauCeti.FiniteTypeCommHopfAlgCat.isNormal_identityComponentHopfIdeal {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : HopfAlgebra.identityComponentHopfIdeal.IsNormal

The identity-component Hopf ideal is normal over an algebraically closed field.

@[reducible, inline]

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

The component group fppf sheaf H / H⁰ of a finite-type affine group over an algebraically closed field. Its representability by a finite étale group scheme is not asserted here.

Equations

• H.componentGroupFppfSheaf = TauCeti.CommHopfAlgCat.fppfQuotientSheaf H.obj TauCeti.HopfAlgebra.identityComponentHopfIdeal ⋯

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupFppfProjection {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : CommHopfAlgCat.pointsFppfGroupObject H.obj ⟶ H.componentGroupFppfSheaf

The canonical morphism from the fppf sheaf of points of H to its component group sheaf.

Equations

• H.componentGroupFppfProjection = TauCeti.CommHopfAlgCat.fppfQuotientProjection H.obj TauCeti.HopfAlgebra.identityComponentHopfIdeal ⋯

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupFppfProjection_def {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : H.componentGroupFppfProjection = CommHopfAlgCat.fppfQuotientProjection H.obj HopfAlgebra.identityComponentHopfIdeal ⋯

The component-group projection is the fppf quotient projection by the identity component.

instance TauCeti.FiniteTypeCommHopfAlgCat.instEpiComponentGroupFppfProjection {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : CategoryTheory.Epi H.componentGroupFppfProjection

The projection to the component group is an epimorphism of group objects in fppf sheaves.

theorem TauCeti.FiniteTypeCommHopfAlgCat.isLocallySurjective_componentGroupFppfProjection {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : CategoryTheory.Sheaf.IsLocallySurjective H.componentGroupFppfProjection.hom.hom

Every section of the component group lifts to an ambient-group section after an fppf cover.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPoints {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : GrpCat

The rational pointwise component group H(k) / H⁰(k).

This is the value at k of the pointwise quotient presheaf whose sheafification is componentGroupFppfSheaf.

Equations

• H.componentGroupPoints = TauCeti.CommHopfAlgCat.pointwiseQuotientGroup H.obj TauCeti.HopfAlgebra.identityComponentHopfIdeal ⋯ ↧k

@[instance_reducible]

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsGroup {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : Group ↑H.componentGroupPoints

Locally expose the group structure carried by the bundled rational component group.

Equations

• H.componentGroupPointsGroup = H.componentGroupPoints.str

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsMk {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : HopfAlgebra.points ↧k ⟶ H.componentGroupPoints

The quotient homomorphism from rational points to the rational pointwise component group.

Equations

• H.componentGroupPointsMk = TauCeti.CommHopfAlgCat.pointwiseQuotientMk H.obj TauCeti.HopfAlgebra.identityComponentHopfIdeal ⋯ ↧k

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsMk_surjective {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom H.componentGroupPointsMk)

The quotient homomorphism from rational points to the rational component group is surjective.

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsMk_eq_one_iff {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) : (CategoryTheory.ConcreteCategory.hom H.componentGroupPointsMk) g = 1 ↔ g ∈ CommHopfAlgCat.quotientPointsSubgroup H.obj HopfAlgebra.identityComponentHopfIdeal ↧k

A rational point maps to the identity of the rational component group exactly when it lies in the identity-component subgroup.

theorem TauCeti.FiniteTypeCommHopfAlgCat.mem_identityComponentPointsSubgroup_iff {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup H.obj HopfAlgebra.identityComponentHopfIdeal ↧k ↔ H.rationalKernelPoint g ∈ connectedComponent (H.rationalKernelPoint 1)

A rational point belongs to H⁰(k) exactly when its kernel point belongs to the identity component of Spec H.

theorem TauCeti.FiniteTypeCommHopfAlgCat.connectedComponents_rationalKernelPoint_eq_iff {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g h : ↑(HopfAlgebra.points ↧k)) : ConnectedComponents.mk (H.rationalKernelPoint g) = ConnectedComponents.mk (H.rationalKernelPoint h) ↔ g⁻¹ * h ∈ CommHopfAlgCat.quotientPointsSubgroup H.obj HopfAlgebra.identityComponentHopfIdeal ↧k

Two rational points have kernel points in the same connected component exactly when their left quotient belongs to the identity-component subgroup.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsToConnectedComponents {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : ↑H.componentGroupPoints → ConnectedComponents (PrimeSpectrum ↑H.obj)

Send a rational point to the connected component containing its kernel point. This descends to the quotient by H⁰(k).

Equations

• H.componentGroupPointsToConnectedComponents q = Quotient.liftOn' q (fun (g : ↑(TauCeti.HopfAlgebra.points ↧k)) => ConnectedComponents.mk (H.rationalKernelPoint g)) ⋯

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsToConnectedComponents_mk {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (g : ↑(HopfAlgebra.points ↧k)) : H.componentGroupPointsToConnectedComponents ((CategoryTheory.ConcreteCategory.hom H.componentGroupPointsMk) g) = ConnectedComponents.mk (H.rationalKernelPoint g)

The component map sends the class of a rational point to the component containing its kernel point.

noncomputable def TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsEquivConnectedComponents {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : ↑H.componentGroupPoints ≃ ConnectedComponents (PrimeSpectrum ↑H.obj)

Over an algebraically closed field, the rational pointwise component group is canonically equivalent to the connected components of the prime spectrum.

Equations

• H.componentGroupPointsEquivConnectedComponents = Equiv.ofBijective H.componentGroupPointsToConnectedComponents ⋯

@[simp]

theorem TauCeti.FiniteTypeCommHopfAlgCat.componentGroupPointsEquivConnectedComponents_apply {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) (q : ↑H.componentGroupPoints) : H.componentGroupPointsEquivConnectedComponents q = H.componentGroupPointsToConnectedComponents q

The canonical equivalence from the rational pointwise component group is the component map on elements.

instance TauCeti.FiniteTypeCommHopfAlgCat.instFiniteComponentGroupPoints {k : Type u} [Field k] [IsAlgClosed k] (H : FiniteTypeCommHopfAlgCat k) : Finite ↑H.componentGroupPoints

The rational pointwise component group of a finite-type affine group over an algebraically closed field is finite.