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
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
@[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
@[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
@[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
@[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
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
@[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)) ⋯
@[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) ⋯
@[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
@[simp]
theorem
comonEquiv_inverse
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasTerminal C]
[CategoryTheory.Limits.HasBinaryProducts C]
:
comonEquiv.inverse = cartesianComon_ C
def
comonEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasTerminal C]
[CategoryTheory.Limits.HasBinaryProducts 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.