ofMon

Mathlib.CategoryTheory.Monad.EquivMon

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

Lean4

/-- To every monoid object in `C ⥤ C` we associate a `Monad C`. -/
@[simps «η» «μ»]
def ofMon (M : Mon (C ⥤ C)) : Monad C where
  toFunctor := M.X
  «η» := η[M.X]
  «μ» := μ[M.X]
  left_unit := fun X => by simpa [-MonObj.mul_one] using congrArg (fun t ↦ t.app X) (mul_one M.X)
  right_unit := fun X => by simpa [-MonObj.one_mul] using congrArg (fun t ↦ t.app X) (one_mul M.X)
  assoc := fun X => by
    simpa [-MonObj.mul_assoc] using
      congrArg (fun t ↦ t.app X)
        (mul_assoc M.X)
          -- Porting note: `@[simps]` fails to generate `ofMon_obj`:

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

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

Разделы

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

Аффилиация

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