English
If h is a retract of f1 by f2 in ShortComplex and f2 is a quasi-isomorphism, then f1 is a quasi-isomorphism.
Русский
Если h образует retract стрелы f1 относительно f2 в ShortComplex и f2 — квазиизоморфизм, то f1 — квазиизоморфизм.
LaTeX
$$$\text{RetractArrow}(f_1,f_2) \Rightarrow (\text{QuasiIso}(f_2) \Rightarrow \text{QuasiIso}(f_1))$$$
Lean4
theorem quasiIso_of_retract (h : RetractArrow f₁ f₂) [hf₂ : QuasiIso f₂] : QuasiIso f₁ :=
by
rw [quasiIso_iff] at hf₂ ⊢
have h : RetractArrow (homologyMap f₁) (homologyMap f₂) :=
{ i :=
Arrow.homMk (u := homologyMap (show S₁ ⟶ S₂ from h.i.left)) (v := homologyMap (show T₁ ⟶ T₂ from h.i.right))
(by simp [← homologyMap_comp])
r :=
Arrow.homMk (u := homologyMap (show S₂ ⟶ S₁ from h.r.left)) (v := homologyMap (show T₂ ⟶ T₁ from h.r.right))
(by simp [← homologyMap_comp])
retract := by ext <;> simp [← homologyMap_comp] }
exact (MorphismProperty.isomorphisms C).of_retract h hf₂
