Homological functors

In this file, given a functor F : C ⥤ A from a pretriangulated category to an abelian category, we define the type class F.IsHomological, which is the property that F sends distinguished triangles in C to exact sequences in A.

If F has been endowed with [F.ShiftSequence ℤ], then we may think of the functor F as a H^0, and then the H^n functors are the functors F.shift n : C ⥤ A: we have isomorphisms (F.shift n).obj X ≅ F.obj (X⟦n⟧), but through the choice of this "shift sequence", the user may provide functors with better definitional properties.

Given a triangle T in C, we define a connecting homomorphism F.homologySequenceδ T n₀ n₁ h : (F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₁ under the assumption h : n₀ + 1 = n₁. When T is distinguished, this connecting homomorphism is part of a long exact sequence ... ⟶ (F.shift n₀).obj T.obj₁ ⟶ (F.shift n₀).obj T.obj₂ ⟶ (F.shift n₀).obj T.obj₃ ⟶ ...

The exactness of this long exact sequence is given by three lemmas F.homologySequence_exact₁, F.homologySequence_exact₂ and F.homologySequence_exact₃.

If F is a homological functor, we define the strictly full triangulated subcategory F.homologicalKernel: it consists of objects X : C such that for all n : ℤ, (F.shift n).obj X (or F.obj (X⟦n⟧)) is zero. We show that a morphism f in C belongs to F.homologicalKernel.W (i.e. the cone of f is in this kernel) iff (F.shift n).map f is an isomorphism for all n : ℤ.

Note: depending on the sources, homological functors are sometimes called cohomological functors, while certain authors use "cohomological functors" for "contravariant" functors (i.e. functors Cᵒᵖ ⥤ A).

TODO

• The long exact sequence in homology attached to an homological functor.

References

• [Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes][verdier1996]

class CategoryTheory.Functor.IsHomological {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) extends CategoryTheory.Functor.PreservesZeroMorphisms : Prop

A functor from a pretriangulated category to an abelian category is an homological functor if it sends distinguished triangles to exact sequences.

• map_zero : ∀ (X Y : C), F.map 0 = 0
• exact : ∀ (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact

theorem CategoryTheory.Functor.IsHomological.exact {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] {F : CategoryTheory.Functor C A} [self : F.IsHomological] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact

theorem CategoryTheory.Functor.map_distinguished_exact {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact

instance CategoryTheory.Functor.instIsHomologicalCompOfIsTriangulated {C : Type u_1} {D : Type u_2} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Abelian A] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor D A) [L.CommShift ℤ] [L.IsTriangulated] [F.IsHomological] : (L.comp F).IsHomological

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.IsHomological.mk' {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.PreservesZeroMorphisms] (hF : ∀ (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), ∃ (T' : CategoryTheory.Pretriangulated.Triangle C) (e : T ≅ T'), ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T' ⋯).map F).Exact) : F.IsHomological

theorem CategoryTheory.Functor.IsHomological.of_iso {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] {F₁ : CategoryTheory.Functor C A} {F₂ : CategoryTheory.Functor C A} [F₁.IsHomological] (e : F₁ ≅ F₂) : F₂.IsHomological

def CategoryTheory.Functor.homologicalKernel {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] : CategoryTheory.Triangulated.Subcategory C

The kernel of a homological functor F : C ⥤ A is the strictly full triangulated subcategory consisting of objects X such that for all n : ℤ, F.obj (X⟦n⟧) is zero.

Equations

• F.homologicalKernel = CategoryTheory.Triangulated.Subcategory.mk' (fun (X : C) => ∀ (n : ℤ), CategoryTheory.Limits.IsZero (F.obj ((CategoryTheory.shiftFunctor C n).obj X))) ⋯ ⋯ ⋯

instance CategoryTheory.Functor.instClosedUnderIsomorphismsPHomologicalKernel {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] : CategoryTheory.ClosedUnderIsomorphisms F.homologicalKernel.P

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.mem_homologicalKernel_iff {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (X : C) : F.homologicalKernel.P X ↔ ∀ (n : ℤ), CategoryTheory.Limits.IsZero ((F.shift n).obj X)

@[instance 100]

noncomputable instance CategoryTheory.Functor.instPreservesLimitsOfShapeDiscreteWalkingPairOfIsHomological {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F

Equations

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

@[instance 100]

instance CategoryTheory.Functor.instAdditiveOfIsHomological {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] : F.Additive

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.isHomological_of_localization {C : Type u_1} {D : Type u_2} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.Preadditive D] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.Category.{u_6, u_3} A] [CategoryTheory.Abelian A] (L : CategoryTheory.Functor C D) [L.CommShift ℤ] [L.IsTriangulated] [L.mapArrow.EssSurj] (F : CategoryTheory.Functor D A) (G : CategoryTheory.Functor C A) (e : L.comp F ≅ G) [G.IsHomological] : F.IsHomological

noncomputable def CategoryTheory.Functor.homologySequenceδ {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Category.{u_5, u_3} A] (F : CategoryTheory.Functor C A) [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : (F.shift n₀).obj T.obj₃ ⟶ (F.shift n₁).obj T.obj₁

The connecting homomorphism in the long exact sequence attached to an homological functor and a distinguished triangle.

Equations

• F.homologySequenceδ T n₀ n₁ h = F.shiftMap T.mor₃ n₀ n₁ ⋯

theorem CategoryTheory.Functor.homologySequenceδ_naturality_assoc {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Category.{u_4, u_3} A] (F : CategoryTheory.Functor C A) [F.ShiftSequence ℤ] {T : CategoryTheory.Pretriangulated.Triangle C} {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T ⟶ T') (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : A} (h : (F.shift n₁).obj T'.obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.shift n₀).map φ.hom₃) (CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T' n₀ n₁ h✝) h) = CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h✝) (CategoryTheory.CategoryStruct.comp ((F.shift n₁).map φ.hom₁) h)

theorem CategoryTheory.Functor.homologySequenceδ_naturality {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Category.{u_4, u_3} A] (F : CategoryTheory.Functor C A) [F.ShiftSequence ℤ] {T : CategoryTheory.Pretriangulated.Triangle C} {T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T ⟶ T') (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryTheory.CategoryStruct.comp ((F.shift n₀).map φ.hom₃) (F.homologySequenceδ T' n₀ n₁ h) = CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map φ.hom₁)

theorem CategoryTheory.Functor.comp_homologySequenceδ_assoc {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : A} (h : (F.shift n₁).obj T.obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₂) (CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h✝) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.Functor.comp_homologySequenceδ {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) = 0

theorem CategoryTheory.Functor.homologySequenceδ_comp_assoc {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : A} (h : (F.shift n₁).obj T.obj₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h✝) (CategoryTheory.CategoryStruct.comp ((F.shift n₁).map T.mor₁) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.Functor.homologySequenceδ_comp {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryTheory.CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) = 0

theorem CategoryTheory.Functor.homologySequence_comp_assoc {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) {Z : A} (h : (F.shift n₀).obj T.obj₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₁) (CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₂) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem CategoryTheory.Functor.homologySequence_comp {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) : CategoryTheory.CategoryStruct.comp ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) = 0

theorem CategoryTheory.Functor.homologySequence_exact₂ {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) : (CategoryTheory.ShortComplex.mk ((F.shift n₀).map T.mor₁) ((F.shift n₀).map T.mor₂) ⋯).Exact

theorem CategoryTheory.Functor.homologySequence_exact₃ {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : (CategoryTheory.ShortComplex.mk ((F.shift n₀).map T.mor₂) (F.homologySequenceδ T n₀ n₁ h) ⋯).Exact

theorem CategoryTheory.Functor.homologySequence_exact₁ {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : (CategoryTheory.ShortComplex.mk (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map T.mor₁) ⋯).Exact

theorem CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) : CategoryTheory.Epi ((F.shift n₀).map T.mor₁) ↔ (F.shift n₀).map T.mor₂ = 0

theorem CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryTheory.Mono ((F.shift n₁).map T.mor₁) ↔ F.homologySequenceδ T n₀ n₁ h = 0

theorem CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryTheory.Epi ((F.shift n₀).map T.mor₂) ↔ F.homologySequenceδ T n₀ n₁ h = 0

theorem CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) : CategoryTheory.Mono ((F.shift n₀).map T.mor₂) ↔ (F.shift n₀).map T.mor₁ = 0

theorem CategoryTheory.Functor.mem_homologicalKernel_W_iff {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_5, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] {X : C} {Y : C} (f : X ⟶ Y) : F.homologicalKernel.W f ↔ ∀ (n : ℤ), CategoryTheory.IsIso ((F.shift n).map f)

noncomputable def CategoryTheory.Functor.homologySequenceComposableArrows₅ {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Category.{u_5, u_3} A] (F : CategoryTheory.Functor C A) [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryTheory.ComposableArrows A 5

The exact sequence with six terms starting from (F.shift n₀).obj T.obj₁ until (F.shift n₁).obj T.obj₃ when T is a distinguished triangle and F a homological functor.

Equations

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

theorem CategoryTheory.Functor.homologySequenceComposableArrows₅_exact {C : Type u_1} {A : Type u_3} [CategoryTheory.Category.{u_5, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Category.{u_4, u_3} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor C A) [F.IsHomological] [F.ShiftSequence ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ : ℤ) (n₁ : ℤ) (h : n₀ + 1 = n₁) : (F.homologySequenceComposableArrows₅ T n₀ n₁ h).Exact