English
Let adj be an adjunction F ⊣ G with F preserving projectives; then G preserves epimorphisms.
Русский
Пусть adj — тождество F ⊣ G с сохранением проективности F; тогда G сохраняет эпиморфизмы.
LaTeX
$$$ (\\text{adj} : F \\dashv G) \\land F.PreservesProjectiveObjects \\Rightarrow G.PreservesEpimorphisms. $$$
Lean4
theorem preservesEpimorphisms_of_adjunction_of_preservesProjectiveObjects [EnoughProjectives C] {F : C ⥤ D} {G : D ⥤ C}
(adj : F ⊣ G) [F.PreservesProjectiveObjects] : G.PreservesEpimorphisms where
preserves {X Y} f
_ := by
suffices ∃ h, h ≫ G.map f = Projective.π (G.obj Y) from epi_of_epi_fac this.choose_spec
refine
⟨adj.unit.app (Projective.over (G.obj Y)) ≫
G.map (Projective.factorThru (F.map (Projective.π _) ≫ adj.counit.app Y) f),
?_⟩
rw [Category.assoc, ← Functor.map_comp]
simp
