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}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Category.{u_5, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.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 : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).map F).Exact
Instances
theorem
CategoryTheory.Functor.map_distinguished_exact
{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)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift 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.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[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.HasShift C ℤ]
[CategoryTheory.Category.{u_5, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_5, u_3} A]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian A]
{F₁ 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.HasShift C ℤ]
[CategoryTheory.Category.{u_5, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.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}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Category.{u_5, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_5, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_5, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian A]
[F.IsHomological]
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
CategoryTheory.Functor.instAdditiveOfIsHomological
{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)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift 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.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[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₁ ⋯
Instances For
theorem
CategoryTheory.Functor.homologySequenceδ_naturality
{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 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.homologySequenceδ_naturality_assoc
{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 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.comp_homologySequenceδ
{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)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.comp_homologySequenceδ_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)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.homologySequenceδ_comp
{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)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_4, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_4, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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_comp_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)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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_exact₂
{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)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_4, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_4, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_4, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_4, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_4, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_4, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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.HasShift C ℤ]
[CategoryTheory.Category.{u_5, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian A]
[F.IsHomological]
[F.ShiftSequence ℤ]
{X 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₁)
:
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}
[CategoryTheory.Category.{u_5, u_1} C]
[CategoryTheory.HasShift C ℤ]
[CategoryTheory.Category.{u_4, u_3} A]
(F : CategoryTheory.Functor C A)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Preadditive C]
[∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
[CategoryTheory.Pretriangulated C]
[CategoryTheory.Abelian 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