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 BimonObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) extends MonObj M, ComonObj 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 MonObj.mul ComonObj.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul))
• one_comul : CategoryTheory.CategoryStruct.comp MonObj.one ComonObj.comul = MonObj.one
• mul_counit : CategoryTheory.CategoryStruct.comp MonObj.mul ComonObj.counit = ComonObj.counit
• one_counit : CategoryTheory.CategoryStruct.comp MonObj.one ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

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

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

Alias of BimonObj.

---

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.

Equations

• @Bimon_Class = @BimonObj

@[simp]

theorem BimonObj.one_comul_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (M : C) [self : BimonObj M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z) : CategoryTheory.CategoryStruct.comp MonObj.one (CategoryTheory.CategoryStruct.comp ComonObj.comul h) = CategoryTheory.CategoryStruct.comp MonObj.one h

@[simp]

theorem BimonObj.mul_counit_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (M : C) [self : BimonObj M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp MonObj.mul (CategoryTheory.CategoryStruct.comp ComonObj.counit h) = CategoryTheory.CategoryStruct.comp ComonObj.counit h

@[simp]

theorem BimonObj.one_counit_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (M : C) [self : BimonObj M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp MonObj.one (CategoryTheory.CategoryStruct.comp ComonObj.counit h) = h

@[simp]

theorem BimonObj.mul_comul_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} (M : C) [self : BimonObj M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z) : CategoryTheory.CategoryStruct.comp MonObj.mul (CategoryTheory.CategoryStruct.comp ComonObj.comul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul) h))

class IsBimon_Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [BimonObj M] [BimonObj 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 MonObj.one f = MonObj.one
• mul_hom : CategoryTheory.CategoryStruct.comp MonObj.mul f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f) MonObj.mul
• hom_counit : CategoryTheory.CategoryStruct.comp f ComonObj.counit = ComonObj.counit
• hom_comul : CategoryTheory.CategoryStruct.comp f ComonObj.comul = CategoryTheory.CategoryStruct.comp ComonObj.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.

Equations

• Bimon_ C = Comon_ (Mon_ 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)

Equations

• Bimon_.instCategory = inferInstanceAs (CategoryTheory.Category.{?u.24, max ?u.23 ?u.24} (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

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.

Equations

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

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)

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

Equations

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

@[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)) : ComonObj.counit = ComonObj.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)) : ((toComon_ C).obj A).X = A.X.X

@[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)) : ComonObj.comul = ComonObj.comul.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)

Equations

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

@[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) : MonObj.mul.hom = MonObj.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) : 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) : MonObj.one.hom = MonObj.one

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

• Bimon_.toMon_Comon_ C = { obj := Bimon_.toMon_Comon_obj, map := fun {X Y : Bimon_ C} (f : X ⟶ Y) => Mon_.Hom.mk' ((Bimon_.toComon_ C).map f) ⋯ ⋯, map_id := ⋯, map_comp := ⋯ }

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

Equations

• Bimon_.ofMon_Comon_ObjX M = (Comon_.forget C).mapMon.obj M

@[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)) : MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) MonObj.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)) : MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X.X M.X.X)) MonObj.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)

Equations

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

@[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_comul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : ComonObj.comul.hom = ComonObj.comul

@[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)) : ComonObj.counit.hom = ComonObj.counit

@[deprecated MonObj.tensorObj.mul_def (since := "2025-09-09")]

theorem Bimon_.Mon_Class.tensorObj.mul_def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [MonObj M] [MonObj N] : MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N) (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul)

Alias of MonObj.tensorObj.mul_def.

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

• Bimon_.ofMon_Comon_ C = { obj := Bimon_.ofMon_Comon_Obj, map := fun {X Y : Mon_ (Comon_ C)} (f : X ⟶ Y) => Comon_.Hom.mk' ((Comon_.forget C).mapMon.map f) ⋯ ⋯, map_id := ⋯, map_comp := ⋯ }

@[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) : MonObj.one = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) MonObj.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) : MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X.X M.X.X)) MonObj.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.

Equations

• M.equivMon_Comon_UnitIsoAppXAux = CategoryTheory.Iso.refl 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

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

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.

Equations

• M.equivMon_Comon_UnitIsoAppX = Mon_.mkIso M.equivMon_Comon_UnitIsoAppXAux ⋯ ⋯

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

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

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

Equations

• M.equivMon_Comon_UnitIsoApp = Comon_.mkIso' M.equivMon_Comon_UnitIsoAppX

@[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_.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_.ofMon_Comon_toMon_Comon_obj_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : ComonObj.counit = CategoryTheory.CategoryStruct.comp ComonObj.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)) : ComonObj.comul = CategoryTheory.CategoryStruct.comp ComonObj.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.

Equations

• Bimon_.equivMon_Comon_CounitIsoAppXAux M = CategoryTheory.Iso.refl (((Bimon_.ofMon_Comon_ C).comp (Bimon_.toMon_Comon_ C)).obj 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

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

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.

Equations

• Bimon_.equivMon_Comon_CounitIsoAppX M = Comon_.mkIso' (Bimon_.equivMon_Comon_CounitIsoAppXAux M)

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

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

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

Equations

• Bimon_.equivMon_Comon_CounitIsoApp M = Mon_.mkIso (Bimon_.equivMon_Comon_CounitIsoAppX M) ⋯ ⋯

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

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

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.

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.

Equations

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

@[simp]

theorem Bimon_.trivial_X_mon_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : MonObj.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] : ComonObj.counit.hom = CategoryTheory.CategoryStruct.id (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] : MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

@[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_comon_comul_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : ComonObj.comul.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv

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.

Equations

• A.trivialTo = Comon_.Hom.mk' default ⋯ ⋯

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

Equations

• A.toTrivial = default

@[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 = ComonObj.counit

Additional lemmas

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

@[deprecated Bimon_.BimonObjAux_counit (since := "2025-09-09")]

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

Alias of Bimon_.BimonObjAux_counit.

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

@[deprecated Bimon_.BimonObjAux_comul (since := "2025-09-09")]

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

Alias of Bimon_.BimonObjAux_comul.

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

Equations

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

theorem Bimon_.one_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [BimonObj M] : CategoryTheory.CategoryStruct.comp MonObj.one ComonObj.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.one MonObj.one)

theorem Bimon_.one_comul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [BimonObj M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z) : CategoryTheory.CategoryStruct.comp MonObj.one (CategoryTheory.CategoryStruct.comp ComonObj.comul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom MonObj.one MonObj.one) h)

theorem Bimon_.mul_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [BimonObj M] : CategoryTheory.CategoryStruct.comp MonObj.mul ComonObj.counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ComonObj.counit ComonObj.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) [BimonObj M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryTheory.CategoryStruct.comp MonObj.mul (CategoryTheory.CategoryStruct.comp ComonObj.counit h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ComonObj.counit ComonObj.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) [BimonObj M] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.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 MonObj.mul MonObj.mul)))))) = CategoryTheory.CategoryStruct.comp MonObj.mul ComonObj.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) [BimonObj M] {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.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 MonObj.mul MonObj.mul) h)))))) = CategoryTheory.CategoryStruct.comp MonObj.mul (CategoryTheory.CategoryStruct.comp ComonObj.comul h)

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

Auxiliary definition for Bimon_.mk'.

Equations

• Bimon_.mk'X X = { X := X, mon := inst✝.toMonObj }

@[simp]

theorem Bimon_.mk'X_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) [BimonObj 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) [BimonObj X] : Bimon_ C

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

Equations

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

@[simp]

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