English
If L ⊣ R is an adjunction with L preserving monos and R has enough injectives in D, then C has enough injectives.
Русский
Если L ⊣ R есть сопряжение, где L сохраняет моно morphisms, а D имеет достаточно инъективных объектов, то C имеет достаточно инъективных объектов.
LaTeX
$$$$\\forall {L : C \\to D}\\;{R : D \\to C}\\;(\\text{adj} : L \\dashv R)\\;[L\\text{PreservesMonomorphisms}]\\,[\\text{EnoughInjectives}(D)]\\;\\Rightarrow \\; \\text{EnoughInjectives}(C).$$$$
Lean4
/-- [Lemma 3.8](https://ncatlab.org/nlab/show/injective+object#preservation_of_injective_objects)
-/
theorem of_adjunction {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] {L : C ⥤ D} {R : D ⥤ C}
(adj : L ⊣ R) [L.PreservesMonomorphisms] [L.ReflectsMonomorphisms] [EnoughInjectives D] : EnoughInjectives C where
presentation _ := ⟨adj.injectivePresentationOfMap _ (EnoughInjectives.presentation _).some⟩
