The category of bimonoids in a braided monoidal category.

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

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

TODO

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

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

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

• one : 𝟙_ C ⟶ M
• mul : CategoryTheory.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 ⟶ 𝟙_ 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 (𝟙_ C)

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

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

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

theorem Bimon_Class.mul_comul'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} {M : C} [self : Bimon_Class M] {Z : C} (h : CategoryTheory.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.mul_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] : CategoryTheory.CategoryStruct.comp Mon_Class.mul Comon_Class.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.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))

@[simp]

theorem Bimon_Class.mul_comul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] {Z : C} (h : CategoryTheory.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_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] : CategoryTheory.CategoryStruct.comp Mon_Class.one Comon_Class.comul = Mon_Class.one

@[simp]

theorem Bimon_Class.one_comul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] {Z : C} (h : CategoryTheory.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 {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] : CategoryTheory.CategoryStruct.comp Mon_Class.mul Comon_Class.counit = Comon_Class.counit

@[simp]

theorem Bimon_Class.mul_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] {Z : C} (h : 𝟙_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp Mon_Class.mul (CategoryTheory.CategoryStruct.comp Comon_Class.counit h) = CategoryTheory.CategoryStruct.comp Comon_Class.counit h

@[simp]

theorem Bimon_Class.one_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] : CategoryTheory.CategoryStruct.comp Mon_Class.one Comon_Class.counit = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Bimon_Class.one_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : C) [Bimon_Class M] {Z : C} (h : 𝟙_ C ⟶ Z) : CategoryTheory.CategoryStruct.comp Mon_Class.one (CategoryTheory.CategoryStruct.comp Comon_Class.counit h) = h

class IsBimon_Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : C} [Bimon_Class M] [Bimon_Class N] (f : M ⟶ N) extends IsMon_Hom f, IsComon_Hom f : 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.

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 C = inferInstanceAs (CategoryTheory.Category.{?u.35, max ?u.34 ?u.35} (Comon_ (Mon_ C)))

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

The forgetful functor from bimonoid objects to monoid objects.

Equations

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

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_comul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Comon_ (Mon_ C)) : ((toComon_ C).obj A).comul = A.comul.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_counit (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Comon_ (Mon_ C)) : ((toComon_ C).obj A).counit = A.counit.hom

@[simp]

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

@[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_one_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : (toMon_Comon_obj C M).one.hom = M.X.one

@[simp]

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

@[simp]

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

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

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

Equations

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

@[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 = toMon_Comon_obj C M

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

@[simp]

theorem Bimon_.ofMon_Comon_obj_counit_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Mon_ (Comon_ C)) : (ofMon_Comon_obj C M).counit.hom = M.X.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)

Equations

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

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

@[simp]

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

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

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

Equations

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

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

@[simp]

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

@[simp]

theorem Bimon_.trivial_counit_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (trivial C).counit.hom = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Bimon_.trivial_X_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (trivial C).X.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ C)).hom

@[simp]

theorem Bimon_.trivial_X_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (trivial C).X.one = CategoryTheory.CategoryStruct.id (𝟙_ 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

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

@[simp]

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

@[deprecated Bimon_.trivialTo (since := "2024-12-07")]

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

Alias of Bimon_.trivialTo.

---

The bimonoid morphism from the trivial bimonoid to any bimonoid.

Equations

• Bimon_.trivial_to = Bimon_.trivialTo

@[deprecated Bimon_.trivialTo_hom (since := "2024-12-07")]

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

Alias of Bimon_.trivialTo_hom.

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

The bimonoid morphism from any bimonoid to the trivial bimonoid.

Equations

• Bimon_.toTrivial C A = default

@[simp]

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

@[deprecated Bimon_.toTrivial (since := "2024-12-07")]

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

Alias of Bimon_.toTrivial.

---

The bimonoid morphism from any bimonoid to the trivial bimonoid.

Equations

• Bimon_.to_trivial = Bimon_.toTrivial

@[deprecated Bimon_.toTrivial_hom (since := "2024-12-07")]

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

Alias of Bimon_.toTrivial_hom.

Additional lemmas

theorem Bimon_.one_comul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : CategoryTheory.CategoryStruct.comp M.X.one M.comul.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom M.X.one M.X.one)

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

theorem Bimon_.mul_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : CategoryTheory.CategoryStruct.comp M.X.mul M.counit.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom M.counit.hom M.counit.hom) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ (Mon_ C)).X).hom

theorem Bimon_.mul_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : (𝟙_ (Mon_ C)).X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.X.mul (CategoryTheory.CategoryStruct.comp M.counit.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom M.counit.hom M.counit.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ (Mon_ C)).X).hom h)

@[simp]

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

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

@[simp]

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

@[simp]

theorem Bimon_.comul_counit_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X.X M.counit.hom) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X.X).inv

@[simp]

theorem Bimon_.comul_counit_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M.X.X (𝟙_ (Mon_ C)).X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X.X M.counit.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor M.X.X).inv h

@[simp]

theorem Bimon_.counit_comul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.counit.hom M.X.X) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X.X).inv

@[simp]

theorem Bimon_.counit_comul_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (𝟙_ (Mon_ C)).X M.X.X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.counit.hom M.X.X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.X.X).inv h

@[simp]

theorem Bimon_.comul_assoc_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X.X M.comul.hom) = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.comul.hom M.X.X) (CategoryTheory.MonoidalCategoryStruct.associator M.X.X M.X.X M.X.X).hom)

@[simp]

theorem Bimon_.comul_assoc_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M.X.X (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X M.X).X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X.X M.comul.hom) h) = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.comul.hom M.X.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X.X M.X.X M.X.X).hom h))

theorem Bimon_.comul_assoc_flip_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) : CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.comul.hom M.X.X) = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X.X M.comul.hom) (CategoryTheory.MonoidalCategoryStruct.associator M.X.X M.X.X M.X.X).inv)

theorem Bimon_.comul_assoc_flip_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (M : Bimon_ C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X M.X).X M.X.X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.comul.hom M.X.X) h) = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X.X M.comul.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X.X M.X.X M.X.X).inv h))

theorem Bimon_.hom_comul_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : Bimon_ C} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp f.hom.hom N.comul.hom = CategoryTheory.CategoryStruct.comp M.comul.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom.hom f.hom.hom)

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

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

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