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 : ℤ.
Instances For
noncomputable def
DerivedCategory.homologyFunctorFactors
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(n : ℤ)
:
The homology functor on the derived category is induced by the homology functor on the category of cochain complexes.
Instances For
@[simp]
theorem
DerivedCategory.homologyFunctorFactors_hom_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
{K L : CochainComplex C ℤ}
(f : K ⟶ L)
(n : ℤ)
:
CategoryTheory.CategoryStruct.comp ((homologyFunctor C n).map (Q.map f)) ((homologyFunctorFactors C n).hom.app L) = CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C n).hom.app K) (HomologicalComplex.homologyMap f n)
@[simp]
theorem
DerivedCategory.homologyFunctorFactors_hom_naturality_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
{K L : CochainComplex C ℤ}
(f : K ⟶ L)
(n : ℤ)
{Z : C}
(h : (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) n).obj L ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((homologyFunctor C n).map (Q.map f))
(CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C n).hom.app L) h) = CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C n).hom.app K)
(CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap f n) h)
noncomputable def
DerivedCategory.homologyFunctorFactorsh
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(n : ℤ)
:
The homology functor on the derived category is induced by the homology functor on the homotopy category of cochain complexes.
Instances For
theorem
DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(K : CochainComplex C ℤ)
(n : ℤ)
:
(homologyFunctorFactorsh C n).hom.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) = CategoryTheory.CategoryStruct.comp ((homologyFunctor C n).map ((quotientCompQhIso C).hom.app K))
(CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C n).hom.app K)
((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n).inv.app K))
theorem
DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(K : CochainComplex C ℤ)
(n : ℤ)
{Z : C}
(h :
(HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n).obj
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
((homologyFunctorFactorsh C n).hom.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)) h = CategoryTheory.CategoryStruct.comp ((homologyFunctor C n).map ((quotientCompQhIso C).hom.app K))
(CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C n).hom.app K)
(CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n).inv.app K)
h))
theorem
DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(K : CochainComplex C ℤ)
(n : ℤ)
:
(homologyFunctorFactorsh C n).inv.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n).hom.app K)
(CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C n).inv.app K)
((homologyFunctor C n).map ((quotientCompQhIso C).inv.app K)))
theorem
DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(K : CochainComplex C ℤ)
(n : ℤ)
{Z : C}
(h : (homologyFunctor C n).obj (Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
((homologyFunctorFactorsh C n).inv.app ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)) h = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n).hom.app K)
(CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C n).inv.app K)
(CategoryTheory.CategoryStruct.comp ((homologyFunctor C n).map ((quotientCompQhIso C).inv.app K)) h))
theorem
DerivedCategory.isIso_Qh_map_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
{X Y : HomotopyCategory C (ComplexShape.up ℤ)}
(f : X ⟶ Y)
:
CategoryTheory.IsIso (Qh.map f) ↔ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f
instance
DerivedCategory.instIsHomologicalHomologyFunctor
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(n : ℤ)
:
(homologyFunctor C n).IsHomological
@[implicit_reducible]
noncomputable instance
DerivedCategory.instShiftSequenceHomologyFunctorOfNatInt
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
:
(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.
theorem
DerivedCategory.shift_homologyFunctor
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(n : ℤ)
:
(homologyFunctor C 0).shift n = homologyFunctor C n
theorem
DerivedCategory.shiftMap_homologyFunctor_map_Qh
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
{K L : HomotopyCategory C (ComplexShape.up ℤ)}
{n : ℤ}
(f : K ⟶ (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj L)
(a a' : ℤ)
(h : n + a = a' := by lia)
:
(homologyFunctor C 0).shiftMap (CategoryTheory.ShiftedHom.map f Qh) a a' h = CategoryTheory.CategoryStruct.comp ((homologyFunctorFactorsh C a).hom.app K)
(CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
((homologyFunctorFactorsh C a').inv.app L))
theorem
DerivedCategory.shiftMap_homologyFunctor_map_Qh_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
{K L : HomotopyCategory C (ComplexShape.up ℤ)}
{n : ℤ}
(f : K ⟶ (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj L)
(a a' : ℤ)
(h : n + a = a' := by lia)
{Z : C}
(h✝ : ((homologyFunctor C 0).shift a').obj (Qh.obj L) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((homologyFunctor C 0).shiftMap (CategoryTheory.ShiftedHom.map f Qh) a a' h) h✝ = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp ((homologyFunctorFactorsh C a).hom.app K)
(CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
((homologyFunctorFactorsh C a').inv.app L)))
h✝
theorem
DerivedCategory.shiftMap_homologyFunctor_map_Q
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
{K L : CochainComplex C ℤ}
{n : ℤ}
(f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
(a a' : ℤ)
(h : n + a = a' := by lia)
:
(homologyFunctor C 0).shiftMap (CategoryTheory.ShiftedHom.map f Q) a a' h = CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C a).hom.app K)
(CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
((homologyFunctorFactors C a').inv.app L))
theorem
DerivedCategory.shiftMap_homologyFunctor_map_Q_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
{K L : CochainComplex C ℤ}
{n : ℤ}
(f : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
(a a' : ℤ)
(h : n + a = a' := by lia)
{Z : C}
(h✝ : ((homologyFunctor C 0).shift a').obj (Q.obj L) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((homologyFunctor C 0).shiftMap (CategoryTheory.ShiftedHom.map f Q) a a' h) h✝ = CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C a).hom.app K)
(CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap f a a' h)
(CategoryTheory.CategoryStruct.comp ((homologyFunctorFactors C a').inv.app L) h✝))
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₁ := by lia)
:
The connecting homomorphism on the homology sequence attached to a distinguished triangle in the derived category.
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₁ := by lia)
:
CategoryTheory.CategoryStruct.comp ((homologyFunctor C n₀).map T.mor₂) (δ 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₁ := by lia)
{Z : C}
(h✝ : (homologyFunctor C n₁).obj T.obj₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((homologyFunctor C n₀).map T.mor₂)
(CategoryTheory.CategoryStruct.comp (δ 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₁ := by lia)
:
CategoryTheory.CategoryStruct.comp (δ T n₀ n₁ h) ((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₁ := by lia)
{Z : C}
(h✝ : (homologyFunctor C n₁).obj T.obj₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (δ T n₀ n₁ h)
(CategoryTheory.CategoryStruct.comp ((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₀ : ℤ)
:
{ X₁ := (homologyFunctor C n₀).obj T.obj₁, X₂ := (homologyFunctor C n₀).obj T.obj₂,
X₃ := (homologyFunctor C n₀).obj T.obj₃, f := (homologyFunctor C n₀).map T.mor₁,
g := (homologyFunctor C n₀).map T.mor₂, zero := ⋯ }.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₁ := by lia)
:
{ X₁ := (homologyFunctor C n₀).obj T.obj₂, X₂ := (homologyFunctor C n₀).obj T.obj₃,
X₃ := (homologyFunctor C n₁).obj T.obj₁, f := (homologyFunctor C n₀).map T.mor₂, g := δ T n₀ n₁ h, zero := ⋯ }.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₁ := by lia)
:
{ X₁ := (homologyFunctor C n₀).obj T.obj₃, X₂ := (homologyFunctor C n₁).obj T.obj₁,
X₃ := (homologyFunctor C n₁).obj T.obj₂, f := δ T n₀ n₁ h, g := (homologyFunctor C n₁).map T.mor₁, zero := ⋯ }.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 ((homologyFunctor C n₀).map T.mor₁) ↔ (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₁ := by lia)
:
CategoryTheory.Mono ((homologyFunctor C n₁).map T.mor₁) ↔ δ 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₁ := by lia)
:
CategoryTheory.Epi ((homologyFunctor C n₀).map T.mor₂) ↔ δ 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 ((homologyFunctor C n₀).map T.mor₂) ↔ (homologyFunctor C n₀).map T.mor₁ = 0
noncomputable def
CochainComplex.homologyδOfTriangle
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(n₀ n₁ : ℤ)
(h : n₀ + 1 = n₁ := by lia)
:
If T is a triangle in CochainComplex C ℤ, this is the connecting homomorphism
T.obj₃.homology n₀ ⟶ T.obj₁.homology n₁ in homology when n₀ + 1 = n₁.
Instances For
@[simp]
theorem
CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(n₀ n₁ : ℤ)
(h : n₀ + 1 = n₁ := by lia)
:
CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃)
(homologyδOfTriangle T n₀ n₁ h) = CategoryTheory.CategoryStruct.comp (DerivedCategory.HomologySequence.δ (DerivedCategory.Q.mapTriangle.obj T) n₀ n₁ h)
((DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₁)
@[simp]
theorem
CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(n₀ n₁ : ℤ)
(h : n₀ + 1 = n₁ := by lia)
{Z : C}
(h✝ : HomologicalComplex.homology T.obj₁ n₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃)
(CategoryTheory.CategoryStruct.comp (homologyδOfTriangle T n₀ n₁ h) h✝) = CategoryTheory.CategoryStruct.comp (DerivedCategory.HomologySequence.δ (DerivedCategory.Q.mapTriangle.obj T) n₀ n₁ h)
(CategoryTheory.CategoryStruct.comp ((DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₁) h✝)
theorem
CochainComplex.homologyMap_comp_eq_zero_of_distTriang
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(n : ℤ)
:
theorem
CochainComplex.homologyMap_comp_eq_zero_of_distTriang_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(n : ℤ)
{Z : C}
(h : HomologicalComplex.homology T.obj₃ n ⟶ Z)
:
theorem
CochainComplex.homologyδOfTriangle_homologyMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(n₀ n₁ : ℤ)
(h : n₀ + 1 = n₁ := by lia)
:
CategoryTheory.CategoryStruct.comp (homologyδOfTriangle T n₀ n₁ h) (HomologicalComplex.homologyMap T.mor₁ n₁) = 0
theorem
CochainComplex.homologyδOfTriangle_homologyMap_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(n₀ n₁ : ℤ)
(h : n₀ + 1 = n₁ := by lia)
{Z : C}
(h✝ : HomologicalComplex.homology T.obj₂ n₁ ⟶ Z)
:
theorem
CochainComplex.homologyMap_homologyδOfTriangle
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(n₀ n₁ : ℤ)
(h : n₀ + 1 = n₁ := by lia)
:
CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap T.mor₂ n₀) (homologyδOfTriangle T n₀ n₁ h) = 0
theorem
CochainComplex.homologyMap_homologyδOfTriangle_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(n₀ n₁ : ℤ)
(h : n₀ + 1 = n₁ := by lia)
{Z : C}
(h✝ : HomologicalComplex.homology T.obj₁ n₁ ⟶ Z)
:
theorem
CochainComplex.homologyMap_exact₁_of_distTriang
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(n₀ n₁ : ℤ)
(h : n₀ + 1 = n₁ := by lia)
:
{ X₁ := HomologicalComplex.homology T.obj₃ n₀, X₂ := HomologicalComplex.homology T.obj₁ n₁,
X₃ := HomologicalComplex.homology T.obj₂ n₁, f := homologyδOfTriangle T n₀ n₁ h,
g := HomologicalComplex.homologyMap T.mor₁ n₁, zero := ⋯ }.Exact
theorem
CochainComplex.homologyMap_exact₂_of_distTriang
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(n : ℤ)
:
{ X₁ := HomologicalComplex.homology T.obj₁ n, X₂ := HomologicalComplex.homology T.obj₂ n,
X₃ := HomologicalComplex.homology T.obj₃ n, f := HomologicalComplex.homologyMap T.mor₁ n,
g := HomologicalComplex.homologyMap T.mor₂ n, zero := ⋯ }.Exact
theorem
CochainComplex.homologyMap_exact₃_of_distTriang
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[HasDerivedCategory C]
(T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ))
(hT : DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
(n₀ n₁ : ℤ)
(h : n₀ + 1 = n₁ := by lia)
:
{ X₁ := HomologicalComplex.homology T.obj₂ n₀, X₂ := HomologicalComplex.homology T.obj₃ n₀,
X₃ := HomologicalComplex.homology T.obj₁ n₁, f := HomologicalComplex.homologyMap T.mor₂ n₀,
g := homologyδOfTriangle T n₀ n₁ h, zero := ⋯ }.Exact