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 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
    source
    @[deprecated cartesianComon (since := "2025-09-15")]
    def cartesianComon_ (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] :
    CategoryTheory.Functor C (Comon C)

    Alias of cartesianComon.

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

    Equations
    Instances For
      source
      @[simp]
      theorem counit_eq_toUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (A : C) [ComonObj A] :
      ComonObj.counit = CategoryTheory.CartesianMonoidalCategory.toUnit A
      source
      @[deprecated counit_eq_toUnit (since := "2025-05-09")]
      theorem counit_eq_from {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (A : C) [ComonObj A] :
      ComonObj.counit = CategoryTheory.CartesianMonoidalCategory.toUnit A

      Alias of counit_eq_toUnit.

      source
      @[simp]
      theorem comul_eq_lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (A : C) [ComonObj A] :
      ComonObj.comul = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A) (CategoryTheory.CategoryStruct.id A)
      source
      @[deprecated comul_eq_lift (since := "2025-05-09")]
      theorem comul_eq_diag {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (A : C) [ComonObj A] :
      ComonObj.comul = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A) (CategoryTheory.CategoryStruct.id A)

      Alias of comul_eq_lift.

      source
      def isoCartesianComon {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.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 isoCartesianComon_inv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Comon C) :
        (isoCartesianComon A).inv.hom = CategoryTheory.CategoryStruct.id ((cartesianComon C).obj A.X).X
        source
        @[simp]
        theorem isoCartesianComon_hom_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Comon C) :
        (isoCartesianComon A).hom.hom = CategoryTheory.CategoryStruct.id A.X
        source
        @[deprecated isoCartesianComon (since := "2025-09-15")]
        def iso_cartesianComon_ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Comon C) :
        A ≅ (cartesianComon C).obj A.X

        Alias of isoCartesianComon.

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

        Equations
        Instances For
          source
          def comonEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.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 comonEquiv_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] :
            comonEquiv.functor = Comon.forget C
            source
            @[simp]
            theorem comonEquiv_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] :
            comonEquiv.unitIso = CategoryTheory.NatIso.ofComponents isoCartesianComon ⋯
            source
            @[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)) ⋯
            source
            @[simp]
            theorem comonEquiv_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] :
            comonEquiv.inverse = cartesianComon C