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 ⥤ Dinto a braided categoryD, the internal endomorphisms ofFform a bimonoid in presheaves onD, in good circumstances this is representable by a bimonoid inD, and thenCis 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_comul : CategoryStruct.comp MonObj.one ComonObj.comul = MonObj.one
- mul_counit : CategoryStruct.comp MonObj.mul ComonObj.counit = ComonObj.counit
Instances
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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 :
The property that a morphism between bimonoid objects is a bimonoid morphism.
Instances
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.
Instances For
@[implicit_reducible]
instance
CategoryTheory.Bimon.instCategory
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
:
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}
:
@[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]
:
The forgetful functor from bimonoid objects to monoid objects.
Instances For
def
CategoryTheory.Bimon.forget
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
:
The forgetful functor from bimonoid objects to the underlying category.
Instances For
@[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]
:
The forgetful functor from bimonoid objects to comonoid objects.
Instances For
@[simp]
theorem
CategoryTheory.Bimon.toComon_obj_comon_counit
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(A : Comon (Mon C))
:
@[simp]
theorem
CategoryTheory.Bimon.toComon_obj_comon_comul
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(A : Comon (Mon C))
:
@[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✝)
:
@[simp]
theorem
CategoryTheory.Bimon.toComon_obj_X
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(A : Comon (Mon C))
:
@[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)
:
The object level part of the forward direction of Comon (Mon C) ≌ Mon (Comon C)
Instances For
@[simp]
theorem
CategoryTheory.Bimon.toMonComonObj_mon_one_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
@[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
@[simp]
theorem
CategoryTheory.Bimon.toMonComonObj_mon_mul_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
def
CategoryTheory.Bimon.toMonComon
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
:
The forward direction of Comon (Mon C) ≌ Mon (Comon C)
Instances For
@[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
@[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
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.
Instances For
@[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))
:
@[simp]
theorem
CategoryTheory.Bimon.ofMonComonObjX_mul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
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)
Instances For
@[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_comul_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
@[simp]
theorem
CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
def
CategoryTheory.Bimon.ofMonComon
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
:
The backward direction of Comon (Mon C) ≌ Mon (Comon C)
Instances For
@[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)
:
@[simp]
theorem
CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
def
CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
Auxiliary definition for equivMonComonUnitIsoApp.
Instances For
@[simp]
theorem
CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
@[simp]
theorem
CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
instance
CategoryTheory.Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
def
CategoryTheory.Bimon.equivMonComonUnitIsoAppX
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
Auxiliary definition for equivMonComonUnitIsoApp.
Instances For
@[simp]
theorem
CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
@[simp]
theorem
CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
instance
CategoryTheory.Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
def
CategoryTheory.Bimon.equivMonComonUnitIsoApp
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
The unit for the equivalence Comon (Mon C) ≌ Mon (Comon C).
Instances For
@[simp]
theorem
CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
@[simp]
theorem
CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
@[simp]
theorem
CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
@[simp]
theorem
CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
def
CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
Auxiliary definition for equivMonComonCounitIsoApp.
Instances For
@[simp]
theorem
CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
@[simp]
theorem
CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
instance
CategoryTheory.Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
def
CategoryTheory.Bimon.equivMonComonCounitIsoAppX
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
Auxiliary definition for equivMonComonCounitIsoApp.
Instances For
@[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
@[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
instance
CategoryTheory.Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
def
CategoryTheory.Bimon.equivMonComonCounitIsoApp
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Mon (Comon C))
:
The counit for the equivalence Comon (Mon C) ≌ Mon (Comon C).
Instances For
@[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
@[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
def
CategoryTheory.Bimon.equivMonComon
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
:
The equivalence Comon (Mon C) ≌ Mon (Comon C)
Instances For
The trivial bimonoid #
def
CategoryTheory.Bimon.trivial
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
:
Bimon C
The trivial bimonoid object.
Instances For
@[simp]
theorem
CategoryTheory.Bimon.trivial_X_mon_one
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
:
@[simp]
theorem
CategoryTheory.Bimon.trivial_X_mon_mul
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
:
@[simp]
theorem
CategoryTheory.Bimon.trivial_comon_counit_hom
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory 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_comon_comul_hom
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
:
def
CategoryTheory.Bimon.trivialTo
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(A : Bimon C)
:
The bimonoid morphism from the trivial bimonoid to any bimonoid.
Instances For
@[simp]
theorem
CategoryTheory.Bimon.trivialTo_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(A : Bimon C)
:
def
CategoryTheory.Bimon.toTrivial
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(A : Bimon C)
:
The bimonoid morphism from any bimonoid to the trivial bimonoid.
Instances For
@[simp]
theorem
CategoryTheory.Bimon.toTrivial_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(A : Bimon C)
:
Additional lemmas #
theorem
CategoryTheory.Bimon.BimonObjAux_counit
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
theorem
CategoryTheory.Bimon.BimonObjAux_comul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
@[implicit_reducible]
instance
CategoryTheory.Bimon.instBimonObjXXMon
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : Bimon C)
:
theorem
CategoryTheory.Bimon.one_comul
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : C)
[BimonObj M]
:
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)
:
theorem
CategoryTheory.Bimon.mul_counit
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(M : C)
[BimonObj M]
:
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)
:
@[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'.
Instances For
@[simp]
theorem
CategoryTheory.Bimon.mk'X_X
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(X : C)
[BimonObj 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.
Instances For
@[simp]
theorem
CategoryTheory.Bimon.mk'_X
{C : Type u₁}
[Category.{v₁, u₁} C]
[MonoidalCategory C]
[BraidedCategory C]
(X : C)
[BimonObj X]
: