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.

noncomputable def DerivedCategory.homologyFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : CategoryTheory.Functor (DerivedCategory C) C

The homology functor DerivedCategory C ⥤ C in degree n : ℤ.

noncomputable def DerivedCategory.homologyFunctorFactors (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : Q.comp (homologyFunctor C n) ≅ HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) n

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

noncomputable def DerivedCategory.homologyFunctorFactorsh (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : Qh.comp (homologyFunctor C n) ≅ HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n

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

theorem DerivedCategory.isIso_Qh_map_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] {X Y : HomotopyCategory C (ComplexShape.up ℤ)} (f : X ⟶ Y) : CategoryTheory.IsIso (Qh.map f) ↔ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f

instance DerivedCategory.instIsHomologicalHomologyFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (homologyFunctor C n).IsHomological

noncomputable instance DerivedCategory.instShiftSequenceHomologyFunctorOfNatInt (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] : (homologyFunctor C 0).ShiftSequence ℤ

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

noncomputable def DerivedCategory.HomologySequence.δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : (homologyFunctor C n₀).obj T.obj₃ ⟶ (homologyFunctor C n₁).obj T.obj₁

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

@[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₁) : CategoryTheory.CategoryStruct.comp ((homologyFunctor C n₀).map T.mor₂) (δ T n₀ n₁ h) = 0

@[simp]

theorem DerivedCategory.HomologySequence.comp_δ_assoc {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₁) {Z : C} (h✝ : (homologyFunctor C n₁).obj T.obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((homologyFunctor C n₀).map T.mor₂) (CategoryTheory.CategoryStruct.comp (δ T n₀ n₁ h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[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₁) : CategoryTheory.CategoryStruct.comp (δ T n₀ n₁ h) ((homologyFunctor C n₁).map T.mor₁) = 0

@[simp]

theorem DerivedCategory.HomologySequence.δ_comp_assoc {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₁) {Z : C} (h✝ : (homologyFunctor C n₁).obj T.obj₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (δ T n₀ n₁ h) (CategoryTheory.CategoryStruct.comp ((homologyFunctor C n₁).map T.mor₁) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

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₀ : ℤ) : { X₁ := (homologyFunctor C n₀).obj T.obj₁, X₂ := (homologyFunctor C n₀).obj T.obj₂, X₃ := (homologyFunctor C n₀).obj T.obj₃, f := (homologyFunctor C n₀).map T.mor₁, g := (homologyFunctor C n₀).map T.mor₂, zero := ⋯ }.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₁) : { X₁ := (homologyFunctor C n₀).obj T.obj₂, X₂ := (homologyFunctor C n₀).obj T.obj₃, X₃ := (homologyFunctor C n₁).obj T.obj₁, f := (homologyFunctor C n₀).map T.mor₂, g := δ T n₀ n₁ h, zero := ⋯ }.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₁) : { X₁ := (homologyFunctor C n₀).obj T.obj₃, X₂ := (homologyFunctor C n₁).obj T.obj₁, X₃ := (homologyFunctor C n₁).obj T.obj₂, f := δ T n₀ n₁ h, g := (homologyFunctor C n₁).map T.mor₁, zero := ⋯ }.Exact

theorem DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff {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.Epi ((homologyFunctor C n₀).map T.mor₁) ↔ (homologyFunctor C n₀).map T.mor₂ = 0

theorem DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff {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₁) : CategoryTheory.Mono ((homologyFunctor C n₁).map T.mor₁) ↔ δ T n₀ n₁ h = 0

theorem DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff {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₁) : CategoryTheory.Epi ((homologyFunctor C n₀).map T.mor₂) ↔ δ T n₀ n₁ h = 0

theorem DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff {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.Mono ((homologyFunctor C n₀).map T.mor₂) ↔ (homologyFunctor C n₀).map T.mor₁ = 0