Documentation

Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

The homology sequence #

In this file, we construct homologyFunctor C n : DerivedCategory C ⥤ C for all n : ℤ, show that they are homological functors which form a shift sequence, and construct the long exact homology sequences associated to distinguished triangles in the derived category.

The homology functor on the derived category is induced by the homology functor on the category of cochain complexes.

Equations
Instances For

    The homology functor on the derived category is induced by the homology functor on the homotopy category of cochain complexes.

    Equations
    Instances For

      The functors homologyFunctor C n : DerivedCategory C ⥤ C for all n : ℤ are part of a "shift sequence", i.e. they satisfy compatibilities with shifts.

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

      The connecting homomorphism on the homology sequence attached to a distinguished triangle in the derived category.

      Equations
      Instances For
        @[simp]
        theorem DerivedCategory.HomologySequence.comp_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)) (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ) (n₁ : ) (h : n₀ + 1 = n₁) :
        @[simp]
        theorem DerivedCategory.HomologySequence.δ_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)) (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ) (n₁ : ) (h : n₀ + 1 = n₁) :
        theorem DerivedCategory.HomologySequence.exact₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)) (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ) :
        (CategoryTheory.ShortComplex.mk ((DerivedCategory.homologyFunctor C n₀).map T.mor₁) ((DerivedCategory.homologyFunctor C n₀).map T.mor₂) ).Exact
        theorem DerivedCategory.HomologySequence.exact₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)) (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ) (n₁ : ) (h : n₀ + 1 = n₁) :
        theorem DerivedCategory.HomologySequence.exact₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)) (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ) (n₁ : ) (h : n₀ + 1 = n₁) :