English
Let φ: S1 → S2 with particular boundary conditions, there is an equivalence between φ being a quasi-iso and a canonical right-hand map being an isomorphism (through descended op-cycles).
Русский
Пусть φ: S1 → S2 удовлетворяет определенным граничным условиям; эквивалентность: φ — квазиизоморфизм ⇔ соответствующая карта в descended op-cycles является изоморфизмом.
LaTeX
$$$\operatorname{QuasiIso}(φ) \iff \operatorname{IsIso}(S_1.descOpcycles φ.τ_2 (\dots))$$$
Lean4
theorem quasiIso_iff_isIso_descOpcycles (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :
QuasiIso φ ↔ IsIso (S₁.descOpcycles φ.τ₂ (by rw [← φ.comm₁₂, hf₂, comp_zero])) :=
by
let H :
RightHomologyMapData φ (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ _ S₁.opcyclesIsCokernel)
(RightHomologyData.ofZeros S₂ hf₂ hg₂) :=
{ φQ := S₁.descOpcycles φ.τ₂ (by rw [← φ.comm₁₂, hf₂, comp_zero])
φH := S₁.descOpcycles φ.τ₂ (by rw [← φ.comm₁₂, hf₂, comp_zero]) }
exact H.quasiIso_iff
