hasRightHomology_of_preserves' — Mathlib

English

If S has right homology and F preserves the right homology of S, then the mapped short complex F.mapShortComplex.obj S has right homology.

Русский

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

LaTeX

$$$S\text{ HasRightHomology} \wedge F\text{PreservesRightHomologyOf S} \Rightarrow (F.mapShortComplex.obj S).HasRightHomology.$$$

Lean4

instance hasRightHomology_of_preserves' [S.HasRightHomology] [F.PreservesRightHomologyOf S] :
    (F.mapShortComplex.obj S).HasRightHomology := by dsimp; infer_instance

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