Quasi-isomorphisms in short exact sequences of complexes

For a morphism of short exact sequences of integer-indexed cochain complexes in an abelian category, quasi-isomorphisms on the outer terms imply one on the middle term.

Main results

• HomologicalComplex.HomologySequence.quasiIso_τ₂ gives the middle-term quasi-isomorphism without choosing a model for the abelian category.

Implementation notes

The long exact homology sequences supply two five-object windows. The four lemma gives monicity in the window ending at the current degree and epicity in the window beginning there. These combine into an isomorphism on each homology object.

References

This extends Mathlib's HomologicalComplex.HomologySequence.quasiIso_τ₃ and uses its exact five-object homology sequence and the abelian four lemmas.

theorem HomologicalComplex.HomologySequence.quasiIso_τ₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (h₁ : QuasiIso φ.τ₁) (h₃ : QuasiIso φ.τ₃) : QuasiIso φ.τ₂

The τ₂ companion to Mathlib's HomologicalComplex.HomologySequence.quasiIso_τ₃: if the outer maps in a morphism of short exact cochain-complex sequences are quasi-isomorphisms, so is the middle map. The neighboring five-object homology windows and abelian four lemmas make each middle homology map both mono and epi.