Documentation

Mathlib.Algebra.Homology.HomologySequenceLemmas

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).

source
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₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j) :
snakeInput hS₁ i j hij ⟶ 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
    Instances For
      source
      @[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₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j) :
      (mapSnakeInput φ hS₁ hS₂ i j hij).f₂ = (cyclesFunctor C c j).mapShortComplex.map φ
      source
      @[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₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j) :
      (mapSnakeInput φ hS₁ hS₂ i j hij).f₀ = (homologyFunctor C c i).mapShortComplex.map φ
      source
      @[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₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j) :
      (mapSnakeInput φ hS₁ hS₂ i j hij).f₃ = (homologyFunctor C c j).mapShortComplex.map φ
      source
      @[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₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j) :
      (mapSnakeInput φ hS₁ hS₂ i j hij).f₁ = (opcyclesFunctor C c i).mapShortComplex.map φ
      source
      theorem HomologicalComplex.HomologySequence.δ_naturality {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] {c : ComplexShape ι} {S₁ 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) (homologyMap φ.τ₁ j) = CategoryTheory.CategoryStruct.comp (homologyMap φ.τ₃ i) (hS₂.δ i j hij)
      source
      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₁ 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 (homologyMap φ.τ₁ j) h) = CategoryTheory.CategoryStruct.comp (homologyMap φ.τ₃ i) (CategoryTheory.CategoryStruct.comp (hS₂.δ i j hij) h)
      source
      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
        Instances For
          source
          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 : ι) :
          (composableArrows₂ S₁ i).Exact
          source
          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
            Instances For
              source
              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) :
              (composableArrows₅ hS₁ i j hij).Exact
              source
              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₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (i : ι) :
              composableArrows₂ S₁ i ⟶ 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
                Instances For
                  source
                  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₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j) :
                  composableArrows₅ hS₁ i j hij ⟶ 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
                    Instances For
                      source
                      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₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (h₁ : CategoryTheory.Epi (homologyMap φ.τ₁ i)) (h₂ : CategoryTheory.Mono (homologyMap φ.τ₂ i)) (h₃ : ∀ (j : ι), c.Rel i j → CategoryTheory.Mono (homologyMap φ.τ₁ j)) :
                      CategoryTheory.Mono (homologyMap φ.τ₃ i)
                      source
                      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₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (h₁ : CategoryTheory.Epi (homologyMap φ.τ₂ i)) (h₂ : ∀ (j : ι), c.Rel i j → CategoryTheory.Epi (homologyMap φ.τ₁ j)) (h₃ : ∀ (j : ι), c.Rel i j → CategoryTheory.Mono (homologyMap φ.τ₂ j)) :
                      CategoryTheory.Epi (homologyMap φ.τ₃ i)
                      source
                      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₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂) (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i : ι) (h₁ : CategoryTheory.Epi (homologyMap φ.τ₁ i)) (h₂ : CategoryTheory.IsIso (homologyMap φ.τ₂ i)) (h₃ : ∀ (j : ι), c.Rel i j → CategoryTheory.IsIso (homologyMap φ.τ₁ j)) (h₄ : ∀ (j : ι), c.Rel i j → CategoryTheory.Mono (homologyMap φ.τ₂ j)) :
                      CategoryTheory.IsIso (homologyMap φ.τ₃ i)
                      source
                      theorem HomologicalComplex.HomologySequence.quasiIso_τ₃ {C : Type u_1} {ι : Type u_2} [CategoryTheory.Category.{u_3, 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 φ.τ₃