Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

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.

source
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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.counit_eq_toUnit {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (A : C) [ComonObj A] :
    ComonObj.counit = SemiCartesianMonoidalCategory.toUnit A
    source
    @[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)
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[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
      source
      @[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
      source
      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.comonEquiv_unitIso {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] :
        comonEquiv.unitIso = NatIso.ofComponents isoCartesianComon ⋯
        source
        @[simp]
        theorem CategoryTheory.comonEquiv_functor {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] :
        comonEquiv.functor = Comon.forget C
        source
        @[simp]
        theorem CategoryTheory.comonEquiv_inverse {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] :
        comonEquiv.inverse = cartesianComon C
        source
        @[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)) ⋯