The augmentation point of a commutative bialgebra

The counit of a commutative bialgebra over a field defines a point of its prime spectrum. For a Hopf algebra, this is the identity point of the represented affine group.

Main declarations

• TauCeti.Bialgebra.augmentationPoint: the point of the affine spectrum defined by the counit.

@[reducible, inline]

abbrev TauCeti.Bialgebra.augmentationPoint (k : Type u) [Field k] (H : Type v) [CommRing H] [Bialgebra k H] : ↥(AlgebraicGeometry.Spec ↧H)

The point of Spec H defined by the counit of a commutative bialgebra. For a Hopf algebra, this is the identity point of the represented affine group.

Equations

• TauCeti.Bialgebra.augmentationPoint k H = TauCeti.AlgHom.kernelPoint (Bialgebra.counitAlgHom k H)