Documentation

def CategoryTheory.HopfObj.term𝒮 :

Lean.ParserDescr

The antipode is an endomorphism of the underlying object of the Hopf monoid.

Instances For

def CategoryTheory.HopfObj.«term𝒮[_]» :

Lean.ParserDescr

The antipode is an endomorphism of the underlying object of the Hopf monoid.

Instances For

@[simp]

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

CategoryStruct.comp ComonObj.comul (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X antipode) (CategoryStruct.comp MonObj.mul h)) = CategoryStruct.comp ComonObj.counit (CategoryStruct.comp MonObj.one h)

@[simp]

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

CategoryStruct.comp ComonObj.comul (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight antipode X) (CategoryStruct.comp MonObj.mul h)) = CategoryStruct.comp ComonObj.counit (CategoryStruct.comp MonObj.one h)

🔶 coverage

structure CategoryTheory.Hopf (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [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 : C
The underlying object in the ambient monoidal category
hopf : HopfObj self.X

Instances For

def CategoryTheory.Hopf.toBimon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Hopf C) :

Bimon C

A Hopf monoid is a bimonoid.

Instances For

@[implicit_reducible]

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

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.

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

CategoryStruct.comp f antipode = CategoryStruct.comp antipode f

Morphisms of Hopf monoids intertwine the antipodes.

CategoryStruct.comp MonObj.one antipode = MonObj.one

@[simp]

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

@[simp]

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

CategoryStruct.comp MonObj.one (CategoryStruct.comp antipode h) = CategoryStruct.comp MonObj.one h

CategoryStruct.comp antipode ComonObj.counit = ComonObj.counit

@[simp]

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

@[simp]

theorem CategoryTheory.HopfObj.antipode_counit_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : C) [HopfObj A] {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :

CategoryStruct.comp antipode (CategoryStruct.comp ComonObj.counit h) = CategoryStruct.comp ComonObj.counit h

The antipode is an antihomomorphism with respect to both the monoid and comonoid structures. #

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

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

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

CategoryStruct.comp antipode ComonObj.comul = CategoryStruct.comp ComonObj.comul (CategoryStruct.comp (β_ A A).hom (MonoidalCategoryStruct.tensorHom antipode antipode))

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

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

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

CategoryStruct.comp MonObj.mul antipode = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom antipode antipode) (CategoryStruct.comp (β_ A A).hom MonObj.mul)