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.
- one_mul' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.one M) Mon_Class.mul = (CategoryTheory.MonoidalCategory.leftUnitor M).hom
- mul_one' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M Mon_Class.one) Mon_Class.mul = (CategoryTheory.MonoidalCategory.rightUnitor M).hom
- mul_assoc' : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Mon_Class.mul M) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M M M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft M Mon_Class.mul) Mon_Class.mul)
- counit_comul' : CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerRight Comon_Class.counit M) = (CategoryTheory.MonoidalCategory.leftUnitor M).inv
- comul_counit' : CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerLeft M Comon_Class.counit) = (CategoryTheory.MonoidalCategory.rightUnitor M).inv
- comul_assoc' : CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.MonoidalCategory.whiskerLeft M Comon_Class.comul) = CategoryTheory.CategoryStruct.comp Comon_Class.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight Comon_Class.comul M) (CategoryTheory.MonoidalCategory.associator M M M).hom)
- mul_comul' : CategoryTheory.CategoryStruct.comp Mon_Class.mul Comon_Class.comul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom Comon_Class.comul Comon_Class.comul) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M M M M) (CategoryTheory.MonoidalCategory.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)
Instances
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.MonoidalCategory.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.MonoidalCategory.tensorHom f f)
Instances
A bimonoid object in a braided category C
is a comonoid object in the (monoidal)
category of monoid objects in C
.
Instances For
Equations
The forgetful functor from bimonoid objects to monoid objects.
Equations
- Bimon_.toMon_ C = Comon_.forget (Mon_ C)
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
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
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
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
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
The equivalence Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)
Equations
- One or more equations did not get rendered due to their size.
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
- Bimon_.trivialTo C A = { hom := default, hom_counit := ⋯, hom_comul := ⋯ }
Instances For
Alias of Bimon_.trivialTo
.
The bimonoid morphism from the trivial bimonoid to any bimonoid.
Equations
Instances For
Alias of Bimon_.trivialTo_hom
.
The bimonoid morphism from any bimonoid to the trivial bimonoid.
Equations
- Bimon_.toTrivial C A = default
Instances For
Alias of Bimon_.toTrivial
.
The bimonoid morphism from any bimonoid to the trivial bimonoid.
Equations
Instances For
Alias of Bimon_.toTrivial_hom
.
Additional lemmas #
Compatibility of the monoid and comonoid structures, in terms of morphisms in C
.