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

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

class IsBimonHom {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 IsMonHom f, IsComonHom 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)

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

def 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) : Prop

Alias of IsBimonHom.

---

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

Equations

• @IsBimon_Hom = @IsBimonHom

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)

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

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

Alias of Bimon.

---

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

Equations

• Bimon_ = Bimon

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)

@[deprecated Bimon.toMon (since := "2025-09-15")]

def Bimon.toMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (Bimon C) (Mon C)

Alias of Bimon.toMon.

---

The forgetful functor from bimonoid objects to monoid objects.

Equations

• Bimon.toMon_ = Bimon.toMon

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

@[deprecated Bimon.toComon (since := "2025-09-15")]

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

Alias of Bimon.toComon.

---

The forgetful functor from bimonoid objects to comonoid objects.

Equations

• Bimon.toComon_ = Bimon.toComon

@[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.toMonComonObj {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.toMonComonObj_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

@[simp]

theorem Bimon.toMonComonObj_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.toMonComonObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon C) : M.toMonComonObj.X = (toComon C).obj M

@[deprecated Bimon.toMonComonObj (since := "2025-09-15")]

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)

Alias of Bimon.toMonComonObj.

---

The object level part of the forward direction of Comon (Mon C) ≌ Mon (Comon C)

Equations

• @Bimon.toMon_Comon_obj = @Bimon.toMonComonObj

def Bimon.toMonComon (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.toMonComon C = { obj := Bimon.toMonComonObj, map := fun {X Y : Bimon C} (f : X ⟶ Y) => Mon.Hom.mk' ((Bimon.toComon C).map f) ⋯ ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem Bimon.toMonComon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : Bimon C} (f : X✝ ⟶ Y✝) : ((toMonComon C).map f).hom = (toComon C).map f

@[simp]

theorem Bimon.toMonComon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon C) : (toMonComon C).obj M = M.toMonComonObj

@[deprecated Bimon.toMonComon (since := "2025-09-15")]

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

Alias of Bimon.toMonComon.

---

The forward direction of Comon (Mon C) ≌ Mon (Comon C)

Equations

• Bimon.toMon_Comon_ = Bimon.toMonComon

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

Auxiliary definition for ofMonComonObj.

Equations

• Bimon.ofMonComonObjX M = (Comon.forget C).mapMon.obj M

@[simp]

theorem Bimon.ofMonComonObjX_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (ofMonComonObjX M).X = M.X.X

@[deprecated Bimon.ofMonComonObjX (since := "2025-09-15")]

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

Alias of Bimon.ofMonComonObjX.

---

Auxiliary definition for ofMonComonObj.

Equations

• @Bimon.ofMon_Comon_ObjX = @Bimon.ofMonComonObjX

@[simp]

theorem Bimon.ofMonComonObjX_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

@[deprecated Bimon.ofMonComonObjX_one (since := "2025-09-15")]

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

Alias of Bimon.ofMonComonObjX_one.

@[simp]

theorem Bimon.ofMonComonObjX_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

@[deprecated Bimon.ofMonComonObjX_mul (since := "2025-09-15")]

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

Alias of Bimon.ofMonComonObjX_mul.

def Bimon.ofMonComonObj {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.ofMonComonObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (ofMonComonObj M).X = ofMonComonObjX M

@[simp]

theorem Bimon.ofMonComonObj_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

@[simp]

theorem Bimon.ofMonComonObj_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

@[deprecated Bimon.ofMonComonObj (since := "2025-09-15")]

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

Alias of Bimon.ofMonComonObj.

---

The object level part of the backward direction of Comon (Mon C) ≌ Mon (Comon C)

Equations

• @Bimon.ofMon_Comon_Obj = @Bimon.ofMonComonObj

@[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.ofMonComon (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.ofMonComon C = { obj := Bimon.ofMonComonObj, 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.ofMonComon_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (ofMonComon C).obj M = ofMonComonObj M

@[simp]

theorem Bimon.ofMonComon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : Mon (Comon C)} (f : X✝ ⟶ Y✝) : ((ofMonComon C).map f).hom = (Comon.forget C).mapMon.map f

@[deprecated Bimon.ofMonComon (since := "2025-09-15")]

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)

Alias of Bimon.ofMonComon.

---

The backward direction of Comon (Mon C) ≌ Mon (Comon C)

Equations

• Bimon.ofMon_Comon_ = Bimon.ofMonComon

@[simp]

theorem Bimon.toMonComon_ofMonComon_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

@[deprecated Bimon.toMonComon_ofMonComon_obj_one (since := "2025-09-15")]

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

Alias of Bimon.toMonComon_ofMonComon_obj_one.

@[simp]

theorem Bimon.toMonComon_ofMonComon_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

@[deprecated Bimon.toMonComon_ofMonComon_obj_mul (since := "2025-09-15")]

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

Alias of Bimon.toMonComon_ofMonComon_obj_mul.

def Bimon.equivMonComonUnitIsoAppXAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon C) : M.X.X ≅ (((toMonComon C).comp (ofMonComon C)).obj M).X.X

Auxiliary definition for equivMonComonUnitIsoApp.

Equations

• M.equivMonComonUnitIsoAppXAux = CategoryTheory.Iso.refl M.X.X

@[simp]

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

@[simp]

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

@[deprecated Bimon.equivMonComonUnitIsoAppXAux (since := "2025-09-15")]

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 ≅ (((toMonComon C).comp (ofMonComon C)).obj M).X.X

Alias of Bimon.equivMonComonUnitIsoAppXAux.

---

Auxiliary definition for equivMonComonUnitIsoApp.

Equations

• @Bimon.equivMon_Comon_UnitIsoAppXAux = @Bimon.equivMonComonUnitIsoAppXAux

instance Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon C) : IsMonHom M.equivMonComonUnitIsoAppXAux.hom

def Bimon.equivMonComonUnitIsoAppX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon C) : M.X ≅ (((toMonComon C).comp (ofMonComon C)).obj M).X

Auxiliary definition for equivMonComonUnitIsoApp.

Equations

• M.equivMonComonUnitIsoAppX = Mon.mkIso M.equivMonComonUnitIsoAppXAux ⋯ ⋯

@[simp]

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

@[simp]

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

@[deprecated Bimon.equivMonComonUnitIsoAppX (since := "2025-09-15")]

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

Alias of Bimon.equivMonComonUnitIsoAppX.

---

Auxiliary definition for equivMonComonUnitIsoApp.

Equations

• @Bimon.equivMon_Comon_UnitIsoAppX = @Bimon.equivMonComonUnitIsoAppX

instance Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon C) : IsComonHom M.equivMonComonUnitIsoAppX.hom

def Bimon.equivMonComonUnitIsoApp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon C) : M ≅ ((toMonComon C).comp (ofMonComon C)).obj M

The unit for the equivalence Comon (Mon C) ≌ Mon (Comon C).

Equations

• M.equivMonComonUnitIsoApp = Comon.mkIso' M.equivMonComonUnitIsoAppX

@[simp]

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

@[simp]

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

@[deprecated Bimon.equivMonComonUnitIsoApp (since := "2025-09-15")]

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

Alias of Bimon.equivMonComonUnitIsoApp.

---

The unit for the equivalence Comon (Mon C) ≌ Mon (Comon C).

Equations

• @Bimon.equivMon_Comon_UnitIsoApp = @Bimon.equivMonComonUnitIsoApp

@[simp]

theorem Bimon.ofMonComon_toMonComon_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))

@[deprecated Bimon.ofMonComon_toMonComon_obj_counit (since := "2025-09-15")]

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

Alias of Bimon.ofMonComon_toMonComon_obj_counit.

@[simp]

theorem Bimon.ofMonComon_toMonComon_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))

@[deprecated Bimon.ofMonComon_toMonComon_obj_comul (since := "2025-09-15")]

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

Alias of Bimon.ofMonComon_toMonComon_obj_comul.

def Bimon.equivMonComonCounitIsoAppXAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (((ofMonComon C).comp (toMonComon C)).obj M).X.X ≅ M.X.X

Auxiliary definition for equivMonComonCounitIsoApp.

Equations

• Bimon.equivMonComonCounitIsoAppXAux M = CategoryTheory.Iso.refl (((Bimon.ofMonComon C).comp (Bimon.toMonComon C)).obj M).X.X

@[simp]

theorem Bimon.equivMonComonCounitIsoAppXAux_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (equivMonComonCounitIsoAppXAux M).inv = CategoryTheory.CategoryStruct.id M.X.X

@[simp]

theorem Bimon.equivMonComonCounitIsoAppXAux_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (equivMonComonCounitIsoAppXAux M).hom = CategoryTheory.CategoryStruct.id M.X.X

@[deprecated Bimon.equivMonComonCounitIsoAppXAux (since := "2025-09-15")]

def Bimon.equivMon_Comon_CounitIsoAppXAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (((ofMonComon C).comp (toMonComon C)).obj M).X.X ≅ M.X.X

Alias of Bimon.equivMonComonCounitIsoAppXAux.

---

Auxiliary definition for equivMonComonCounitIsoApp.

Equations

• @Bimon.equivMon_Comon_CounitIsoAppXAux = @Bimon.equivMonComonCounitIsoAppXAux

instance Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : IsComonHom (equivMonComonCounitIsoAppXAux M).hom

def Bimon.equivMonComonCounitIsoAppX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (((ofMonComon C).comp (toMonComon C)).obj M).X ≅ M.X

Auxiliary definition for equivMonComonCounitIsoApp.

Equations

• Bimon.equivMonComonCounitIsoAppX M = Comon.mkIso' (Bimon.equivMonComonCounitIsoAppXAux M)

@[simp]

theorem Bimon.equivMonComonCounitIsoAppX_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (equivMonComonCounitIsoAppX M).hom.hom = CategoryTheory.CategoryStruct.id M.X.X

@[simp]

theorem Bimon.equivMonComonCounitIsoAppX_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (equivMonComonCounitIsoAppX M).inv.hom = CategoryTheory.CategoryStruct.id M.X.X

@[deprecated Bimon.equivMonComonCounitIsoAppX (since := "2025-09-15")]

def Bimon.equivMon_Comon_CounitIsoAppX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (((ofMonComon C).comp (toMonComon C)).obj M).X ≅ M.X

Alias of Bimon.equivMonComonCounitIsoAppX.

---

Auxiliary definition for equivMonComonCounitIsoApp.

Equations

• @Bimon.equivMon_Comon_CounitIsoAppX = @Bimon.equivMonComonCounitIsoAppX

instance Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : IsMonHom (equivMonComonCounitIsoAppX M).hom

def Bimon.equivMonComonCounitIsoApp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : ((ofMonComon C).comp (toMonComon C)).obj M ≅ M

The counit for the equivalence Comon (Mon C) ≌ Mon (Comon C).

Equations

• Bimon.equivMonComonCounitIsoApp M = Mon.mkIso (Bimon.equivMonComonCounitIsoAppX M) ⋯ ⋯

@[simp]

theorem Bimon.equivMonComonCounitIsoApp_hom_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (equivMonComonCounitIsoApp M).hom.hom.hom = CategoryTheory.CategoryStruct.id M.X.X

@[simp]

theorem Bimon.equivMonComonCounitIsoApp_inv_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : (equivMonComonCounitIsoApp M).inv.hom.hom = CategoryTheory.CategoryStruct.id M.X.X

@[deprecated Bimon.equivMonComonCounitIsoApp (since := "2025-09-15")]

def Bimon.equivMon_Comon_CounitIsoApp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon (Comon C)) : ((ofMonComon C).comp (toMonComon C)).obj M ≅ M

Alias of Bimon.equivMonComonCounitIsoApp.

---

The counit for the equivalence Comon (Mon C) ≌ Mon (Comon C).

Equations

• @Bimon.equivMon_Comon_CounitIsoApp = @Bimon.equivMonComonCounitIsoApp

def Bimon.equivMonComon {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.

@[deprecated Bimon.equivMonComon (since := "2025-09-15")]

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

Alias of Bimon.equivMonComon.

---

The equivalence Comon (Mon C) ≌ Mon (Comon C)

Equations

• @Bimon.equivMon_Comon_ = @Bimon.equivMonComon

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

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

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