instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison

Mathlib.CategoryTheory.Monad.Adjunction

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

English

There is an equivalence for the comonad comparison when L is ComonadicLeftAdjoint.

Русский

Существует эквивалентность сопоставления комонады для ComonadicLeftAdjoint.

LaTeX

$$$$ (\\mathrm{Comonad.comparison}(L)).IsEquivalence $$$$

Lean4

instance (L : C ⥤ D) [ComonadicLeftAdjoint L] : (Comonad.comparison (comonadicAdjunction L)).IsEquivalence :=
  ComonadicLeftAdjoint.eqv

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

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

Разделы

Аффилиация

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