hg — Mathlib · SciLib

English

When a functor preserves a left homology data, it preserves left homology of S.

Русский

Если функтор сохраняет левую гомологию краткого комплекса S, он сохраняет левую гомологию S.

LaTeX

$$$F\\text{ preserves left homology of }S$$$

Lean4

/-- When a left homology data is preserved by a functor `F`, this functor
preserves the kernel of `S.g : S.X₂ ⟶ S.X₃`. -/
theorem hg : PreservesLimit (parallelPair S.g 0) F :=
  @IsPreservedBy.g _ _ _ _ _ _ _ h F _ _

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