isoCartesianComon

Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

URI: https://scilib.ai/kg/mathlib#isoCartesianComon

Lean4

/-- Every comonoid object in a Cartesian monoidal category is equivalent to
the canonical comonoid structure on the underlying object.
-/
@[simps]
def isoCartesianComon (A : Comon C) : A ≅ (cartesianComon C).obj A.X :=
  { hom := .mk' (𝟙 _)
    inv := .mk' (𝟙 _) }

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru