English
For an adjoint quadruple L ⊣ F ⊣ G ⊣ R with F (and hence R) fully faithful, all components of G ⟶ L are epimorphisms if and only if all components of F ⟶ R are monomorphisms, assuming domain has pullbacks and codomain has pushouts.
Русский
Для четырехугольника сопряжений L ⊣ F ⊣ G ⊣ R, где F (а значит и R) полностью верен, все компоненты G ⟶ L являются эпиморфиями тогда и только тогда, когда все компоненты F ⟶ R моно, при условии существования предков (pullbacks) в области домена и сходных (pushouts) в области кодома.
LaTeX
$$$\\mathrm{Epi}(q.\\text{leftTriple.rightToLeft}) \\;\\iff\\; \\mathrm{Mono}(q.\\text{rightTriple.leftToRight})$$$
Lean4
/-- For an adjoint quadruple `L ⊣ F ⊣ G ⊣ R` where `F` (and hence also `R`) is fully faithful and
its domain / codomain has all pushouts resp. pullbacks, the natural transformation `G ⟶ L` is an
epimorphism iff the natural transformation `F ⟶ R` is a monomorphism. -/
theorem epi_leftTriple_rightToLeft_iff_mono_rightTriple_leftToRight [HasPullbacks C] [HasPushouts D] :
Epi q.leftTriple.rightToLeft ↔ Mono q.rightTriple.leftToRight :=
by
rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]
exact q.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app
