English
For any adjunction F ⊣ G and any algebra A for adj.toMonad, G reflects the colimit of the parallel pair formed by F.map A.a and adj.counit.app (F.obj A.A).
Русский
Для всякого сопряжения F ⊣ G и любой алгебры A для adj.toMonad, G отражает колимит параллельной пары, образованной F.map A.a и adj.counit.app (F.obj A.A).
LaTeX
$$$\\forall A:\\mathrm{Algebra}(adj.toMonad),\\; \\operatorname{ReflectsColimit}(\\operatorname{parallelPair}(F.map A.a,\\; \\mathrm{NatTrans.app}\\ adj.counit\\ (F.obj A.A)))\\ G$$$
Lean4
instance [ReflectsColimitOfIsSplitPair G] :
∀ (A : Algebra adj.toMonad), ReflectsColimit (parallelPair (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))) G :=
fun _ => ReflectsColimitOfIsSplitPair.out _ _
