functorObjObj

Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

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

Lean4

/-- A comonoid object in a functor category sends any object to a comonoid object. -/
@[simps]
def functorObjObj (A : C ⥤ D) [ComonObj A] (X : C) : Comon D
    where
  X := A.obj X
  comon :=
    { counit := ε[A].app X
      comul := Δ[A].app X
      counit_comul := congr_app (counit_comul A) X
      comul_counit := congr_app (comul_counit A) X
      comul_assoc := congr_app (comul_assoc A) X }

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

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

Разделы

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

Аффилиация

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