Documentation

Mathlib.CategoryTheory.Monoidal.Hopf_

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.

structure Hopf_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

Type (max u₁ v₁)

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

@[simp]

theorem Hopf_.antipode_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (self : Hopf_ C) :

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

@[simp]

theorem Hopf_.antipode_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (self : Hopf_ C) :

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

@[simp]

theorem Hopf_.antipode_right_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (self : Hopf_ C) {Z : C} (h : self.X.X.X ⟶ Z) :

CategoryTheory.CategoryStruct.comp self.X.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft self.X.X.X self.antipode) (CategoryTheory.CategoryStruct.comp self.X.X.mul h)) = CategoryTheory.CategoryStruct.comp self.X.counit.hom (CategoryTheory.CategoryStruct.comp self.X.X.one h)

@[simp]

theorem Hopf_.antipode_left_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (self : Hopf_ C) {Z : C} (h : self.X.X.X ⟶ Z) :

CategoryTheory.CategoryStruct.comp self.X.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.antipode self.X.X.X) (CategoryTheory.CategoryStruct.comp self.X.X.mul h)) = CategoryTheory.CategoryStruct.comp self.X.counit.hom (CategoryTheory.CategoryStruct.comp self.X.X.one h)

instance Hopf_.instCategory (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Category.{v₁, max u₁ v₁} (Hopf_ C)

Morphisms of Hopf monoids are just morphisms of the underlying bimonoids. In fact they automatically intertwine the antipodes, proved below.

Equations

Hopf_.instCategory C = inferInstanceAs (CategoryTheory.Category.{?u.31, max ?u.30 ?u.31} (CategoryTheory.InducedCategory (Bimon_ C) Hopf_.X))

theorem Hopf_.hom_antipode {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A : Hopf_ C} {B : Hopf_ C} (f : A ⟶ B) :

CategoryTheory.CategoryStruct.comp f.hom.hom B.antipode = CategoryTheory.CategoryStruct.comp A.antipode f.hom.hom

Morphisms of Hopf monoids intertwine the antipodes.

@[simp]

theorem Hopf_.one_antipode_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) {Z : C} (h : A.X.X.X ⟶ Z) :

CategoryTheory.CategoryStruct.comp A.X.X.one (CategoryTheory.CategoryStruct.comp A.antipode h) = CategoryTheory.CategoryStruct.comp A.X.X.one h

@[simp]

theorem Hopf_.one_antipode {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :

CategoryTheory.CategoryStruct.comp A.X.X.one A.antipode = A.X.X.one

@[simp]

theorem Hopf_.antipode_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) {Z : C} (h : (𝟙_ (Mon_ C)).X ⟶ Z) :

CategoryTheory.CategoryStruct.comp A.antipode (CategoryTheory.CategoryStruct.comp A.X.counit.hom h) = CategoryTheory.CategoryStruct.comp A.X.counit.hom h

@[simp]

theorem Hopf_.antipode_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :

CategoryTheory.CategoryStruct.comp A.antipode A.X.counit.hom = A.X.counit.hom

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) :

CategoryTheory.CategoryStruct.comp A.X.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight A.antipode A.X.X.X) (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.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))

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_.antipode_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :

CategoryTheory.CategoryStruct.comp A.antipode A.X.comul.hom = CategoryTheory.CategoryStruct.comp A.X.comul.hom (CategoryTheory.CategoryStruct.comp (β_ A.X.X.X A.X.X.X).hom (CategoryTheory.MonoidalCategory.tensorHom A.antipode A.antipode))

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.

theorem Hopf_.mul_antipode {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) :

CategoryTheory.CategoryStruct.comp A.X.X.mul A.antipode = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.antipode A.antipode) (CategoryTheory.CategoryStruct.comp (β_ A.X.X.X A.X.X.X).hom A.X.X.mul)

theorem Hopf_.antipode_antipode {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Hopf_ C) (comm : CategoryTheory.CategoryStruct.comp (β_ A.X.X.X A.X.X.X).hom A.X.X.mul = A.X.X.mul) :

CategoryTheory.CategoryStruct.comp A.antipode A.antipode = CategoryTheory.CategoryStruct.id A.X.X.X

In a commutative Hopf algebra, the antipode squares to the identity.