Commit 2024-05-31 09:58 40c57eb6
View on Github →feat(Algebra/Homology): consequences of the homology sequence (#12638)
In this PR, we show that the homology sequence attached to a short exact sequence of homological complexes is functorial with respect to a morphism φ : S₁ ⟶ S₂ between two such short exact sequences. We show that if φ.τ₁ and φ.τ₂ are quasi-isomorphisms, then so is φ.τ₃. (Other similar lemmas shall be obtained in a future PR.)