The augmentation point of a commutative Hopf algebra #
The antipode fixes the augmentation point of a commutative Hopf algebra. This is the prime-spectrum form of the identity saying that the counit composed with the antipode is the counit.
Main declarations #
TauCeti.HopfAlgebra.comap_antipodeAlgHom_augmentationPoint_eq_self: contraction along the antipode fixes the augmentation point.
theorem
TauCeti.HopfAlgebra.comap_antipodeAlgHom_augmentationPoint_eq_self
{k : Type u}
[Field k]
{H : Type v}
[CommRing H]
[HopfAlgebra k H]
:
Contraction along the antipode fixes the prime defined by the counit.