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 : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ M
• mul : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ M
• one_mul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one M) mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom
• mul_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M one) mul = (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom
• mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul M) mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M mul) mul)
• counit : M ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C
• comul : M ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M M
• counit_comul : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerRight counit M) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).inv
• comul_counit : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M counit) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv
• comul_assoc : CategoryTheory.CategoryStruct.comp comul (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M comul) = CategoryTheory.CategoryStruct.comp comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight comul M) (CategoryTheory.MonoidalCategoryStruct.associator M M M).hom)
• mul_comul : CategoryTheory.CategoryStruct.comp Mon_Class.mul Comon_Class.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.comul Comon_Class.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.MonoidalCategoryStruct.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 (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

@[simp]

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.MonoidalCategoryStruct.tensorObj M M ⟶ Z) : CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.comp Comon_Class.comul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.comul Comon_Class.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Mon_Class.mul Mon_Class.mul) h))

@[simp]

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 : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp Mon_Class.one (CategoryTheory.CategoryStruct.comp Comon_Class.counit h) = h

@[simp]

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.MonoidalCategoryStruct.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_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.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.comp Comon_Class.counit h) = CategoryTheory.CategoryStruct.comp Comon_Class.counit 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 : Prop

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.MonoidalCategoryStruct.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.MonoidalCategoryStruct.tensorHom f f)

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.

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)

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

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

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

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.

@[simp]

theorem Bimon_.toMon_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (toMon_ C).comp (Mon_.forget C) = 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.

@[simp]

theorem Bimon_.toComon__obj_comon_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Comon_ (Mon_ C)) : Comon_Class.comul = Comon_Class.comul.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)) : ((toComon_ C).obj A).X = A.X.X

@[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✝) : ((toComon_ C).map f).hom = f.hom.hom

@[simp]

theorem Bimon_.toComon__obj_comon_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Comon_ (Mon_ C)) : Comon_Class.counit = Comon_Class.counit.hom

@[simp]

theorem Bimon_.toComon_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (toComon_ C).comp (Comon_.forget C) = 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)

@[simp]

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

@[simp]

theorem Bimon_.toMon_Comon_obj_mon_one_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : Mon_Class.one.hom = Mon_Class.one

@[simp]

theorem Bimon_.toMon_Comon_obj_mon_mul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : Mon_Class.mul.hom = Mon_Class.mul

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)

@[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✝) : ((toMon_Comon_ C).map f).hom = (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) : (toMon_Comon_ C).obj M = M.toMon_Comon_obj

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

Auxiliary definition for ofMon_Comon_Obj.

@[simp]

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

@[simp]

theorem Bimon_.ofMon_Comon_ObjX_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : Mon_Class.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Mon_Class.one.hom

@[simp]

theorem Bimon_.ofMon_Comon_ObjX_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X.X M.X.X)) Mon_Class.mul.hom

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

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

@[simp]

theorem Bimon_.ofMon_Comon_Obj_comon_comul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : Comon_Class.comul.hom = Comon_Class.comul

@[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)) : (ofMon_Comon_Obj M).X = ofMon_Comon_ObjX M

@[simp]

theorem Bimon_.ofMon_Comon_Obj_comon_counit_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : Comon_Class.counit.hom = Comon_Class.counit

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)

@[simp]

theorem Bimon_.ofMon_Comon__obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (ofMon_Comon_ C).obj M = ofMon_Comon_Obj 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✝) : ((ofMon_Comon_ C).map f).hom = (Comon_.forget C).mapMon.map f

@[simp]

theorem Bimon_.toMon_Comon_ofMon_Comon_obj_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : Mon_Class.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) Mon_Class.one

@[simp]

theorem Bimon_.toMon_Comon_ofMon_Comon_obj_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X.X M.X.X)) Mon_Class.mul

def Bimon_.equivMon_Comon_UnitIsoAppXAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : M.X.X ≅ (((toMon_Comon_ C).comp (ofMon_Comon_ C)).obj M).X.X

Auxiliary definition for equivMon_Comon_UnitIsoApp.

@[simp]

theorem Bimon_.equivMon_Comon_UnitIsoAppXAux_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : M.equivMon_Comon_UnitIsoAppXAux.inv = CategoryTheory.CategoryStruct.id M.X.X

@[simp]

theorem Bimon_.equivMon_Comon_UnitIsoAppXAux_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : M.equivMon_Comon_UnitIsoAppXAux.hom = CategoryTheory.CategoryStruct.id M.X.X

instance Bimon_.instIsMon_HomHomEquivMon_Comon_UnitIsoAppXAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : IsMon_Hom M.equivMon_Comon_UnitIsoAppXAux.hom

def Bimon_.equivMon_Comon_UnitIsoAppX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : M.X ≅ (((toMon_Comon_ C).comp (ofMon_Comon_ C)).obj M).X

Auxiliary definition for equivMon_Comon_UnitIsoApp.

@[simp]

theorem Bimon_.equivMon_Comon_UnitIsoAppX_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : M.equivMon_Comon_UnitIsoAppX.hom.hom = CategoryTheory.CategoryStruct.id M.X.X

@[simp]

theorem Bimon_.equivMon_Comon_UnitIsoAppX_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : M.equivMon_Comon_UnitIsoAppX.inv.hom = CategoryTheory.CategoryStruct.id M.X.X

instance Bimon_.instIsComon_HomMon_HomEquivMon_Comon_UnitIsoAppX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : IsComon_Hom M.equivMon_Comon_UnitIsoAppX.hom

def Bimon_.equivMon_Comon_UnitIsoApp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : M ≅ ((toMon_Comon_ C).comp (ofMon_Comon_ C)).obj M

The unit for the equivalence Comon_ (Mon_ C) ≌ Mon_ (Comon_ C).

@[simp]

theorem Bimon_.equivMon_Comon_UnitIsoApp_hom_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : M.equivMon_Comon_UnitIsoApp.hom.hom.hom = CategoryTheory.CategoryStruct.id M.X.X

@[simp]

theorem Bimon_.equivMon_Comon_UnitIsoApp_inv_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : M.equivMon_Comon_UnitIsoApp.inv.hom.hom = CategoryTheory.CategoryStruct.id M.X.X

@[simp]

theorem Bimon_.ofMon_Comon_toMon_Comon_obj_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : Comon_Class.counit = CategoryTheory.CategoryStruct.comp Comon_Class.counit (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

@[simp]

theorem Bimon_.ofMon_Comon_toMon_Comon_obj_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : Comon_Class.comul = CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X.X M.X.X))

def Bimon_.equivMon_Comon_CounitIsoAppXAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (((ofMon_Comon_ C).comp (toMon_Comon_ C)).obj M).X.X ≅ M.X.X

Auxiliary definition for equivMon_Comon_CounitIsoApp.

@[simp]

theorem Bimon_.equivMon_Comon_CounitIsoAppXAux_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (equivMon_Comon_CounitIsoAppXAux M).hom = CategoryTheory.CategoryStruct.id M.X.X

@[simp]

theorem Bimon_.equivMon_Comon_CounitIsoAppXAux_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (equivMon_Comon_CounitIsoAppXAux M).inv = CategoryTheory.CategoryStruct.id M.X.X

instance Bimon_.instIsComon_HomHomEquivMon_Comon_CounitIsoAppXAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : IsComon_Hom (equivMon_Comon_CounitIsoAppXAux M).hom

def Bimon_.equivMon_Comon_CounitIsoAppX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (((ofMon_Comon_ C).comp (toMon_Comon_ C)).obj M).X ≅ M.X

Auxiliary definition for equivMon_Comon_CounitIsoApp.

@[simp]

theorem Bimon_.equivMon_Comon_CounitIsoAppX_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (equivMon_Comon_CounitIsoAppX M).inv.hom = CategoryTheory.CategoryStruct.id M.X.X

@[simp]

theorem Bimon_.equivMon_Comon_CounitIsoAppX_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (equivMon_Comon_CounitIsoAppX M).hom.hom = CategoryTheory.CategoryStruct.id M.X.X

instance Bimon_.instIsMon_HomComon_HomEquivMon_Comon_CounitIsoAppX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : IsMon_Hom (equivMon_Comon_CounitIsoAppX M).hom

def Bimon_.equivMon_Comon_CounitIsoApp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : ((ofMon_Comon_ C).comp (toMon_Comon_ C)).obj M ≅ M

The counit for the equivalence Comon_ (Mon_ C) ≌ Mon_ (Comon_ C).

@[simp]

theorem Bimon_.equivMon_Comon_CounitIsoApp_hom_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (equivMon_Comon_CounitIsoApp M).hom.hom.hom = CategoryTheory.CategoryStruct.id M.X.X

@[simp]

theorem Bimon_.equivMon_Comon_CounitIsoApp_inv_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (equivMon_Comon_CounitIsoApp M).inv.hom.hom = CategoryTheory.CategoryStruct.id M.X.X

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)

The trivial bimonoid

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

The trivial bimonoid object.

@[simp]

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

@[simp]

theorem Bimon_.trivial_X_mon_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Mon_Class.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem Bimon_.trivial_comon_comul_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Comon_Class.comul.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv

@[simp]

theorem Bimon_.trivial_X_mon_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Mon_Class.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom

@[simp]

theorem Bimon_.trivial_comon_counit_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Comon_Class.counit.hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

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

The bimonoid morphism from the trivial bimonoid to any bimonoid.

@[simp]

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

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

The bimonoid morphism from any bimonoid to the trivial bimonoid.

@[simp]

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

Additional lemmas

theorem Bimon_.Bimon_ClassAux_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : Comon_Class.counit = Comon_Class.counit.hom

theorem Bimon_.Bimon_ClassAux_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : Comon_Class.comul = Comon_Class.comul.hom

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

theorem Bimon_.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 = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom Mon_Class.one Mon_Class.one)

theorem Bimon_.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.MonoidalCategoryStruct.tensorObj M M ⟶ Z) : CategoryTheory.CategoryStruct.comp Mon_Class.one (CategoryTheory.CategoryStruct.comp Comon_Class.comul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Mon_Class.one Mon_Class.one) h)

theorem Bimon_.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 = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.counit Comon_Class.counit) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom

theorem Bimon_.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 : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.comp Comon_Class.counit h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.counit Comon_Class.counit) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom h)

@[simp]

theorem Bimon_.compatibility {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.comul Comon_Class.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M (CategoryTheory.MonoidalCategoryStruct.tensorObj M M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M M).hom M)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (CategoryTheory.MonoidalCategoryStruct.associator M M M).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M (CategoryTheory.MonoidalCategoryStruct.tensorObj M M)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom Mon_Class.mul Mon_Class.mul)))))) = CategoryTheory.CategoryStruct.comp Mon_Class.mul Comon_Class.comul

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 : C) [Bimon_Class M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Comon_Class.comul Comon_Class.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M (CategoryTheory.MonoidalCategoryStruct.tensorObj M M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M M).hom M)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M (CategoryTheory.MonoidalCategoryStruct.associator M M M).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M (CategoryTheory.MonoidalCategoryStruct.tensorObj M M)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom Mon_Class.mul Mon_Class.mul) h)))))) = CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.comp Comon_Class.comul h)

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

Auxiliary definition for Bimon_.mk'.

@[simp]

theorem Bimon_.mk'X_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) [Bimon_Class X] : (mk'X X).X = X

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

Construct an object of Bimon_ C from an object X : C and Bimon_Class X instance.

@[simp]

theorem Bimon_.mk'_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) [Bimon_Class X] : (mk' X).X = mk'X X