free

Mathlib.CategoryTheory.Monad.Algebra

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

Lean4

/-- The free functor from the Eilenberg-Moore category, constructing an algebra for any object. -/
@[simps]
def free : C ⥤ Algebra T
    where
  obj
    X :=
    { A := T.obj X
      a := T.μ.app X
      assoc := (T.assoc _).symm }
  map
    f :=
    { f := T.map f
      h := T.μ.naturality _ }

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

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

Разделы

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

Аффилиация

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