counitFork

Mathlib.CategoryTheory.Monad.Comonadicity

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

Lean4

/-- This is a fork which is helpful for establishing comonadicity: the morphism from this fork to
the Beck equalizer is the counit for the adjunction on the comparison functor.
-/
@[simps! pt]
def counitFork (A : adj.toComonad.Coalgebra) [HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] :
    Fork (F.map (G.map A.a)) (F.map (adj.unit.app (G.obj A.A))) :=
  Fork.ofι (F.map (equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A))))
    (by rw [← F.map_comp, equalizer.condition, F.map_comp])

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

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

Разделы

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

Аффилиация

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