quasiIso_map_of_preservesHomology

Mathlib.Algebra.Homology.QuasiIso

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.quasiIso_map_of_preservesHomology

English

If F preserves homology, then QuasiIso ((F.mapHomologicalComplex c).map φ) is equivalent to QuasiIso φ.

Русский

Если F сохраняет гомологию, то QuasiIso образа φ равносильно QuasiIso φ.

LaTeX

$$$\text{QuasiIso}((F.mapHomologicalComplex c).map \varphi) \iff \text{QuasiIso}(\varphi).$$$

Lean4

instance quasiIso_map_of_preservesHomology [hφ : QuasiIso φ] : QuasiIso ((F.mapHomologicalComplex c).map φ) where

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru