English
Under similar fully faithful assumptions for F and R, the natural transformation G ⟶ L is an epimorphism iff the natural transformation F ⟶ R is a monomorphism.
Русский
При подобном условии полноты для F и R, естественная трансформация G ⟶ L эпиморфна тогда и только тогда, когда естественная трансформация F ⟶ R моноформична.
LaTeX
$$$\\mathrm{Epi}(q.\\text{leftTriple.rightToLeft}) \\iff \\mathrm{Mono}(q.\\text{rightTriple.leftToRight})$$$
Lean4
/-- For an adjoint quadruple `L ⊣ F ⊣ G ⊣ R` where `L` and `G` are fully faithful and their domain
and codomain have all pullbacks resp. pushouts, the natural transformation `L ⟶ G` is an
epimorphism iff the natural transformation `R ⟶ F` is a monomorphism. -/
theorem epi_leftTriple_leftToRight_iff_mono_rightTriple_rightToLeft [HasPullbacks C] [HasPushouts D] :
Epi q.leftTriple.leftToRight ↔ Mono q.rightTriple.rightToLeft :=
by
rw [NatTrans.epi_iff_epi_app, NatTrans.mono_iff_mono_app]
exact q.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app
