preservesMonomorphisms_of_map_exact

English

If a functor preserves exactness of short complexes, it preserves monomorphisms.

Русский

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

LaTeX

$$$\\text{preservesMonomorphisms}(L)\\;\\Longrightarrow\\; \\text{Monomorphisms}(L)$$$

Lean4

/-- A functor which preserves exactness preserves monomorphisms. -/
theorem preservesMonomorphisms_of_map_exact : L.PreservesMonomorphisms where
  preserves f
    hf := by
    apply ((Abelian.tfae_mono (L.map f) (L.obj 0)).out 2 0).mp
    refine ShortComplex.exact_of_iso ?_ (hL _ (((tfae_mono f 0).out 0 2).mp hf))
    exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

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