quasiIso_of_isIso

Mathlib.Algebra.Homology.ShortComplex.QuasiIso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.quasiIso_of_isIso

English

If φ is an isomorphism, then φ is a quasi-iso.

Русский

Если φ является изоморфизмом, то φ является квазиизоморфизмом.

LaTeX

$$$\text{IsIso}(φ) \Rightarrow \text{QuasiIso}(φ)$$$

Lean4

instance quasiIso_of_isIso (φ : S₁ ⟶ S₂) [IsIso φ] : QuasiIso φ :=
  ⟨(homologyMapIso (asIso φ)).isIso_hom⟩

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

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

Разделы

Аффилиация

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