functorObj

Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

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

Lean4

/-- A monoid object in a functor category induces a functor to the category of monoid objects. -/
@[simps]
def functorObj (A : C ⥤ D) [MonObj A] : C ⥤ Mon D
    where
  obj := functorObjObj A
  map
    f :=
    { hom := A.map f
      isMonHom_hom :=
        { one_hom := by dsimp; rw [← η[A].naturality, tensorUnit_map]; dsimp; rw [Category.id_comp]
          mul_hom := by dsimp; rw [← μ[A].naturality, tensorObj_map] } }
  map_id X := by ext; dsimp; rw [CategoryTheory.Functor.map_id]
  map_comp f g := by ext; dsimp; rw [Functor.map_comp]

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

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

Разделы

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

Аффилиация

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