quasiIsoAt_shift_iff — Mathlib

English

A shiftIso for homology in the ShiftSequence context is compatible with quotient and functor composition, yielding a coherent diagram in homology.

Русский

Изоморфия сдвига для гомологии в контексте ShiftSequence совместима с кватированием и композициями функторов, образуя согласованную диаграмму в гомологии.

LaTeX

$$$\\text{shiftIso} \\; n a a' : \\; (\\mathrm{shiftFunctor} \\; n) \\circ \\mathrm{homologyFunctor} (C, \\mathrm{up} \\mathbb{Z}) a \\cong \\mathrm{homologyFunctor} (C, \\mathrm{up} \\mathbb{Z}) a'$$$

Lean4

theorem quasiIsoAt_shift_iff {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n i j : ℤ) (h : n + i = j) :
    QuasiIsoAt (φ⟦n⟧') i ↔ QuasiIsoAt φ j :=
  by
  simp only [quasiIsoAt_iff_isIso_homologyMap]
  exact (NatIso.isIso_map_iff ((homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i j h) φ)

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