preservesCokernel — Mathlib

English

If F preserves homology, it preserves cokernels of f, i.e., preserves the colimit of the parallel pair (f,0).

Русский

Если F сохраняет гомологию, то он сохраняет кофокиль f, т.е. сохраняет сопряжённый предел параллельной пары (f,0).

LaTeX

$$$\\operatorname{PreservesColimit}(\\text{parallelPair}(f,0))\,F$$$

Lean4

/-- A functor which preserves homology preserves cokernels. -/
theorem preservesCokernel [F.PreservesHomology] {X Y : C} (f : X ⟶ Y) : PreservesColimit (parallelPair f 0) F :=
  PreservesHomology.preservesCokernels _

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