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 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_.forgetMonoidal C).toOplaxMonoidalFunctor.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_.trivial_to C A = { hom := default, hom_counit := ⋯, hom_comul := ⋯ }
Instances For
The bimonoid morphism from any bimonoid to the trivial bimonoid.
Equations
- Bimon_.to_trivial C A = default
Instances For
Additional lemmas #
Compatibility of the monoid and comonoid structures, in terms of morphisms in C
.