The identity component as a Hopf ideal

Let H be a commutative Hopf algebra of finite type over an algebraically closed field. The connected component of the counit point is stable under multiplication: equivalently, the comultiplication of the ideal cutting out that component lies in I ⊗ H + H ⊗ I. Together with the counit and antipode results already available for this ideal, this packages the identity component as a HopfIdeal.

The multiplication argument is carried out on algebraically closed points of the component quotient. Translation stability shows that the product of two such points is still in the identity component. The affine Nullstellensatz then promotes this pointwise statement to the required identity in the tensor square; tensor-product right exactness identifies its kernel with I ⊗ H + H ⊗ I.

The algebraically closed hypothesis is the natural one for the geometric identity component in the reductive-groups roadmap. Descent of this construction to the ground field and construction of the component group are separate steps.

Main declarations

• TauCeti.HopfAlgebra.comul_mem_connectedComponentIdeal_augmentationPoint: the component ideal is stable under comultiplication.
• TauCeti.HopfAlgebra.identityComponentHopfIdeal: the Hopf ideal cutting out the identity component.

References

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

This advances Layer 3, "Identity component G° and component group π₀(G)", of the ReductiveGroups roadmap. The quotient Hopf algebra now gives the identity component over an algebraically closed field; descent, geometric connectedness over a general field, and the finite étale component group remain.

theorem TauCeti.HopfAlgebra.comul_mem_connectedComponentIdeal_augmentationPoint {k : Type u} [Field k] [IsAlgClosed k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] {x : H} : x ∈ PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H) → CoalgebraStruct.comul x ∈ HopfIdeal.leftTensorIdeal k H (PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H)) ⊔ HopfIdeal.rightTensorIdeal k H (PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H))

The ideal cutting out the augmentation point's connected component is stable under comultiplication.

noncomputable def TauCeti.HopfAlgebra.identityComponentHopfIdeal {k : Type u} [Field k] [IsAlgClosed k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] : HopfIdeal k H

The Hopf ideal cutting out the connected component of the identity in a finite-type affine group over an algebraically closed field.

Equations

• TauCeti.HopfAlgebra.identityComponentHopfIdeal = TauCeti.HopfIdeal.ofIdeal (PrimeSpectrum.connectedComponentIdeal (TauCeti.Bialgebra.augmentationPoint k H)) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.HopfAlgebra.identityComponentHopfIdeal_toIdeal {k : Type u} [Field k] [IsAlgClosed k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] : identityComponentHopfIdeal.toIdeal = PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H)

The underlying ideal of the identity-component Hopf ideal is the ideal generated by the complement of the augmentation point's component idempotent.

@[simp]

theorem TauCeti.HopfAlgebra.mem_identityComponentHopfIdeal {k : Type u} [Field k] [IsAlgClosed k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] {x : H} : x ∈ identityComponentHopfIdeal ↔ x ∈ PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H)

Membership in the identity-component Hopf ideal is membership in the ideal cutting out the augmentation point's connected component.

@[simp]

theorem TauCeti.HopfAlgebra.identityComponentHopfIdeal_eq_bot_iff_connectedSpace {k : Type u} [Field k] [IsAlgClosed k] {H : Type v} [CommRing H] [HopfAlgebra k H] [Algebra.FiniteType k H] : identityComponentHopfIdeal = ⊥ ↔ ConnectedSpace (PrimeSpectrum H)

The identity-component Hopf ideal of a finite-type affine group vanishes exactly when its spectrum is connected.

theorem TauCeti.CommHopfAlgCat.identityComponentHopfIdeal_toIdeal_le_ker_of_connected {k : Type u} [Field k] [IsAlgClosed k] {H : CommHopfAlgCat k} [Algebra.FiniteType k ↑H] {K : CommHopfAlgCat k} [ConnectedSpace (PrimeSpectrum ↑K)] (f : H ⟶ K) : HopfAlgebra.identityComponentHopfIdeal.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom

The ideal of the identity component of a finite-type affine group is killed by every homomorphism to a connected affine group. Contravariantly, the image of a connected group containing the identity lies in the identity component.