unitEqualizerOfCoreflectsEqualizer

Mathlib.CategoryTheory.Monad.Comonadicity

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

Lean4

/-- The unit fork is a limit provided `F` coreflects it. -/
def unitEqualizerOfCoreflectsEqualizer (B : C)
    [ReflectsLimit (parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))) F] :
    IsLimit (unitFork (adj := adj) B) :=
  isLimitOfIsLimitForkMap F _ (beckEqualizer ((comparison adj).obj B))

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

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

Разделы

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

Аффилиация

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