functor

Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor

Lean4

/-- Functor translating a comonoid object in a functor category
to a functor into the category of comonoid objects.
-/
@[simps]
def functor : Comon (C ⥤ D) ⥤ C ⥤ Comon D where
  obj A := functorObj A.X
  map
    f :=
    {
      app := fun X =>
        { hom := f.hom.app X
          isComonHom_hom.hom_counit := congr_app (IsComonHom.hom_counit f.hom) X
          isComonHom_hom.hom_comul := congr_app (IsComonHom.hom_comul f.hom) X } }

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

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

Разделы

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

Аффилиация

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