Documentation

Mathlib.CategoryTheory.Monoidal.Bimon_

The category of bimonoids in a braided monoidal category. #

We define bimonoids in a braided monoidal category C as comonoid objects in the category of monoid objects in C.

We verify that this is equivalent to the monoid objects in the category of comonoid objects.

TODO #

Construct the category of modules, and show that it is monoidal with a monoidal forgetful functor to C.
Some form of Tannaka reconstruction: given a monoidal functor F : C ⥤ D into a braided category D, the internal endomorphisms of F form a bimonoid in presheaves on D, in good circumstances this is representable by a bimonoid in D, and then C is monoidally equivalent to the modules over that bimonoid.

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

Type v₁

A bimonoid object in a braided category C is a object that is simultaneously monoid and comonoid objects, and structure morphisms of them satisfy appropriate consistency conditions.

one : 𝟙_ C ⟶ M
mul : CategoryTheory.MonoidalCategory.tensorObj M M ⟶ M
one_mul' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.one M) Mon_Class.mul = (CategoryTheory.MonoidalCategory.leftUnitor M).hom
mul_one' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M Mon_Class.one) Mon_Class.mul = (CategoryTheory.MonoidalCategory.rightUnitor M).hom
mul_assoc' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.mul M) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M M M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M Mon_Class.mul) Mon_Class.mul)
counit : M ⟶ 𝟙_ C
comul : M ⟶ CategoryTheory.MonoidalCategory.tensorObj M M
counit_comul' : CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerRight Comon_Class.counit M) = (CategoryTheory.MonoidalCategory.leftUnitor M).inv
comul_counit' : CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerLeft M Comon_Class.counit) = (CategoryTheory.MonoidalCategory.rightUnitor M).inv
comul_assoc' : CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerLeft M Comon_Class.comul) = CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Comon_Class.comul M) (CategoryTheory.MonoidalCategory.associator M M M).hom)
mul_comul' : CategoryTheory.CategoryStruct.comp Mon_Class.mul Comon_Class.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom Comon_Class.comul Comon_Class.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.MonoidalCategory.tensorHom Mon_Class.mul Mon_Class.mul))
one_comul' : CategoryTheory.CategoryStruct.comp Mon_Class.one Comon_Class.comul = Mon_Class.one
mul_counit' : CategoryTheory.CategoryStruct.comp Mon_Class.mul Comon_Class.counit = Comon_Class.counit
one_counit' : CategoryTheory.CategoryStruct.comp Mon_Class.one Comon_Class.counit = CategoryTheory.CategoryStruct.id (𝟙_ C)

Instances

theorem Bimon_Class.one_comul'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} {M : C} [self : Bimon_Class M] {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj M M ⟶ Z) :

CategoryTheory.CategoryStruct.comp Mon_Class.one (CategoryTheory.CategoryStruct.comp Comon_Class.comul h) = CategoryTheory.CategoryStruct.comp Mon_Class.one h

theorem Bimon_Class.mul_counit'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} {M : C} [self : Bimon_Class M] {Z : C} (h : 𝟙_ C ⟶ Z) :

CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.comp Comon_Class.counit h) = CategoryTheory.CategoryStruct.comp Comon_Class.counit h

theorem Bimon_Class.one_counit'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} {M : C} [self : Bimon_Class M] {Z : C} (h : 𝟙_ C ⟶ Z) :

CategoryTheory.CategoryStruct.comp Mon_Class.one (CategoryTheory.CategoryStruct.comp Comon_Class.counit h) = h

theorem Bimon_Class.mul_comul'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} {M : C} [self : Bimon_Class M] {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj M M ⟶ Z) :

CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.comp Comon_Class.comul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom Comon_Class.comul Comon_Class.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom Mon_Class.mul Mon_Class.mul) h))

@[simp]

theorem Bimon_Class.mul_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] :

CategoryTheory.CategoryStruct.comp Mon_Class.mul Comon_Class.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom Comon_Class.comul Comon_Class.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.MonoidalCategory.tensorHom Mon_Class.mul Mon_Class.mul))

@[simp]

theorem Bimon_Class.mul_comul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj M M ⟶ Z) :

CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.comp Comon_Class.comul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom Comon_Class.comul Comon_Class.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom Mon_Class.mul Mon_Class.mul) h))

@[simp]

theorem Bimon_Class.one_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] :

CategoryTheory.CategoryStruct.comp Mon_Class.one Comon_Class.comul = Mon_Class.one

@[simp]

theorem Bimon_Class.one_comul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj M M ⟶ Z) :

CategoryTheory.CategoryStruct.comp Mon_Class.one (CategoryTheory.CategoryStruct.comp Comon_Class.comul h) = CategoryTheory.CategoryStruct.comp Mon_Class.one h

@[simp]

theorem Bimon_Class.mul_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] :

CategoryTheory.CategoryStruct.comp Mon_Class.mul Comon_Class.counit = Comon_Class.counit

@[simp]

theorem Bimon_Class.mul_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] {Z : C} (h : 𝟙_ C ⟶ Z) :

CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.comp Comon_Class.counit h) = CategoryTheory.CategoryStruct.comp Comon_Class.counit h

@[simp]

theorem Bimon_Class.one_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] :

CategoryTheory.CategoryStruct.comp Mon_Class.one Comon_Class.counit = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Bimon_Class.one_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] {Z : C} (h : 𝟙_ C ⟶ Z) :

CategoryTheory.CategoryStruct.comp Mon_Class.one (CategoryTheory.CategoryStruct.comp Comon_Class.counit h) = h

class IsBimon_Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [Bimon_Class M] [Bimon_Class N] (f : M ⟶ N) extends IsMon_Hom f, IsComon_Hom f :

The property that a morphism between bimonoid objects is a bimonoid morphism.

one_hom : CategoryTheory.CategoryStruct.comp Mon_Class.one f = Mon_Class.one
mul_hom : CategoryTheory.CategoryStruct.comp Mon_Class.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f f) Mon_Class.mul
hom_counit : CategoryTheory.CategoryStruct.comp f Comon_Class.counit = Comon_Class.counit
hom_comul : CategoryTheory.CategoryStruct.comp f Comon_Class.comul = CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategory.tensorHom f f)

Instances

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

Type (max (max u₁ v₁) v₁)

A bimonoid object in a braided category C is a comonoid object in the (monoidal) category of monoid objects in C.

Equations

Bimon_ C = Comon_ (Mon_ C)

Instances For

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

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

Equations

Bimon_.instCategory C = inferInstanceAs (CategoryTheory.Category.{?u.31, max ?u.30 ?u.31} (Comon_ (Mon_ C)))

theorem Bimon_.ext (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X Y : Bimon_ C} {f g : X ⟶ Y} (w : f.hom.hom = g.hom.hom) :

f = g

@[simp]

theorem Bimon_.id_hom' (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

(CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X

@[simp]

theorem Bimon_.comp_hom' (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N K : Bimon_ C} (f : M ⟶ N) (g : N ⟶ K) :

(CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

@[reducible, inline]

abbrev Bimon_.toMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Functor (Bimon_ C) (Mon_ C)

The forgetful functor from bimonoid objects to monoid objects.

Equations

Bimon_.toMon_ C = Comon_.forget (Mon_ C)

Instances For

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

CategoryTheory.Functor (Bimon_ C) C

The forgetful functor from bimonoid objects to the underlying category.

Equations

Bimon_.forget C = (Bimon_.toMon_ C).comp (Mon_.forget C)

Instances For

@[simp]

theorem Bimon_.toMon_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(Bimon_.toMon_ C).comp (Mon_.forget C) = Bimon_.forget C

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

CategoryTheory.Functor (Bimon_ C) (Comon_ C)

The forgetful functor from bimonoid objects to comonoid objects.

Equations

Bimon_.toComon_ C = (Mon_.forget C).mapComon

Instances For

@[simp]

theorem Bimon_.toComon__obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Comon_ (Mon_ C)) :

((Bimon_.toComon_ C).obj A).X = A.X.X

@[simp]

theorem Bimon_.toComon__obj_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Comon_ (Mon_ C)) :

((Bimon_.toComon_ C).obj A).comul = A.comul.hom

@[simp]

theorem Bimon_.toComon__obj_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Comon_ (Mon_ C)) :

((Bimon_.toComon_ C).obj A).counit = A.counit.hom

@[simp]

theorem Bimon_.toComon__map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : Comon_ (Mon_ C)} (f : X✝ ⟶ Y✝) :

((Bimon_.toComon_ C).map f).hom = f.hom.hom

@[simp]

theorem Bimon_.toComon_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(Bimon_.toComon_ C).comp (Comon_.forget C) = Bimon_.forget C

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

Mon_ (Comon_ C)

The object level part of the forward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

Equations

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

Instances For

@[simp]

theorem Bimon_.toMon_Comon_obj_one_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

(Bimon_.toMon_Comon_obj C M).one.hom = M.X.one

@[simp]

theorem Bimon_.toMon_Comon_obj_mul_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

(Bimon_.toMon_Comon_obj C M).mul.hom = M.X.mul

@[simp]

theorem Bimon_.toMon_Comon_obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

(Bimon_.toMon_Comon_obj C M).X = (Bimon_.toComon_ C).obj M

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

CategoryTheory.Functor (Bimon_ C) (Mon_ (Comon_ C))

The forward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

Equations

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

Instances For

@[simp]

theorem Bimon_.toMon_Comon__obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

(Bimon_.toMon_Comon_ C).obj M = Bimon_.toMon_Comon_obj C M

@[simp]

theorem Bimon_.toMon_Comon__map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : Bimon_ C} (f : X✝ ⟶ Y✝) :

((Bimon_.toMon_Comon_ C).map f).hom = (Bimon_.toComon_ C).map f

def Bimon_.ofMon_Comon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) :

The object level part of the backward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

Equations

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

Instances For

@[simp]

theorem Bimon_.ofMon_Comon_obj_comul_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) :

(Bimon_.ofMon_Comon_obj C M).comul.hom = M.X.comul

@[simp]

theorem Bimon_.ofMon_Comon_obj_counit_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) :

(Bimon_.ofMon_Comon_obj C M).counit.hom = M.X.counit

@[simp]

theorem Bimon_.ofMon_Comon_obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) :

(Bimon_.ofMon_Comon_obj C M).X = (Comon_.forget C).mapMon.obj M

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

CategoryTheory.Functor (Mon_ (Comon_ C)) (Bimon_ C)

The backward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

Equations

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

Instances For

@[simp]

theorem Bimon_.ofMon_Comon__obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) :

(Bimon_.ofMon_Comon_ C).obj M = Bimon_.ofMon_Comon_obj C M

@[simp]

theorem Bimon_.ofMon_Comon__map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : Mon_ (Comon_ C)} (f : X✝ ⟶ Y✝) :

((Bimon_.ofMon_Comon_ C).map f).hom = (Comon_.forget C).mapMon.map f

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

Bimon_ C ≌ Mon_ (Comon_ C)

The equivalence Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

Equations

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

Instances For

The trivial bimonoid #

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

The trivial bimonoid object.

Equations

Bimon_.trivial C = Comon_.trivial (Mon_ C)

Instances For

@[simp]

theorem Bimon_.trivial_counit_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(Bimon_.trivial C).counit.hom = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Bimon_.trivial_comul_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(Bimon_.trivial C).comul.hom = (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv

@[simp]

theorem Bimon_.trivial_X_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(Bimon_.trivial C).X.one = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Bimon_.trivial_X_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(Bimon_.trivial C).X.mul = (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom

@[simp]

theorem Bimon_.trivial_X_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(Bimon_.trivial C).X.X = 𝟙_ C

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

Bimon_.trivial C ⟶ A

The bimonoid morphism from the trivial bimonoid to any bimonoid.

Equations

Bimon_.trivialTo C A = { hom := default, hom_counit := ⋯, hom_comul := ⋯ }

Instances For

@[simp]

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

(Bimon_.trivialTo C A).hom = default

@[deprecated Bimon_.trivialTo]

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

Bimon_.trivial C ⟶ A

Alias of Bimon_.trivialTo.

The bimonoid morphism from the trivial bimonoid to any bimonoid.

Equations

Bimon_.trivial_to = Bimon_.trivialTo

Instances For

@[deprecated Bimon_.trivialTo_hom]

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

(Bimon_.trivialTo C A).hom = default

Alias of Bimon_.trivialTo_hom.

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

A ⟶ Bimon_.trivial C

The bimonoid morphism from any bimonoid to the trivial bimonoid.

Equations

Bimon_.toTrivial C A = default

Instances For

@[simp]

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

(Bimon_.toTrivial C A).hom = A.counit

@[deprecated Bimon_.toTrivial]

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

A ⟶ Bimon_.trivial C

Alias of Bimon_.toTrivial.

The bimonoid morphism from any bimonoid to the trivial bimonoid.

Equations

Bimon_.to_trivial = Bimon_.toTrivial

Instances For

@[deprecated Bimon_.toTrivial_hom]

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

(Bimon_.toTrivial C A).hom = A.counit

Alias of Bimon_.toTrivial_hom.

Additional lemmas #

theorem Bimon_.one_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

CategoryTheory.CategoryStruct.comp M.X.one M.comul.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorHom M.X.one M.X.one)

theorem Bimon_.one_comul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : (CategoryTheory.MonoidalCategory.tensorObj M.X M.X).X ⟶ Z) :

CategoryTheory.CategoryStruct.comp M.X.one (CategoryTheory.CategoryStruct.comp M.comul.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M.X.one M.X.one) h)

theorem Bimon_.mul_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

CategoryTheory.CategoryStruct.comp M.X.mul M.counit.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M.counit.hom M.counit.hom) (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ (Mon_ C)).X).hom

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

CategoryTheory.CategoryStruct.comp M.X.mul (CategoryTheory.CategoryStruct.comp M.counit.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M.counit.hom M.counit.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ (Mon_ C)).X).hom h)

@[simp]

theorem Bimon_.compatibility {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M.comul.hom M.comul.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X (CategoryTheory.MonoidalCategory.tensorObj M.X.X M.X.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X M.X.X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X (CategoryTheory.MonoidalCategory.whiskerRight (β_ M.X.X M.X.X).hom M.X.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X M.X.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X (CategoryTheory.MonoidalCategory.tensorObj M.X.X M.X.X)).inv (CategoryTheory.MonoidalCategory.tensorHom M.X.mul M.X.mul)))))) = CategoryTheory.CategoryStruct.comp M.X.mul M.comul.hom

Compatibility of the monoid and comonoid structures, in terms of morphisms in C.

@[simp]

theorem Bimon_.compatibility_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj M.X.X M.X.X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M.comul.hom M.comul.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X (CategoryTheory.MonoidalCategory.tensorObj M.X.X M.X.X)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X M.X.X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X (CategoryTheory.MonoidalCategory.whiskerRight (β_ M.X.X M.X.X).hom M.X.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X M.X.X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X (CategoryTheory.MonoidalCategory.tensorObj M.X.X M.X.X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M.X.mul M.X.mul) h)))))) = CategoryTheory.CategoryStruct.comp M.X.mul (CategoryTheory.CategoryStruct.comp M.comul.hom h)

@[simp]

theorem Bimon_.comul_counit_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X M.counit.hom) = (CategoryTheory.MonoidalCategory.rightUnitor M.X.X).inv

@[simp]

theorem Bimon_.comul_counit_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj M.X.X (𝟙_ (Mon_ C)).X ⟶ Z) :

CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X M.counit.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor M.X.X).inv h

@[simp]

theorem Bimon_.counit_comul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.MonoidalCategory.whiskerRight M.counit.hom M.X.X) = (CategoryTheory.MonoidalCategory.leftUnitor M.X.X).inv

@[simp]

theorem Bimon_.counit_comul_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ (Mon_ C)).X M.X.X ⟶ Z) :

CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight M.counit.hom M.X.X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor M.X.X).inv h

@[simp]

theorem Bimon_.comul_assoc_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X M.comul.hom) = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight M.comul.hom M.X.X) (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X M.X.X).hom)

@[simp]

theorem Bimon_.comul_assoc_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj M.X.X (CategoryTheory.MonoidalCategory.tensorObj M.X M.X).X ⟶ Z) :

CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X M.comul.hom) h) = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight M.comul.hom M.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X M.X.X).hom h))

theorem Bimon_.comul_assoc_flip_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) :

CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.MonoidalCategory.whiskerRight M.comul.hom M.X.X) = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X M.comul.hom) (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X M.X.X).inv)

theorem Bimon_.comul_assoc_flip_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj M.X M.X).X M.X.X ⟶ Z) :

CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight M.comul.hom M.X.X) h) = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M.X.X M.comul.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M.X.X M.X.X M.X.X).inv h))

theorem Bimon_.hom_comul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : Bimon_ C} (f : M ⟶ N) :

CategoryTheory.CategoryStruct.comp f.hom.hom N.comul.hom = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.MonoidalCategory.tensorHom f.hom.hom f.hom.hom)

theorem Bimon_.hom_comul_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : Bimon_ C} (f : M ⟶ N) {Z : C} (h : (CategoryTheory.MonoidalCategory.tensorObj N.X N.X).X ⟶ Z) :

CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp N.comul.hom h) = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.hom.hom f.hom.hom) h)

theorem Bimon_.hom_counit_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : Bimon_ C} (f : M ⟶ N) :

CategoryTheory.CategoryStruct.comp f.hom.hom N.counit.hom = M.counit.hom

theorem Bimon_.hom_counit_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : Bimon_ C} (f : M ⟶ N) {Z : C} (h : (𝟙_ (Mon_ C)).X ⟶ Z) :

CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp N.counit.hom h) = CategoryTheory.CategoryStruct.comp M.counit.hom h