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

References

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

def CategoryTheory.Functor.homologicalKernel {C : Type u_1} {A : Type u_3} [Category.{u_4, u_1} C] [HasShift C ℤ] [Category.{u_5, u_3} A] (F : Functor C A) : ObjectProperty 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 X = ∀ (n : ℤ), CategoryTheory.Limits.IsZero (F.obj ((CategoryTheory.shiftFunctor C n).obj X))

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

class CategoryTheory.Functor.IsHomological {C : Type u_1} {A : Type u_3} [Category.{u_4, u_1} C] [HasShift C ℤ] [Category.{u_5, u_3} A] (F : Functor C A) [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Abelian A] extends F.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 : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) : ((Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact

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

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

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

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

instance CategoryTheory.Functor.instIsClosedUnderIsomorphismsHomologicalKernel {C : Type u_1} {A : Type u_3} [Category.{u_4, u_1} C] [HasShift C ℤ] [Category.{u_5, u_3} A] (F : Functor C A) : F.homologicalKernel.IsClosedUnderIsomorphisms

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

@[instance 100]

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

@[instance 100]

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

theorem CategoryTheory.Functor.isHomological_of_localization {C : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{u_4, u_1} C] [HasShift C ℤ] [Category.{u_5, u_2} D] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] [Category.{u_6, u_3} A] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Abelian A] (L : Functor C D) [L.CommShift ℤ] [L.IsTriangulated] [L.mapArrow.EssSurj] (F : Functor D A) (G : 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} [Category.{u_4, u_1} C] [HasShift C ℤ] [Category.{u_5, u_3} A] (F : Functor C A) [F.ShiftSequence ℤ] (T : 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 {C : Type u_1} {A : Type u_3} [Category.{u_4, u_1} C] [HasShift C ℤ] [Category.{u_5, u_3} A] (F : Functor C A) [F.ShiftSequence ℤ] (T T' : Pretriangulated.Triangle C) (φ : T ⟶ T') (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : CategoryStruct.comp ((F.shift n₀).map φ.hom₃) (F.homologySequenceδ T' n₀ n₁ h) = CategoryStruct.comp (F.homologySequenceδ T n₀ n₁ h) ((F.shift n₁).map φ.hom₁)

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

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

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

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

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

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

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

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

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

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

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

@[deprecated CategoryTheory.Functor.mem_homologicalKernel_trW_iff (since := "2025-07-21")]

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

Alias of CategoryTheory.Functor.mem_homologicalKernel_trW_iff.

noncomputable def CategoryTheory.Functor.homologySequenceComposableArrows₅ {C : Type u_1} {A : Type u_3} [Category.{u_4, u_1} C] [HasShift C ℤ] [Category.{u_5, u_3} A] (F : Functor C A) [F.ShiftSequence ℤ] (T : Pretriangulated.Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : 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} [Category.{u_5, u_1} C] [HasShift C ℤ] [Category.{u_4, u_3} A] (F : Functor C A) [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Abelian A] [F.IsHomological] [F.ShiftSequence ℤ] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : (F.homologySequenceComposableArrows₅ T n₀ n₁ h).Exact