quasiIso_shift_iff — Mathlib

English

For Cochain complexes, shifting preserves quasi-isomorphisms: QuasiIso(φ⟦n⟧') iff QuasiIso φ.

Русский

При сдвиге сохранение квазиизоморфизмов: QuasiIso(φ⟦n⟧') ⇔ QuasiIso φ.

LaTeX

$$$$\\text{QuasiIso}(\\phi⟦n⟧') \\iff \\text{QuasiIso}(\\phi)$$$$

Lean4

theorem quasiIso_shift_iff {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ) : QuasiIso (φ⟦n⟧') ↔ QuasiIso φ :=
  by
  simp only [quasiIso_iff, fun i ↦ quasiIsoAt_shift_iff φ n i _ rfl]
  constructor
  · intro h j
    obtain ⟨i, rfl⟩ : ∃ i, j = n + i := ⟨j - n, by cutsat⟩
    exact h i
  · intro h i
    exact h (n + i)

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