The category of comonoids in a monoidal category. #
We define comonoids in a monoidal category C
,
and show that they are equivalently monoid objects in the opposite category.
We construct the monoidal structure on Comon_ C
, when C
is braided.
An oplax monoidal functor takes comonoid objects to comonoid objects.
That is, a oplax monoidal functor F : C ⥤ D
induces a functor Comon_ C ⥤ Comon_ D
.
TODO #
- Comonoid objects in
C
are "just" oplax monoidal functors from the trivial monoidal category toC
.
A comonoid object internal to a monoidal category.
When the monoidal category is preadditive, this is also sometimes called a "coalgebra object".
- X : C
The underlying object of a comonoid object.
- counit : self.X ⟶ 𝟙_ C
The counit of a comonoid object.
- comul : self.X ⟶ CategoryTheory.MonoidalCategory.tensorObj self.X self.X
The comultiplication morphism of a comonoid object.
- counit_comul : CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.MonoidalCategory.whiskerRight self.counit self.X) = (CategoryTheory.MonoidalCategory.leftUnitor self.X).inv
- comul_counit : CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.counit) = (CategoryTheory.MonoidalCategory.rightUnitor self.X).inv
- comul_assoc : CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.MonoidalCategory.whiskerLeft self.X self.comul) = CategoryTheory.CategoryStruct.comp self.comul (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.comul self.X) (CategoryTheory.MonoidalCategory.associator self.X self.X self.X).hom)
Instances For
The trivial comonoid object. We later show this is terminal in Comon_ C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Comon_.instInhabited C = { default := Comon_.trivial C }
A morphism of comonoid objects.
- hom : M.X ⟶ N.X
The underlying morphism of a morphism of comonoid objects.
- hom_counit : CategoryTheory.CategoryStruct.comp self.hom N.counit = M.counit
- hom_comul : CategoryTheory.CategoryStruct.comp self.hom N.comul = CategoryTheory.CategoryStruct.comp M.comul (CategoryTheory.MonoidalCategory.tensorHom self.hom self.hom)
Instances For
The identity morphism on a comonoid object.
Equations
- M.id = { hom := CategoryTheory.CategoryStruct.id M.X, hom_counit := ⋯, hom_comul := ⋯ }
Instances For
Equations
- M.homInhabited = { default := M.id }
Composition of morphisms of monoid objects.
Equations
- Comon_.comp f g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, hom_counit := ⋯, hom_comul := ⋯ }
Instances For
Equations
- Comon_.instCategory = CategoryTheory.Category.mk ⋯ ⋯ ⋯
The forgetful functor from comonoid objects to the ambient category.
Equations
- Comon_.forget C = { obj := fun (A : Comon_ C) => A.X, map := fun {X Y : Comon_ C} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- ⋯ = e
The forgetful functor from comonoid objects to the ambient category reflects isomorphisms.
Equations
- ⋯ = ⋯
Construct an isomorphism of comonoids by giving an isomorphism between the underlying objects and checking compatibility with counit and comultiplication only in the forward direction.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- A.uniqueHomToTrivial = { default := { hom := A.counit, hom_counit := ⋯, hom_comul := ⋯ }, uniq := ⋯ }
Equations
- ⋯ = ⋯
Turn a comonoid object into a monoid object in the opposite category.
Equations
- Comon_.Comon_ToMon_OpOp_obj' C A = { X := Opposite.op A.X, one := A.counit.op, mul := A.comul.op, one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
Instances For
The contravariant functor turning comonoid objects into monoid objects in the opposite category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Turn a monoid object in the opposite category into a comonoid object.
Equations
- Comon_.Mon_OpOpToComon_obj' C A = { X := Opposite.unop A.X, counit := A.one.unop, comul := A.mul.unop, counit_comul := ⋯, comul_counit := ⋯, comul_assoc := ⋯ }
Instances For
The contravariant functor turning monoid objects in the opposite category into comonoid objects.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Comonoid objects are contravariantly equivalent to monoid objects in the opposite category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Comonoid objects in a braided category form a monoidal category.
This definition is via transporting back and forth to monoids in the opposite category,
Equations
Preliminary statement of the comultiplication for a tensor product of comonoids.
This version is the definitional equality provided by transport, and not quite as good as
the version provided in tensorObj_comul
below.
The comultiplication on the tensor product of two comonoids is the tensor product of the comultiplications followed by the tensor strength (to shuffle the factors back into order).
The forgetful functor from Comon_ C
to C
is monoidal when C
is braided monoidal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A oplax monoidal functor takes comonoid objects to comonoid objects.
That is, a oplax monoidal functor F : C ⥤ D
induces a functor Comon_ C ⥤ Comon_ D
.
Equations
- One or more equations did not get rendered due to their size.