hasHomology_of_preserves' — Mathlib

English

If S has homology and F preserves the left and right homology of S, then F.mapShortComplex.obj S has homology.

Русский

Если S обладает гомологией и F сохраняет левую и правую гомологию S, то F.mapShortComplex.obj S имеет гомологию.

LaTeX

$$$S.HasHomology \wedge F.PreservesLeftHomologyOf S \wedge F.PreservesRightHomologyOf S \Rightarrow (F.mapShortComplex.obj S).HasHomology.$$$

Lean4

instance hasHomology_of_preserves' [S.HasHomology] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] :
    (F.mapShortComplex.obj S).HasHomology := by dsimp; infer_instance

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