English
Given a quadruple L ⊣ F ⊣ G ⊣ R with F.Full and F.Faithful and HasPullbacks/HasPushouts, all components of q.leftTriple.rightToLeft are epimorphisms iff all components of q.rightTriple.leftToRight are monomorphisms.
Русский
Для четырехугольника L ⊣ F ⊣ G ⊣ R с F.Full и F.Faithful и наличием pullbacks/pushouts все компоненты q.leftTriple.rightToLeft эпиморфны тогда и только тогда, когда все компоненты q.rightTriple.leftToRight моноформны.
LaTeX
$$$(\\forall X, \\mathrm{Epi}(q.leftTriple.rightToLeft.app X)) \\iff (\\forall X, \\mathrm{Mono}(q.rightTriple.leftToRight.app X))$$$
Lean4
/-- If `A` is essentially in the image of a reflective functor `i`, then `η_A` is an isomorphism.
This gives that the "witness" for `A` being in the essential image can instead be given as the
reflection of `A`, with the isomorphism as `η_A`.
(For any `B` in the reflective subcategory, we automatically have that `ε_B` is an iso.)
-/
theorem unit_isIso [Reflective i] {A : C} (h : i.essImage A) : IsIso ((reflectorAdjunction i).unit.app A) := by
rwa [isIso_unit_app_iff_mem_essImage]
