monadMonEquiv

Mathlib.CategoryTheory.Monad.EquivMon

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Monad.monadMonEquiv

Lean4

/-- Oh, monads are just monoids in the category of endofunctors (equivalence of categories). -/
@[simps]
def monadMonEquiv : Monad C ≌ Mon (C ⥤ C) where
  functor := monadToMon _
  inverse := monToMonad _
  unitIso :=
    { hom := { app := fun _ => { app := fun _ => 𝟙 _ } }
      inv := { app := fun _ => { app := fun _ => 𝟙 _ } } }
  counitIso :=
    { hom := { app := fun _ => { hom := 𝟙 _ } }
      inv := { app := fun _ => { hom := 𝟙 _ } } }
      -- Sanity check

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

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

Разделы

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

Аффилиация

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