mapComon

Mathlib.CategoryTheory.Monoidal.Comon_

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.mapComon

Lean4

/-- A oplax monoidal functor takes comonoid objects to comonoid objects.

That is, a oplax monoidal functor `F : C ⥤ D` induces a functor `Comon C ⥤ Comon D`.
-/
@[simps]
def mapComon (F : C ⥤ D) [F.OplaxMonoidal] : Comon C ⥤ Comon D
    where
  obj A := { X := F.obj A.X }
  map f := { hom := F.map f.hom }
  map_id A := by ext; simp
  map_comp f
    g := by ext;
    simp
      -- TODO We haven't yet set up the category structure on `OplaxMonoidalFunctor C D`
      -- and so can't state `mapComonFunctor : OplaxMonoidalFunctor C D ⥤ Comon C ⥤ Comon D`.

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

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

Разделы

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

Аффилиация

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