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 CategoryTheory.cartesianComon (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] : 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.

@[deprecated CategoryTheory.cartesianComon (since := "2025-09-15")]

def CategoryTheory.cartesianComon_ (C : Type u) [Category.{v, u} C] [CartesianMonoidalCategory C] : Functor C (Comon C)

Alias of CategoryTheory.cartesianComon.

---

The functor from a Cartesian monoidal category to comonoids in that category, equipping every object with the diagonal map as a comultiplication.

@[simp]

theorem CategoryTheory.counit_eq_toUnit {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : C) [ComonObj A] : ComonObj.counit = SemiCartesianMonoidalCategory.toUnit A

@[simp]

theorem CategoryTheory.comul_eq_lift {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : C) [ComonObj A] : ComonObj.comul = CartesianMonoidalCategory.lift (CategoryStruct.id A) (CategoryStruct.id A)

def CategoryTheory.isoCartesianComon {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : Comon C) : A ≅ (cartesianComon C).obj A.X

Every comonoid object in a Cartesian monoidal category is equivalent to the canonical comonoid structure on the underlying object.

@[simp]

theorem CategoryTheory.isoCartesianComon_inv_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : Comon C) : (isoCartesianComon A).inv.hom = CategoryStruct.id ((cartesianComon C).obj A.X).X

@[simp]

theorem CategoryTheory.isoCartesianComon_hom_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : Comon C) : (isoCartesianComon A).hom.hom = CategoryStruct.id A.X

@[deprecated CategoryTheory.isoCartesianComon (since := "2025-09-15")]

def CategoryTheory.iso_cartesianComon_ {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : Comon C) : A ≅ (cartesianComon C).obj A.X

Alias of CategoryTheory.isoCartesianComon.

---

Every comonoid object in a Cartesian monoidal category is equivalent to the canonical comonoid structure on the underlying object.

def CategoryTheory.comonEquiv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : Comon C ≌ C

The category of comonoid objects in a Cartesian monoidal category is equivalent to the category itself, via the forgetful functor.

@[simp]

theorem CategoryTheory.comonEquiv_counitIso {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : comonEquiv.counitIso = NatIso.ofComponents (fun (x : C) => Iso.refl (((cartesianComon C).comp (Comon.forget C)).obj x)) ⋯

@[simp]

theorem CategoryTheory.comonEquiv_unitIso {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : comonEquiv.unitIso = NatIso.ofComponents isoCartesianComon ⋯

@[simp]

theorem CategoryTheory.comonEquiv_inverse {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : comonEquiv.inverse = cartesianComon C

@[simp]

theorem CategoryTheory.comonEquiv_functor {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : comonEquiv.functor = Comon.forget C