The category of Hopf monoids in a braided monoidal category. #
TODO #
- Show that in a cartesian monoidal category Hopf monoids are exactly group objects.
- Show that
Hopf_ (ModuleCat R) ≌ HopfAlgebraCat R
.
A Hopf monoid in a braided category C
is a bimonoid object in C
equipped with an antipode.
- X : Bimon_ C
The underlying bimonoid of a Hopf monoid.
- antipode : self.X.X.X ⟶ self.X.X.X
The antipode is an endomorphism of the underlying object of the Hopf monoid.
- antipode_left : CategoryTheory.CategoryStruct.comp self.X.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.antipode self.X.X.X) self.X.X.mul) = CategoryTheory.CategoryStruct.comp self.X.counit.hom self.X.X.one
- antipode_right : CategoryTheory.CategoryStruct.comp self.X.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X.X.X self.antipode) self.X.X.mul) = CategoryTheory.CategoryStruct.comp self.X.counit.hom self.X.X.one
Instances For
Morphisms of Hopf monoids are just morphisms of the underlying bimonoids. In fact they automatically intertwine the antipodes, proved below.
Equations
Morphisms of Hopf monoids intertwine the antipodes.
The antipode is an antihomomorphism with respect to both the monoid and comonoid structures. #
Auxiliary calculation for antipode_comul
.
This calculation calls for some ASCII art out of This Week's Finds.
| |
n n
| \ / |
| / |
| / \ |
| | S S
| | \ /
| | /
| | /
\ / \ /
v v
\ /
v
|
We move the left antipode up through the crossing,
the right antipode down through the crossing,
the right multiplication down across the strand,
reassociate the comultiplications,
then use antipode_right
then antipode_left
to simplify.
Auxiliary calculation for mul_antipode
.
|
n
/ \
| n
| / \
| S S
| \ /
n /
/ \ / \
| / |
\ / \ /
v v
| |
We move the leftmost multiplication up, so we can reassociate.
We then move the rightmost comultiplication under the strand,
and simplify using antipode_right
.
In a commutative Hopf algebra, the antipode squares to the identity.