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 CategoryTheory.BimonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : C) extends CategoryTheory.MonObj M, CategoryTheory.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 : MonoidalCategoryStruct.tensorUnit C ⟶ M
• mul : MonoidalCategoryStruct.tensorObj M M ⟶ M
• one_mul : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight one M) mul = (MonoidalCategoryStruct.leftUnitor M).hom
• mul_one : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M one) mul = (MonoidalCategoryStruct.rightUnitor M).hom
• mul_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul M) mul = CategoryStruct.comp (MonoidalCategoryStruct.associator M M M).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M mul) mul)
• counit : M ⟶ MonoidalCategoryStruct.tensorUnit C
• comul : M ⟶ MonoidalCategoryStruct.tensorObj M M
• counit_comul : CategoryStruct.comp comul (MonoidalCategoryStruct.whiskerRight counit M) = (MonoidalCategoryStruct.leftUnitor M).inv
• comul_counit : CategoryStruct.comp comul (MonoidalCategoryStruct.whiskerLeft M counit) = (MonoidalCategoryStruct.rightUnitor M).inv
• comul_assoc : CategoryStruct.comp comul (MonoidalCategoryStruct.whiskerLeft M comul) = CategoryStruct.comp comul (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight comul M) (MonoidalCategoryStruct.associator M M M).hom)
• mul_comul : CategoryStruct.comp MonObj.mul ComonObj.comul = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (CategoryStruct.comp (MonoidalCategory.tensorμ M M M M) (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul))
• one_comul : CategoryStruct.comp MonObj.one ComonObj.comul = MonObj.one
• mul_counit : CategoryStruct.comp MonObj.mul ComonObj.counit = ComonObj.counit
• one_counit : CategoryStruct.comp MonObj.one ComonObj.counit = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

class CategoryTheory.IsBimonHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [BimonObj M] [BimonObj N] (f : M ⟶ N) extends CategoryTheory.IsMonHom f, CategoryTheory.IsComonHom f : Prop

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

• one_hom : CategoryStruct.comp MonObj.one f = MonObj.one
• mul_hom : CategoryStruct.comp MonObj.mul f = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom f f) MonObj.mul
• hom_counit : CategoryStruct.comp f ComonObj.counit = ComonObj.counit
• hom_comul : CategoryStruct.comp f ComonObj.comul = CategoryStruct.comp ComonObj.comul (MonoidalCategoryStruct.tensorHom f f)

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

• CategoryTheory.Bimon C = CategoryTheory.Comon (CategoryTheory.Mon C)

@[implicit_reducible]

instance CategoryTheory.Bimon.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Category.{v₁, max u₁ v₁} (Bimon C)

Equations

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

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

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

The forgetful functor from bimonoid objects to monoid objects.

Equations

• CategoryTheory.Bimon.toMon C = CategoryTheory.Comon.forget (CategoryTheory.Mon C)

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

The forgetful functor from bimonoid objects to the underlying category.

Equations

• CategoryTheory.Bimon.forget C = (CategoryTheory.Bimon.toMon C).comp (CategoryTheory.Mon.forget C)

@[simp]

theorem CategoryTheory.Bimon.toMon_forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : (toMon C).comp (Mon.forget C) = forget C

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

The forgetful functor from bimonoid objects to comonoid objects.

Equations

• CategoryTheory.Bimon.toComon C = (CategoryTheory.Mon.forget C).mapComon

@[simp]

theorem CategoryTheory.Bimon.toComon_obj_comon_comul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Comon (Mon C)) : ComonObj.comul = ComonObj.comul.hom

@[simp]

theorem CategoryTheory.Bimon.toComon_obj_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Comon (Mon C)) : ((toComon C).obj A).X = A.X.X

@[simp]

theorem CategoryTheory.Bimon.toComon_obj_comon_counit (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Comon (Mon C)) : ComonObj.counit = ComonObj.counit.hom

@[simp]

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

@[simp]

theorem CategoryTheory.Bimon.toComon_forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : (toComon C).comp (Comon.forget C) = forget C

def CategoryTheory.Bimon.toMonComonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [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 CategoryTheory.Bimon.toMonComonObj_mon_mul_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) : MonObj.mul.hom = MonObj.mul

@[simp]

theorem CategoryTheory.Bimon.toMonComonObj_mon_one_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) : MonObj.one.hom = MonObj.one

@[simp]

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

def CategoryTheory.Bimon.toMonComon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : 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 CategoryTheory.Bimon.toMonComon_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) : (toMonComon C).obj M = M.toMonComonObj

@[simp]

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

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

Auxiliary definition for ofMonComonObj.

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.Bimon.ofMonComonObjX_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) : MonObj.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) MonObj.one.hom

@[simp]

theorem CategoryTheory.Bimon.ofMonComonObjX_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) : MonObj.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj M.X.X M.X.X)) MonObj.mul.hom

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [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 CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) : M.equivMonComonUnitIsoAppXAux.hom = CategoryStruct.id M.X.X

@[simp]

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

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

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

Auxiliary definition for equivMonComonUnitIsoApp.

Equations

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

@[simp]

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

@[simp]

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

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

def CategoryTheory.Bimon.equivMonComonUnitIsoApp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [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 = CategoryTheory.Comon.mkIso' M.equivMonComonUnitIsoAppX

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) : ComonObj.counit = CategoryStruct.comp ComonObj.counit (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C))

@[simp]

theorem CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) : ComonObj.comul = CategoryStruct.comp ComonObj.comul (CategoryStruct.id (MonoidalCategoryStruct.tensorObj M.X.X M.X.X))

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

Auxiliary definition for equivMonComonCounitIsoApp.

Equations

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

@[simp]

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

@[simp]

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

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

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

Auxiliary definition for equivMonComonCounitIsoApp.

Equations

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

@[simp]

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

@[simp]

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

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

def CategoryTheory.Bimon.equivMonComonCounitIsoApp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Bimon.equivMonComon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [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 CategoryTheory.Bimon.trivial (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] : Bimon C

The trivial bimonoid object.

Equations

• CategoryTheory.Bimon.trivial C = CategoryTheory.Comon.trivial (CategoryTheory.Mon C)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The bimonoid morphism from the trivial bimonoid to any bimonoid.

Equations

• A.trivialTo = CategoryTheory.Comon.Hom.mk' default ⋯ ⋯

@[simp]

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

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

The bimonoid morphism from any bimonoid to the trivial bimonoid.

Equations

• A.toTrivial = default

@[simp]

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

Additional lemmas

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

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

@[implicit_reducible]

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

Equations

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

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

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

theorem CategoryTheory.Bimon.mul_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : C) [BimonObj M] : CategoryStruct.comp MonObj.mul ComonObj.counit = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.counit ComonObj.counit) (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

theorem CategoryTheory.Bimon.mul_counit_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : C) [BimonObj M] {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) : CategoryStruct.comp MonObj.mul (CategoryStruct.comp ComonObj.counit h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.counit ComonObj.counit) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom h)

@[simp]

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

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

@[simp]

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

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

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

Auxiliary definition for Bimon.mk'.

Equations

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

@[simp]

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

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