The identity component of an affine group

Let H be a commutative Hopf algebra over a field whose prime spectrum is locally connected. The connected component of the counit point is cut out by the principal ideal generated by the complement of its component idempotent. This file proves that inversion preserves that ideal and records the corresponding antipode closure statement needed to make it a Hopf ideal. The locally-connected hypothesis is automatic for a bundled finite-type coordinate Hopf algebra over a Noetherian base, through TauCeti.FiniteTypeCommHopfAlgCat.isNoetherianRing. For an unbundled H with Algebra.FiniteType k H, the user must first supply IsNoetherianRing H := Algebra.FiniteType.isNoetherianRing k H. Counit closure follows from the generic augmentation-component API; the remaining comultiplication statement is equivalent to closure of the component under the group multiplication.

The component here is the ordinary connected component over the ground field. The geometric identity component is obtained by applying the construction after base change to an algebraic closure; its descent and the component group are later parts of Layer 3.

Main declarations

• TauCeti.HopfAlgebra.antipode_connectedComponentIdempotent_augmentationPoint_eq_self: the antipode fixes the component idempotent of the augmentation point.
• TauCeti.HopfAlgebra.antipode_mem_connectedComponentIdeal_augmentationPoint_iff: antipode images belong to the augmentation point's component ideal exactly when their preimages do.
• TauCeti.HopfAlgebra.map_antipodeAlgHom_connectedComponentIdeal_augmentationPoint_eq_self: mapping the augmentation point's component ideal along the antipode fixes it.

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 next step is comultiplication closure and the resulting quotient Hopf algebra; geometric connectedness and the finite étale component group then remain.

@[simp]

theorem TauCeti.HopfAlgebra.antipode_connectedComponentIdempotent_augmentationPoint_eq_self {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [LocallyConnectedSpace (PrimeSpectrum H)] : (HopfAlgebraStruct.antipode k) (PrimeSpectrum.connectedComponentIdempotent (Bialgebra.augmentationPoint k H)) = PrimeSpectrum.connectedComponentIdempotent (Bialgebra.augmentationPoint k H)

The antipode fixes the component idempotent of the augmentation point.

@[simp]

theorem TauCeti.HopfAlgebra.map_antipodeAlgHom_connectedComponentIdeal_augmentationPoint_eq_self {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [LocallyConnectedSpace (PrimeSpectrum H)] : Ideal.map (HopfAlgebra.antipodeAlgHom k H) (PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H)) = PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H)

Mapping the ideal cutting out the augmentation point's connected component along the antipode fixes it. This is the ideal-theoretic form of inversion stability of the ordinary identity component.

@[simp]

theorem TauCeti.HopfAlgebra.antipode_mem_connectedComponentIdeal_augmentationPoint_iff {k : Type u} [Field k] {H : Type v} [CommRing H] [HopfAlgebra k H] [LocallyConnectedSpace (PrimeSpectrum H)] {x : H} : (HopfAlgebraStruct.antipode k) x ∈ PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H) ↔ x ∈ PrimeSpectrum.connectedComponentIdeal (Bialgebra.augmentationPoint k H)

An antipode image belongs to the ideal cutting out the augmentation point's connected component exactly when its preimage does.