instQuasiIsoIntMapHomologicalComplexUpShiftFunctor

English

If φ is a quasi-isomorphism between Cochain complexes, then the shifted morphism φ⟦n⟧' is also a quasi-isomorphism.

Русский

Если φ — квазиизоморфизм между двухконечными комплексами, то и сдвиг φ⟦n⟧' является квазиизоморфизмом.

LaTeX

$$$[\\text{QuasiIso } φ] \\Rightarrow [\\text{QuasiIso } φ⟦n⟧']$$$

Lean4

instance {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) [QuasiIso φ] : QuasiIso (φ⟦n⟧') :=
  by
  rw [quasiIso_shift_iff]
  infer_instance

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