hg' — Mathlib

English

The kernel preservation claim for g' holds under preservation assumptions.

Русский

Утверждение о сохранении ядра для g' выполняется при предположениях сохранения.

LaTeX

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

Lean4

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

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