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.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts 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
    @[simp]
    theorem counit_eq_from {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (A : Comon_ C) :
    A.counit = CategoryTheory.Limits.terminal.from A.X
    source
    @[simp]
    theorem comul_eq_diag {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (A : Comon_ C) :
    A.comul = CategoryTheory.Limits.diag A.X
    source
    def iso_cartesianComon_ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts 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 iso_cartesianComon__inv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (A : Comon_ C) :
      (iso_cartesianComon_ A).inv.hom = CategoryTheory.CategoryStruct.id ((cartesianComon_ C).obj A.X).X
      source
      @[simp]
      theorem iso_cartesianComon__hom_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] (A : Comon_ C) :
      (iso_cartesianComon_ A).hom.hom = CategoryTheory.CategoryStruct.id A.X
      source
      def comonEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts 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.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] :
        comonEquiv.functor = Comon_.forget C
        source
        @[simp]
        theorem comonEquiv_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts 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.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts 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.Limits.HasTerminal C] [CategoryTheory.Limits.HasBinaryProducts C] :
        comonEquiv.inverse = cartesianComon_ C