cartesianComon

Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

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

Lean4

/-- The functor from a Cartesian monoidal category to comonoids in that category,
equipping every object with the diagonal map as a comultiplication.
-/
def cartesianComon : C ⥤ Comon C
    where
  obj
    X :=
    { X := X
      comon :=
        { comul := lift (𝟙 _) (𝟙 _)
          counit := toUnit _ } }
  map f := .mk' f

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

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

Разделы

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

Аффилиация

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