isIso_opcyclesMap_of_iso — Mathlib

English

Let φ: S1 ⟶ S2 be an isomorphism between short complexes with right homology. Then opcyclesMap φ is an isomorphism.

Русский

Пусть φ: S1 ⟶ S2 — изоморфизм между короткими комплексами, имеющими правую гомологию. Тогда opcyclesMap φ является изоморфизмом.

LaTeX

$$IsIso\left(\mathrm{opcyclesMap}(\varphi)\right)$$

Lean4

instance isIso_opcyclesMap_of_iso (φ : S₁ ⟶ S₂) [IsIso φ] [S₁.HasRightHomology] [S₂.HasRightHomology] :
    IsIso (opcyclesMap φ) :=
  (inferInstance : IsIso (opcyclesMapIso (asIso φ)).hom)

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