Documentation

Mathlib.CategoryTheory.Monoidal.Hopf_

The category of Hopf monoids in a braided monoidal category. #

TODO #

A Hopf monoid in a braided category C is a bimonoid object in C equipped with an antipode.

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. #

    theorem Hopf_.antipode_comul₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
    theorem Hopf_.antipode_comul₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
    CategoryTheory.CategoryStruct.comp A.X.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.X.comul.hom A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X A.X.comul.hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (β_ A.X.X.X A.X.X.X).hom)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.tensorHom A.antipode A.antipode))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerRight (β_ A.X.X.X A.X.X.X).hom A.X.X.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X)).inv (CategoryTheory.MonoidalCategory.tensorHom A.X.X.mul A.X.X.mul)))))))))) = CategoryTheory.CategoryStruct.comp A.X.counit.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom A.X.X.one A.X.X.one))

    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.

    theorem Hopf_.mul_antipode₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.X.comul.hom A.X.comul.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerRight (β_ A.X.X.X A.X.X.X).hom A.X.X.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X) A.X.X.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight A.X.X.mul A.X.X.X) A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight A.antipode A.X.X.X) A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X A.X.X.mul) A.X.X.mul))))))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.X.counit.hom A.X.counit.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom A.X.X.one)
    theorem Hopf_.mul_antipode₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.X.comul.hom A.X.comul.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.whiskerRight (β_ A.X.X.X A.X.X.X).hom A.X.X.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X (CategoryTheory.MonoidalCategory.tensorObj A.X.X.X A.X.X.X) A.X.X.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).inv A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.whiskerRight A.X.X.mul A.X.X.X) A.X.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X.X.X A.X.X.X A.X.X.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (β_ A.X.X.X A.X.X.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X (CategoryTheory.MonoidalCategory.tensorHom A.antipode A.antipode)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A.X.X.X A.X.X.mul) A.X.X.mul)))))))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.X.counit.hom A.X.counit.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom A.X.X.one)

    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.