isIso_cyclesMap_of_iso — Mathlib

English

Let S1 and S2 be short complexes in a category with zero morphisms, and let φ: S1 ⟶ S2 be an isomorphism. If S1 and S2 have left homology, then the induced map on cycles, cyclesMap(φ), is an isomorphism.

Русский

Пусть S1 и S2 — краткие комплексные объекты в категории с нулевыми морфизмами, и φ: S1 ⟶ S2 таково, что φ является изоморфизмом. Если у S1 и S2 есть левая гомология, то индуцированное отображение на циклах cyclesMap(φ) является изоморфизмом.

LaTeX

$$$IsIso\big(cyclesMap(\varphi)\big)$$$

Lean4

instance isIso_cyclesMap_of_iso (φ : S₁ ⟶ S₂) [IsIso φ] [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    IsIso (cyclesMap φ) :=
  (inferInstance : IsIso (cyclesMapIso (asIso φ)).hom)

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