English
Given an adjunction F ⊣ G with G preserving injectives and D having enough injectives, F preserves monomorphisms.
Русский
При заданном сопряжении F ⊣ G, если G сохраняет инъективные и D имеет достаточно инъективных, то F сохраняет моно-морфизмы.
LaTeX
$$$$\\forall \\text{adj} : F \\dashv G\\;[G\\text{PreservesInjectiveObjects}]\\;\\Rightarrow \\; F\\text{PreservesMonomorphisms}. $$$$
Lean4
theorem preservesInjectiveObjects_of_adjunction_of_preservesMonomorphisms {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
[F.PreservesMonomorphisms] : G.PreservesInjectiveObjects where injective_obj h := adj.map_injective _ h
