English
The unit component at B of the comparison adjunction equals the limit lift along the parallel pair diagram with unit Fork, i.e., unit satisfies the universal property.
Русский
Компонента единицы в точке B сравнения эквивалентна взятию пределa через параллельную пару и fork единицы, удовлетворяя универсальному свойству.
LaTeX
$$$(\mathrm{comparisonAdjunction}\ adj).\mathrm{unit}.app B = \operatorname{limit.lift}_{\cdot}\Bigl(\operatorname{parallelPair}\bigl(G.map (F.map (\operatorname{unit.app} B)), \operatorname{unit.app} (G.obj (F.obj B))\bigr)\Bigr)(\mathrm{unitFork} adj B).$$$
Lean4
theorem comparisonAdjunction_unit_app
[∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))] (B : C) :
(comparisonAdjunction adj).unit.app B = limit.lift _ (unitFork adj B) :=
by
apply equalizer.hom_ext
change equalizer.lift ((adj.homEquiv B _) (𝟙 _)) _ ≫ equalizer.ι _ _ = equalizer.lift _ _ ≫ equalizer.ι _ _
simp [Adjunction.homEquiv_unit]
