hasRightHomology_of_iso — Mathlib

English

If S1 ≅ S2 and S1 has right homology, then S2 has right homology.

Русский

Если S1 изоморфен S2 и у S1 есть правая гомология, то у S2 тоже есть правая гомология.

LaTeX

$$$S_1 \\cong S_2 \\Rightarrow \\text{HasRightHomology}(S_2) \\text{ from } \\text{HasRightHomology}(S_1)$$$

Lean4

theorem hasRightHomology_of_iso {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) [HasRightHomology S₁] : HasRightHomology S₂ :=
  hasRightHomology_of_epi_of_isIso_of_mono e.hom

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