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) ≌ HopfAlgCat R.

class CategoryTheory.HopfObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : C) extends CategoryTheory.BimonObj X :

Type v₁

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

one : MonoidalCategoryStruct.tensorUnit C ⟶ X
mul : MonoidalCategoryStruct.tensorObj X X ⟶ X
one_mul : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight one X) mul = (MonoidalCategoryStruct.leftUnitor X).hom
mul_one : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X one) mul = (MonoidalCategoryStruct.rightUnitor X).hom
mul_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul X) mul = CategoryStruct.comp (MonoidalCategoryStruct.associator X X X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X mul) mul)
counit : X ⟶ MonoidalCategoryStruct.tensorUnit C
comul : X ⟶ MonoidalCategoryStruct.tensorObj X X
counit_comul : CategoryStruct.comp comul (MonoidalCategoryStruct.whiskerRight counit X) = (MonoidalCategoryStruct.leftUnitor X).inv
comul_counit : CategoryStruct.comp comul (MonoidalCategoryStruct.whiskerLeft X counit) = (MonoidalCategoryStruct.rightUnitor X).inv
comul_assoc : CategoryStruct.comp comul (MonoidalCategoryStruct.whiskerLeft X comul) = CategoryStruct.comp comul (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight comul X) (MonoidalCategoryStruct.associator X X X).hom)
mul_comul : CategoryStruct.comp MonObj.mul ComonObj.comul = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (CategoryStruct.comp (MonoidalCategory.tensorμ X X X X) (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul))
one_comul : CategoryStruct.comp MonObj.one ComonObj.comul = MonObj.one
mul_counit : CategoryStruct.comp MonObj.mul ComonObj.counit = ComonObj.counit
one_counit : CategoryStruct.comp MonObj.one ComonObj.counit = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
antipode : X ⟶ X
The antipode is an endomorphism of the underlying object of the Hopf monoid.
antipode_left : CategoryStruct.comp ComonObj.comul (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight antipode X) MonObj.mul) = CategoryStruct.comp ComonObj.counit MonObj.one
antipode_right : CategoryStruct.comp ComonObj.comul (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X antipode) MonObj.mul) = CategoryStruct.comp ComonObj.counit MonObj.one

Instances

source

@[deprecated CategoryTheory.HopfObj (since := "2025-09-14")]

def CategoryTheory.Hopf_Class {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : C) :

Type v₁

Alias of CategoryTheory.HopfObj.

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

Equations

@CategoryTheory.Hopf_Class = @CategoryTheory.HopfObj

Instances For

source

def CategoryTheory.HopfObj.term𝒮 :

Lean.ParserDescr

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

Equations

CategoryTheory.HopfObj.term𝒮 = Lean.ParserDescr.node `CategoryTheory.HopfObj.term𝒮 1024 (Lean.ParserDescr.symbol "𝒮")

Instances For

source

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

Lean.ParserDescr

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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)

source

@[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)

source

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

source

@[deprecated CategoryTheory.Hopf (since := "2025-09-15")]

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

Type (max u₁ v₁)

Alias of CategoryTheory.Hopf.

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

Equations

CategoryTheory.Hopf_ = CategoryTheory.Hopf

Instances For

source

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.

Equations

A.toBimon = CategoryTheory.Bimon.mk' A.X

Instances For

source

@[deprecated CategoryTheory.Hopf.toBimon (since := "2025-09-15")]

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

Bimon C

Alias of CategoryTheory.Hopf.toBimon.

A Hopf monoid is a bimonoid.

Equations

@CategoryTheory.Hopf.toBimon_ = @CategoryTheory.Hopf.toBimon

Instances For

source

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.

Equations

CategoryTheory.Hopf.instCategory = inferInstanceAs (CategoryTheory.Category.{?u.28, max ?u.27 ?u.28} (CategoryTheory.InducedCategory (CategoryTheory.Bimon C) CategoryTheory.Hopf.toBimon))

source

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.

source

@[simp]

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

CategoryStruct.comp MonObj.one antipode = MonObj.one

source

@[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

source

@[simp]

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

CategoryStruct.comp antipode ComonObj.counit = ComonObj.counit

source

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

source

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

source

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.

source

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

source

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

source

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.

source

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)

source

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

CategoryStruct.comp antipode antipode = CategoryStruct.id A

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

Documentation

Mathlib.CategoryTheory.Monoidal.Hopf_

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

TODO #

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