extendHomologyIso_inv_homologyι — Mathlib

English

For any complexes K and L with HasHomology, extendMap φ e is a quasi-isomorphism iff φ is a quasi-isomorphism.

Русский

Для комплексов K и L с наличием гомологий extendMap φ e является квазиизоморфизмом тогда и только тогда, когда φ является квазиизоморфизмом.

LaTeX

$$QuasiIso (extendMap φ e) ↔ QuasiIso φ$$

Lean4

@[reassoc (attr := simp)]
theorem extendHomologyIso_inv_homologyι :
    (K.extendHomologyIso e hj').inv ≫ (K.extend e).homologyι j' = K.homologyι j ≫ (K.extendOpcyclesIso e hj').inv := by
  simp only [← cancel_epi (K.extendHomologyIso e hj').hom, Iso.hom_inv_id_assoc, extendHomologyIso_hom_homologyι_assoc,
    Iso.hom_inv_id, comp_id]

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