English
For an adjoint quadruple L ⊣ F ⊣ G ⊣ R with F (and hence R) fully faithful, all components of the natural transformation L ⟶ G are epimorphisms iff all components of the natural transformation R ⟶ F are monomorphisms, under HasPullbacks C and HasPushouts D.
Русский
Для четырехугольника сопряжений L ⊣ F ⊣ G ⊣ R при условии полного достоверности F и R и существования pullbacks/pushouts, все компоненты L ⟶ G эпиморфизм, если и только если все компоненты R ⟶ F моноℹморфизм.
LaTeX
$$$\\mathrm{Epi}(q.\\text{leftTriple.leftToRight}) \\;\\iff\\; \\mathrm{Mono}(q.\\text{rightTriple.rightToLeft})$$$
Lean4
/-- For an adjoint quadruple `L ⊣ F ⊣ G ⊣ R` where `L` and `G` are fully faithful, all components
of the natural transformation `L ⟶ G` are epimorphisms iff all components of the natural
transformation `R ⟶ F` are monomorphisms. -/
theorem epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app :
(∀ X, Epi (q.leftTriple.leftToRight.app X)) ↔ ∀ X, Mono (q.rightTriple.rightToLeft.app X) :=
by
have h := q.op.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app
rw [← (Opposite.equivToOpposite (α := C)).forall_congr_right] at h
rw [← (Opposite.equivToOpposite (α := D)).forall_congr_right] at h
simpa using h.symm
