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 #
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 :
A functor from a pretriangulated category to an abelian category is an homological functor if it sends distinguished triangles to exact sequences.
- exact (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) : ((Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact
Instances
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
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)
[Limits.HasZeroObject C]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[Abelian A]
[F.IsHomological]
:
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))) ⋯ ⋯ ⋯
Instances For
instance
CategoryTheory.Functor.instClosedUnderIsomorphismsPHomologicalKernel
{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]
:
ClosedUnderIsomorphisms F.homologicalKernel.P
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)
[Limits.HasZeroObject C]
[Preadditive C]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
[Abelian A]
[F.IsHomological]
[F.ShiftSequence ℤ]
(X : C)
:
F.homologicalKernel.P X ↔ ∀ (n : ℤ), Limits.IsZero ((F.shift n).obj X)
@[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]
:
@[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₁ ⋯
Instances For
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₀ : ℤ)
:
(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}
[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₁)
:
(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}
[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₁)
:
(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}
[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₀ : ℤ)
:
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₁)
:
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₁)
:
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₀ : ℤ)
:
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)
:
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.
Instances For
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