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
    Instances For
      source
      @[simp]
      theorem counit_eq_toUnit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (A : C) [Comon_Class A] :
      Comon_Class.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) [Comon_Class A] :
      Comon_Class.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) [Comon_Class A] :
      Comon_Class.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) [Comon_Class A] :
      Comon_Class.comul = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A) (CategoryTheory.CategoryStruct.id A)

      Alias of comul_eq_lift.

      source
      def iso_cartesianComon_ {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
        Instances For
          source
          @[simp]
          theorem iso_cartesianComon__hom_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Comon_ C) :
          (iso_cartesianComon_ A).hom.hom = CategoryTheory.CategoryStruct.id A.X
          source
          @[simp]
          theorem iso_cartesianComon__inv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Comon_ C) :
          (iso_cartesianComon_ A).inv.hom = CategoryTheory.CategoryStruct.id ((cartesianComon_ C).obj A.X).X
          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
            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_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_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] :
              comonEquiv.unitIso = CategoryTheory.NatIso.ofComponents (fun (A : Comon_ C) => iso_cartesianComon_ A) ⋯
              source
              @[simp]
              theorem comonEquiv_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] :
              comonEquiv.inverse = cartesianComon_ C