English
Let K, L be homological complexes over a category C, and let φ: K → L be a morphism of complexes. Given an embedding e, extending φ along e yields a morphism extendMap φ e. Then φ is a quasi-isomorphism if and only if extendMap φ e is a quasi-isomorphism, assuming K and L have homology in every degree.
Русский
Пусть K, L — гомологические комплексы в категориях C, \( \varphi: K \to L \) — морфизм между ними. При заданном вложении e расширение φ вдоль e даёт морфизм extendMap φ e. Тогда φ является квазиизоморфизмом тогда и только тогда, когда extendMap φ e является квазиизоморфизмом, при условии существования гомологий для всех степеней у K и L.
LaTeX
$$$\\operatorname{QuasiIso}(\\mathrm{extendMap}\\,\\varphi\\,e) \\iff \\operatorname{QuasiIso}(\\varphi).$$$
Lean4
theorem quasiIso_extendMap_iff [∀ j, K.HasHomology j] [∀ j, L.HasHomology j] : QuasiIso (extendMap φ e) ↔ QuasiIso φ :=
by
simp only [quasiIso_iff, ← fun j ↦ quasiIsoAt_extendMap_iff φ e (j := j) (hj' := rfl)]
constructor
· tauto
· intro h j'
by_cases hj' : ∃ j, e.f j = j'
· obtain ⟨j, rfl⟩ := hj'
exact h j
· rw [quasiIsoAt_iff_exactAt]
all_goals exact extend_exactAt _ _ _ (by simpa using hj')
