English
There is a natural equivalence between Hom((comparisonLeftAdjointObj adj A), B) and Hom(A, (comparison adj).obj B) for A in adj.toMonad.Algebra and B in D, given a suitable coequalizer.
Русский
Существует естественное эквивалентность между множествами гом-отрезков, соединяющая (comparisonLeftAdjointObj adj A) и B с A и (comparison adj).obj B, при наличии нужного коэквалайзера.
LaTeX
$$$\\bigl(\\operatorname{Hom}(\\mathrm{comparisonLeftAdjointObj}\\;adj\\;A, B) \\bigr) \\simeq \\operatorname{Hom}\\bigl(A, (\\mathrm{comparison}\\;adj).\\mathrm{obj}\\;B\\bigr).$$$
Lean4
/-- The "main pair" for an algebra `(A, α)` is the pair of morphisms `(F α, ε_FA)`. It is always a
`G`-split pair, and will be used to construct the left adjoint to the comparison functor and show it
is an equivalence.
-/
instance main_pair_G_split (A : adj.toMonad.Algebra) : G.IsSplitPair (F.map A.a) (adj.counit.app (F.obj A.A)) where
splittable := ⟨_, _, ⟨beckSplitCoequalizer A⟩⟩
