preservesKernel — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- A functor which preserves homology preserves kernels. -/
theorem preservesKernel [F.PreservesHomology] {X Y : C} (f : X ⟶ Y) : PreservesLimit (parallelPair f 0) F :=
  PreservesHomology.preservesKernels _

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