English
Under EnoughInjectives in D, adjunction F ⊣ G and GPreservesInjectiveObjects, FPreservesMonomorphisms.
Русский
При EnoughInjectives в D, сопряжение F ⊣ G и GPreservesInjectiveObjects, FPreservesMonomorphisms.
LaTeX
$$$$\\forall \\text{adj} : F \\dashv G\\;[G\\text{PreservesInjectiveObjects}]\\;\\Rightarrow F\\PreservesMonomorphisms.$$$$
Lean4
theorem preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects [EnoughInjectives D] {F : C ⥤ D} {G : D ⥤ C}
(adj : F ⊣ G) [G.PreservesInjectiveObjects] : F.PreservesMonomorphisms where
preserves {X Y} f
_ := by
suffices ∃ h, F.map f ≫ h = Injective.ι (F.obj X) from mono_of_mono_fac this.choose_spec
exact
⟨F.map (Injective.factorThru (adj.unit.app X ≫ G.map (Injective.ι _)) f) ≫
adj.counit.app (Injective.under (F.obj X)),
by simp [← Functor.map_comp_assoc]⟩
