Comonoid objects in a cartesian monoidal category. #
The category of comonoid objects in a cartesian monoidal category is equivalent to the category itself, via the forgetful functor.
def
cartesianComon_
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
CategoryTheory.Functor C (Comon_ C)
The functor from a cartesian monoidal category to comonoids in that category, equipping every object with the diagonal map as a comultiplication.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
counit_eq_toUnit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Comon_ C)
:
@[deprecated counit_eq_toUnit (since := "2025-05-09")]
theorem
counit_eq_from
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Comon_ C)
:
Alias of counit_eq_toUnit
.
@[simp]
theorem
comul_eq_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Comon_ C)
:
@[deprecated comul_eq_lift (since := "2025-05-09")]
theorem
comul_eq_diag
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Comon_ C)
:
Alias of comul_eq_lift
.
def
iso_cartesianComon_
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Comon_ C)
:
Every comonoid object in a cartesian monoidal category is equivalent to the canonical comonoid structure on the underlying object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
iso_cartesianComon__hom_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Comon_ C)
:
@[simp]
theorem
iso_cartesianComon__inv_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
(A : Comon_ C)
:
def
comonEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
The category of comonoid objects in a cartesian monoidal category is equivalent to the category itself, via the forgetful functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
comonEquiv_functor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
@[simp]
theorem
comonEquiv_counitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
comonEquiv.counitIso = CategoryTheory.NatIso.ofComponents
(fun (x : C) => CategoryTheory.Iso.refl (((cartesianComon_ C).comp (Comon_.forget C)).obj x)) ⋯
@[simp]
theorem
comonEquiv_unitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
:
comonEquiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (A : Comon_ C) => iso_cartesianComon_ A) ⋯
@[simp]
theorem
comonEquiv_inverse
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.CartesianMonoidalCategory C]
: