preservesMonomorphisms_of_preserves_shortExact_left

English

If a functor preserves right-hand side exact sequences, then it preserves epimorphisms.

Русский

Если функтор сохраняет правые точные последовательности, он сохраняет эпиморфизмы.

LaTeX

$$$F \text{ preserves right-exact short sequences} \Rightarrow F\text{ preserves epimorphisms}$$$

Lean4

/-- If a functor `F : C ⥤ D` preserves short exact sequences on the left-hand side, (i.e.
if `0 ⟶ A ⟶ B ⟶ C ⟶ 0` is exact then `0 ⟶ F(A) ⟶ F(B) ⟶ F(C)` is exact)
then it preserves monomorphism.
-/
theorem preservesMonomorphisms_of_preserves_shortExact_left
    (h : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) : F.PreservesMonomorphisms where
  preserves f := h _ { exact := exact_cokernel f } |>.2

Похожие утверждения