Lemmas on the homology sequence of a short exact sequence of complexes

Let φ : S₁ ⟶ S₂ be a morphism between two short exact sequences of homological complexes in an abelian category. Mathlib's HomologicalComplex.HomologySequence.quasiIso_τ₃ shows that φ.τ₃ is a quasi-isomorphism when φ.τ₁ and φ.τ₂ are. This file proves the corresponding statement for the middle map: φ.τ₂ is a quasi-isomorphism when φ.τ₁ and φ.τ₃ are. This lets one transfer a quasi-isomorphism to the middle terms of short exact sequences after comparing their outer terms, as for the short exact sequences associated with maps of mapping cones.

It also proves that the connecting maps of a 3 × 3 diagram of complexes with short exact rows and columns anticommute: the two composites of connecting maps from the homology of one corner to that of the opposite corner differ by a sign. Both composites factor through the connecting maps of two auxiliary short exact sequences, ker (X₂₂ ⟶ X₃₃) ⟶ X₂₂ ⟶ X₃₃ and X₁₁ ⟶ X₁₂ ⊞ X₂₁ ⟶ ker (X₂₂ ⟶ X₃₃), and the sign is that of the first map (f, -f) of the second one. This is the sign rule behind the compatibility of products with connecting maps in each variable, such as for the cup product in Tate cohomology.

Main results

• HomologicalComplex.HomologySequence.mono_homologyMap_τ₂, HomologicalComplex.HomologySequence.epi_homologyMap_τ₂, HomologicalComplex.HomologySequence.isIso_homologyMap_τ₂: sufficient conditions for φ.τ₂ to induce a mono, epi or iso in a given degree.
• HomologicalComplex.HomologySequence.quasiIso_τ₂: if φ.τ₁ and φ.τ₃ are quasi-isomorphisms, so is φ.τ₂.
• HomologicalComplex.HomologySequence.δ_comp_δ_eq_neg: the connecting maps of a 3 × 3 diagram with short exact rows and columns anticommute.

theorem HomologicalComplex.HomologySequence.mono_homologyMap_τ₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (j : ι) (h₁ : ∀ (i : ι), c.Rel i j → CategoryTheory.Epi (homologyMap φ.τ₃ i)) (h₂ : CategoryTheory.Mono (homologyMap φ.τ₁ j)) (h₃ : CategoryTheory.Mono (homologyMap φ.τ₃ j)) : CategoryTheory.Mono (homologyMap φ.τ₂ j)

The map φ.τ₂ is injective on homology in degree j if φ.τ₁ and φ.τ₃ are injective in degree j and φ.τ₃ is surjective in the degrees preceding j.

theorem HomologicalComplex.HomologySequence.epi_homologyMap_τ₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (j : ι) (h₁ : CategoryTheory.Epi (homologyMap φ.τ₁ j)) (h₂ : CategoryTheory.Epi (homologyMap φ.τ₃ j)) (h₃ : ∀ (k : ι), c.Rel j k → CategoryTheory.Mono (homologyMap φ.τ₁ k)) : CategoryTheory.Epi (homologyMap φ.τ₂ j)

The map φ.τ₂ is surjective on homology in degree j if φ.τ₁ and φ.τ₃ are surjective in degree j and φ.τ₁ is injective in the degrees following j.

theorem HomologicalComplex.HomologySequence.isIso_homologyMap_τ₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (j : ι) (h₁ : ∀ (i : ι), c.Rel i j → CategoryTheory.Epi (homologyMap φ.τ₃ i)) (h₂ : CategoryTheory.IsIso (homologyMap φ.τ₁ j)) (h₃ : CategoryTheory.IsIso (homologyMap φ.τ₃ j)) (h₄ : ∀ (k : ι), c.Rel j k → CategoryTheory.Mono (homologyMap φ.τ₁ k)) : CategoryTheory.IsIso (homologyMap φ.τ₂ j)

The map φ.τ₂ is an isomorphism on homology in degree j if φ.τ₁ and φ.τ₃ are isomorphisms in degree j, φ.τ₃ is surjective in the degrees preceding j, and φ.τ₁ is injective in the degrees following j.

theorem HomologicalComplex.HomologySequence.quasiIso_τ₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (h₁ : QuasiIso φ.τ₁) (h₃ : QuasiIso φ.τ₃) : QuasiIso φ.τ₂

Two out of three for the middle map. In a morphism of short exact sequences of complexes, if the outer maps φ.τ₁ and φ.τ₃ are quasi-isomorphisms, so is the middle map φ.τ₂.

Anticommutativity of the connecting maps of a 3 × 3 diagram

theorem HomologicalComplex.HomologySequence.δ_comp_δ_eq_neg {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (D : CategoryTheory.ShortComplex (CategoryTheory.ShortComplex (HomologicalComplex C c))) (h₁ : D.X₁.ShortExact) (h₂ : D.X₂.ShortExact) (h₃ : D.X₃.ShortExact) (h₁' : (D.map CategoryTheory.ShortComplex.π₁).ShortExact) (h₂' : (D.map CategoryTheory.ShortComplex.π₂).ShortExact) (h₃' : (D.map CategoryTheory.ShortComplex.π₃).ShortExact) (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) : CategoryTheory.CategoryStruct.comp (h₃.δ i j hij) (h₁'.δ j k hjk) = -CategoryTheory.CategoryStruct.comp (h₃'.δ i j hij) (h₁.δ j k hjk)

The connecting maps of a 3 × 3 diagram anticommute. Let D be a 3 × 3 diagram of homological complexes in an abelian category, presented as a short complex D.X₁ ⟶ D.X₂ ⟶ D.X₃ of short complexes, all of whose rows D.Xᵢ and columns D.map π_j are short exact. Then the two composites of connecting maps from the homology of the corner X₃₃ to that of the corner X₁₁, through the third row and the first column, and through the third column and the first row, differ by a sign.