cofree

Mathlib.CategoryTheory.Monad.Algebra

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Comonad.cofree

Lean4

/-- The cofree functor from the Eilenberg-Moore category, constructing a coalgebra for any
object. -/
@[simps]
def cofree : C ⥤ Coalgebra G
    where
  obj
    X :=
    { A := G.obj X
      a := G.δ.app X
      coassoc := (G.coassoc _).symm }
  map
    f :=
    { f := G.map f
      h := (G.δ.naturality _).symm }
      -- The other two `simps` projection lemmas can be derived from these two, so `simp_nf` complains if
      -- those are added too

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

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

Разделы

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

Аффилиация

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