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 categoryD
, the internal endomorphisms ofF
form a bimonoid in presheaves onD
, in good circumstances this is representable by a bimonoid inD
, and thenC
is monoidally equivalent to the modules over that bimonoid.
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.
- 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)
- 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))
Instances
Alias of BimonObj
.
A bimonoid object in a braided category C
is a object that is simultaneously monoid and comonoid
objects, and structure morphisms of them satisfy appropriate consistency conditions.
Equations
Instances For
The property that a morphism between bimonoid objects is a bimonoid morphism.
Instances
Alias of IsBimonHom
.
The property that a morphism between bimonoid objects is a bimonoid morphism.
Equations
Instances For
A bimonoid object in a braided category C
is a comonoid object in the (monoidal)
category of monoid objects in C
.
Instances For
Alias of Bimon
.
A bimonoid object in a braided category C
is a comonoid object in the (monoidal)
category of monoid objects in C
.
Instances For
The forgetful functor from bimonoid objects to monoid objects.
Equations
- Bimon.toMon C = Comon.forget (Mon C)
Instances For
Alias of Bimon.toMon
.
The forgetful functor from bimonoid objects to monoid objects.
Equations
Instances For
The forgetful functor from bimonoid objects to the underlying category.
Equations
- Bimon.forget C = (Bimon.toMon C).comp (Mon.forget C)
Instances For
The forgetful functor from bimonoid objects to comonoid objects.
Equations
- Bimon.toComon C = (Mon.forget C).mapComon
Instances For
Alias of Bimon.toComon
.
The forgetful functor from bimonoid objects to comonoid objects.
Equations
Instances For
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.
Instances For
Alias of Bimon.toMonComonObj
.
The object level part of the forward direction of Comon (Mon C) ≌ Mon (Comon C)
Equations
Instances For
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 := ⋯ }
Instances For
Alias of Bimon.toMonComon
.
The forward direction of Comon (Mon C) ≌ Mon (Comon C)
Equations
Instances For
Auxiliary definition for ofMonComonObj
.
Equations
- Bimon.ofMonComonObjX M = (Comon.forget C).mapMon.obj M
Instances For
Alias of Bimon.ofMonComonObjX
.
Auxiliary definition for ofMonComonObj
.
Equations
Instances For
Alias of Bimon.ofMonComonObjX_one
.
Alias of Bimon.ofMonComonObjX_mul
.
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.
Instances For
Alias of Bimon.ofMonComonObj
.
The object level part of the backward direction of Comon (Mon C) ≌ Mon (Comon C)
Equations
Instances For
Alias of MonObj.tensorObj.mul_def
.
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 := ⋯ }
Instances For
Alias of Bimon.ofMonComon
.
The backward direction of Comon (Mon C) ≌ Mon (Comon C)
Equations
Instances For
Alias of Bimon.toMonComon_ofMonComon_obj_one
.
Alias of Bimon.toMonComon_ofMonComon_obj_mul
.
Auxiliary definition for equivMonComonUnitIsoApp
.
Equations
Instances For
Alias of Bimon.equivMonComonUnitIsoAppXAux
.
Auxiliary definition for equivMonComonUnitIsoApp
.
Instances For
Auxiliary definition for equivMonComonUnitIsoApp
.
Equations
Instances For
Alias of Bimon.equivMonComonUnitIsoAppX
.
Auxiliary definition for equivMonComonUnitIsoApp
.
Instances For
The unit for the equivalence Comon (Mon C) ≌ Mon (Comon C)
.
Equations
Instances For
Alias of Bimon.equivMonComonUnitIsoApp
.
The unit for the equivalence Comon (Mon C) ≌ Mon (Comon C)
.
Instances For
Alias of Bimon.ofMonComon_toMonComon_obj_counit
.
Alias of Bimon.ofMonComon_toMonComon_obj_comul
.
Auxiliary definition for equivMonComonCounitIsoApp
.
Equations
Instances For
Alias of Bimon.equivMonComonCounitIsoAppXAux
.
Auxiliary definition for equivMonComonCounitIsoApp
.
Instances For
Auxiliary definition for equivMonComonCounitIsoApp
.
Instances For
Alias of Bimon.equivMonComonCounitIsoAppX
.
Auxiliary definition for equivMonComonCounitIsoApp
.
Instances For
The counit for the equivalence Comon (Mon C) ≌ Mon (Comon C)
.
Equations
Instances For
Alias of Bimon.equivMonComonCounitIsoApp
.
The counit for the equivalence Comon (Mon C) ≌ Mon (Comon C)
.
Instances For
The equivalence Comon (Mon C) ≌ Mon (Comon C)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of Bimon.equivMonComon
.
The equivalence Comon (Mon C) ≌ Mon (Comon C)
Equations
Instances For
The trivial bimonoid #
The trivial bimonoid object.
Equations
- Bimon.trivial C = Comon.trivial (Mon C)
Instances For
The bimonoid morphism from the trivial bimonoid to any bimonoid.
Equations
- A.trivialTo = Comon.Hom.mk' default ⋯ ⋯
Instances For
The bimonoid morphism from any bimonoid to the trivial bimonoid.
Instances For
Additional lemmas #
Alias of Bimon.BimonObjAux_counit
.
Alias of Bimon.BimonObjAux_comul
.
Equations
- One or more equations did not get rendered due to their size.
Compatibility of the monoid and comonoid structures, in terms of morphisms in C
.
Auxiliary definition for Bimon.mk'
.
Equations
- Bimon.mk'X X = { X := X, mon := inst✝.toMonObj }
Instances For
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.