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 : ℤ)
:
The homology functor DerivedCategory C ⥤ C in degree n : ℤ.
Equations
Instances For
noncomputable def
DerivedCategory.homologyFunctorFactors
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(n : ℤ)
:
DerivedCategory.Q.comp (DerivedCategory.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.
Equations
Instances For
noncomputable def
DerivedCategory.homologyFunctorFactorsh
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(n : ℤ)
:
DerivedCategory.Qh.comp (DerivedCategory.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.
Equations
Instances For
instance
DerivedCategory.instIsHomologicalHomologyFunctor
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(n : ℤ)
:
(DerivedCategory.homologyFunctor C n).IsHomological
noncomputable instance
DerivedCategory.instShiftSequenceHomologyFunctorOfNatInt
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
:
(DerivedCategory.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.
Equations
- One or more equations did not get rendered due to their size.
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₁)
:
(DerivedCategory.homologyFunctor C n₀).obj T.obj₃ ⟶ (DerivedCategory.homologyFunctor C n₁).obj T.obj₁
The connecting homomorphism on the homology sequence attached to a distinguished triangle in the derived category.
Equations
- DerivedCategory.HomologySequence.δ T n₀ n₁ h = (DerivedCategory.homologyFunctor C 0).shiftMap T.mor₃ n₀ n₁ ⋯
Instances For
@[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 ((DerivedCategory.homologyFunctor C n₀).map T.mor₂)
(DerivedCategory.HomologySequence.δ 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✝ : (DerivedCategory.homologyFunctor C n₁).obj T.obj₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctor C n₀).map T.mor₂)
(CategoryTheory.CategoryStruct.comp (DerivedCategory.HomologySequence.δ 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 (DerivedCategory.HomologySequence.δ T n₀ n₁ h)
((DerivedCategory.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✝ : (DerivedCategory.homologyFunctor C n₁).obj T.obj₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (DerivedCategory.HomologySequence.δ T n₀ n₁ h)
(CategoryTheory.CategoryStruct.comp ((DerivedCategory.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₀ : ℤ)
:
(CategoryTheory.ShortComplex.mk ((DerivedCategory.homologyFunctor C n₀).map T.mor₁)
((DerivedCategory.homologyFunctor C n₀).map T.mor₂) ⋯).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₁)
:
(CategoryTheory.ShortComplex.mk ((DerivedCategory.homologyFunctor C n₀).map T.mor₂)
(DerivedCategory.HomologySequence.δ T n₀ n₁ h) ⋯).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₁)
:
(CategoryTheory.ShortComplex.mk (DerivedCategory.HomologySequence.δ T n₀ n₁ h)
((DerivedCategory.homologyFunctor C n₁).map T.mor₁) ⋯).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 ((DerivedCategory.homologyFunctor C n₀).map T.mor₁) ↔ (DerivedCategory.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 ((DerivedCategory.homologyFunctor C n₁).map T.mor₁) ↔ DerivedCategory.HomologySequence.δ 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 ((DerivedCategory.homologyFunctor C n₀).map T.mor₂) ↔ DerivedCategory.HomologySequence.δ 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 ((DerivedCategory.homologyFunctor C n₀).map T.mor₂) ↔ (DerivedCategory.homologyFunctor C n₀).map T.mor₁ = 0