instComonadicLeftAdjointCoalgebraForget

Mathlib.CategoryTheory.Monad.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instComonadicLeftAdjointCoalgebraForget

Lean4

noncomputable instance (G : Comonad C) : ComonadicLeftAdjoint G.forget
    where
  R := G.cofree
  adj := G.adj
  eqv :=
    { }
      -- TODO: This holds more generally for idempotent adjunctions, not just reflective adjunctions.

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

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

Разделы

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

Аффилиация

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