Mathlib.CategoryTheory.Monoidal.Hopf

source

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

Type v₁

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

Instances

source

def Hopf_Class.term𝒮 :

Lean.ParserDescr

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

Equations

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

Instances For

source

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

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

source

@[simp]

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

CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X antipode) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h)) = CategoryTheory.CategoryStruct.comp Comon_Class.counit (CategoryTheory.CategoryStruct.comp Mon_Class.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 : Hopf_Class self.X

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

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 Hopf_Class.hom_antipode {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : C} [Hopf_Class A] [Hopf_Class B] (f : A ⟶ B) [IsBimon_Hom f] :

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

Morphisms of Hopf monoids intertwine the antipodes.

source

@[simp]

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

CategoryTheory.CategoryStruct.comp Mon_Class.one antipode = Mon_Class.one

source

@[simp]

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

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

source

@[simp]

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

CategoryTheory.CategoryStruct.comp antipode Comon_Class.counit = Comon_Class.counit

source

@[simp]

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

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

source

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

source

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

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

source

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

source

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

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

source

theorem Hopf_Class.antipode_antipode {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : C) [Hopf_Class A] (comm : CategoryTheory.CategoryStruct.comp (β_ A A).hom Mon_Class.mul = Mon_Class.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. #