inverse

Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse

Lean4

/-- Functor translating a functor into the category of monoid objects
to a monoid object in the functor category
-/
@[simps]
def inverse : (C ⥤ Mon D) ⥤ Mon (C ⥤ D) where
  obj := inverseObj
  map
    α :=
    .mk'
      { app := fun X => (α.app X).hom
        naturality := fun _ _ f => congr_arg Mon.Hom.hom (α.naturality f) }

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

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

Разделы

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

Аффилиация

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