hf — Mathlib · SciLib

English

In a preserved right-homology data, the kernel of g' is preserved by F.

Русский

В сохранённом правом гомологическом наборе ядро g' сохраняется функтором F.

LaTeX

$$$\\operatorname{PreservesLimit}(\\text{parallelPair}~h.g'\\,0)\\,F$$$

Lean4

/-- When a right homology data is preserved by a functor `F`, this functor
preserves the cokernel of `S.f : S.X₁ ⟶ S.X₂`. -/
theorem hf : PreservesColimit (parallelPair S.f 0) F :=
  @IsPreservedBy.f _ _ _ _ _ _ _ h F _ _

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