monToMonad

Mathlib.CategoryTheory.Monad.EquivMon

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

Lean4

/-- Passing from `Mon (C ⥤ C)` to `Monad C` is functorial. -/
@[simps]
def monToMonad : Mon (C ⥤ C) ⥤ Monad C where
  obj := ofMon
  map {X Y}
    f :=
    {
      f.hom with
      app_η X := by simpa [-IsMonHom.one_hom] using congrArg (fun t ↦ t.app X) (IsMonHom.one_hom f.hom)
      app_μ Z := by simpa [-IsMonHom.mul_hom] using congrArg (fun t ↦ t.app Z) (IsMonHom.mul_hom f.hom) }

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

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

Разделы

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

Аффилиация

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