Mathlib.CategoryTheory.Monoidal.Hopf

source

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

Type v₁

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

Instances

source

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

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

Type v₁

Alias of HopfObj.

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

Equations

@Hopf_Class = @HopfObj

Instances For

source

def HopfObj.term𝒮 :

Lean.ParserDescr

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

Equations

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

Instances For

source

def 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 HopfObj.antipode_left_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (X : C) [self : HopfObj X] {Z : C} (h : X ⟶ Z) :

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

source

@[simp]

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

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

source

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 : C
The underlying object in the ambient monoidal category
hopf : HopfObj self.X

Instances For

source

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

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

Type (max u₁ v₁)

Alias of Hopf.

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

Equations

Hopf_ = Hopf

Instances For

source

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

Bimon C

A Hopf monoid is a bimonoid.

Equations

A.toBimon = Bimon.mk' A.X

Instances For

source

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

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

Bimon C

Alias of Hopf.toBimon.

A Hopf monoid is a bimonoid.

Equations

@Hopf.toBimon_ = @Hopf.toBimon

Instances For

source

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 = inferInstanceAs (CategoryTheory.Category.{?u.24, max ?u.23 ?u.24} (CategoryTheory.InducedCategory (Bimon C) Hopf.toBimon))

source

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

CategoryTheory.CategoryStruct.comp f antipode = CategoryTheory.CategoryStruct.comp antipode f

Morphisms of Hopf monoids intertwine the antipodes.

source

@[simp]

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

CategoryTheory.CategoryStruct.comp MonObj.one antipode = MonObj.one

source

@[simp]

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

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

source

@[simp]

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

CategoryTheory.CategoryStruct.comp antipode ComonObj.counit = ComonObj.counit

source

@[simp]

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

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

source

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

source

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

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

source

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

source

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

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

source

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

CategoryTheory.CategoryStruct.comp antipode antipode = CategoryTheory.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. #