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.

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_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X : Bimon_ C} {Y : Bimon_ C} {f : X ⟶ Y} {g : X ⟶ Y} :

f = g ↔ f.hom.hom = g.hom.hom

theorem Bimon_.ext (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X : Bimon_ C} {Y : Bimon_ C} {f : X ⟶ Y} {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 : Bimon_ C} {N : Bimon_ C} {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

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

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_.forgetMonoidal C).toOplaxMonoidalFunctor.mapComon

Instances For

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

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

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

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_.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_.forgetMonoidal C).mapMon.obj M

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

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 (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_.forgetMonoidal C).mapMon.map f

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

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 #

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

(Bimon_.trivial C).X.X = 𝟙_ 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_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

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

(Bimon_.trivial_to C A).hom = default

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

The bimonoid morphism from the trivial bimonoid to any bimonoid.

Equations

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

Instances For

@[simp]

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

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

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

The bimonoid morphism from any bimonoid to the trivial bimonoid.

Equations

Bimon_.to_trivial C A = default

Instances For

Additional lemmas #

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

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

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

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

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_.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_.hom_comul_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : Bimon_ C} {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_comul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : Bimon_ C} {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_counit_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M : Bimon_ C} {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

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

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