Consequences of the homology sequence

Given a morphism φ : S₁ ⟶ S₂ between two short exact sequences of homological complexes in an abelian category, we show the naturality of the homology sequence of S₁ and S₂ with respect to φ (see HomologicalComplex.HomologySequence.δ_naturality).

Then, we shall show in this file that if two out of the three maps φ.τ₁, φ.τ₂, φ.τ₃ are quasi-isomorphisms, then the third is. We also obtain more specific separate lemmas which gives sufficient condition for one of these three morphisms to induce a mono/epi/iso in a given degree in terms of properties of the two others in the same or neighboring degrees.

So far, we state only four lemmas for φ.τ₃. Eight more similar lemmas for φ.τ₁ and φ.τ₂ shall be also obtained (TODO).

@[simp]

theorem HomologicalComplex.HomologySequence.mapSnakeInput_f₀ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} {S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) : (HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₀ = (HomologicalComplex.homologyFunctor C c i).mapShortComplex.map φ

@[simp]

theorem HomologicalComplex.HomologySequence.mapSnakeInput_f₃ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} {S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) : (HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₃ = (HomologicalComplex.homologyFunctor C c j).mapShortComplex.map φ

@[simp]

theorem HomologicalComplex.HomologySequence.mapSnakeInput_f₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} {S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) : (HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₂ = (HomologicalComplex.cyclesFunctor C c j).mapShortComplex.map φ

@[simp]

theorem HomologicalComplex.HomologySequence.mapSnakeInput_f₁ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} {S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) : (HomologicalComplex.HomologySequence.mapSnakeInput φ hS₁ hS₂ i j hij).f₁ = (HomologicalComplex.opcyclesFunctor C c i).mapShortComplex.map φ

noncomputable def HomologicalComplex.HomologySequence.mapSnakeInput {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} {S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) : HomologicalComplex.HomologySequence.snakeInput hS₁ i j hij ⟶ HomologicalComplex.HomologySequence.snakeInput hS₂ i j hij

The morphism snakeInput hS₁ i j hij ⟶ snakeInput hS₂ i j hij induced by a morphism φ : S₁ ⟶ S₂ of short complexes of homological complexes, that are short exact (hS₁ : S₁.ShortExact and hS₂ : S₁.ShortExact).

Equations

• One or more equations did not get rendered due to their size.

theorem HomologicalComplex.HomologySequence.δ_naturality_assoc {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} {S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) {Z : C} (h : S₂.X₁.homology j ⟶ Z) : CategoryTheory.CategoryStruct.comp (hS₁.δ i j hij) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ.τ₁ j) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ.τ₃ i) (CategoryTheory.CategoryStruct.comp (hS₂.δ i j hij) h)

theorem HomologicalComplex.HomologySequence.δ_naturality {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} {S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) : CategoryTheory.CategoryStruct.comp (hS₁.δ i j hij) (HomologicalComplex.homologyMap φ.τ₁ j) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ.τ₃ i) (hS₂.δ i j hij)

noncomputable def HomologicalComplex.HomologySequence.composableArrows₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} (S : CategoryTheory.ShortComplex (HomologicalComplex C c)) (i : ι) : CategoryTheory.ComposableArrows C 2

The (exact) sequence S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i

Equations

• HomologicalComplex.HomologySequence.composableArrows₂ S i = CategoryTheory.ComposableArrows.mk₂ (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i)

theorem HomologicalComplex.HomologySequence.composableArrows₂_exact {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS₁ : S₁.ShortExact) (i : ι) : (HomologicalComplex.HomologySequence.composableArrows₂ S₁ i).Exact

noncomputable def HomologicalComplex.HomologySequence.composableArrows₅ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS₁ : S₁.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) : CategoryTheory.ComposableArrows C 5

The (exact) sequence H_i(S.X₁) ⟶ H_i(S.X₂) ⟶ H_i(S.X₃) ⟶ H_j(S.X₁) ⟶ H_j(S.X₂) ⟶ H_j(S.X₃) when c.Rel i j and S is a short exact short complex of homological complexes in an abelian category.

Equations

• One or more equations did not get rendered due to their size.

theorem HomologicalComplex.HomologySequence.composableArrows₅_exact {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS₁ : S₁.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) : (HomologicalComplex.HomologySequence.composableArrows₅ hS₁ i j hij).Exact

noncomputable def HomologicalComplex.HomologySequence.mapComposableArrows₂ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} {S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (i : ι) : HomologicalComplex.HomologySequence.composableArrows₂ S₁ i ⟶ HomologicalComplex.HomologySequence.composableArrows₂ S₂ i

The map between the exact sequences S₁.X₁.homology i ⟶ S₁.X₂.homology i ⟶ S₁.X₃.homology i and S₂.X₁.homology i ⟶ S₂.X₂.homology i ⟶ S₂.X₃.homology i that is induced by φ : S₁ ⟶ S₂.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HomologicalComplex.HomologySequence.mapComposableArrows₅ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} {S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (j : ι) (hij : c.Rel i j) : HomologicalComplex.HomologySequence.composableArrows₅ hS₁ i j hij ⟶ HomologicalComplex.HomologySequence.composableArrows₅ hS₂ i j hij

The map composableArrows₅ hS₁ i j hij ⟶ composableArrows₅ hS₂ i j hij of exact sequences induced by a morphism φ : S₁ ⟶ S₂ between short exact short complexes of homological complexes.

Equations

• One or more equations did not get rendered due to their size.

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

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

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

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