The pretriangulated structure on the homotopy category of complexes
In this file, we define the pretriangulated structure on the homotopy
category HomotopyCategory C (ComplexShape.up ℤ) of an additive category C.
The distinguished triangles are the triangles that are isomorphic to the
image in the homotopy category of the standard triangle
K ⟶ L ⟶ mappingCone φ ⟶ K⟦(1 : ℤ)⟧ for some morphism of
cochain complexes φ : K ⟶ L.
This result first appeared in the Liquid Tensor Experiment. In the LTE, the formalization followed the Stacks Project: in particular, the distinguished triangles were defined using degreewise-split short exact sequences of cochain complexes. Here, we follow the original definitions in [Verdier's thesis, I.3][verdier1996] (with the better sign conventions from the introduction of [Brian Conrad's book Grothendieck duality and base change][conrad2000]).
References #
- [Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes][verdier1996]
- [Brian Conrad, Grothendieck duality and base change][conrad2000]
- https://stacks.math.columbia.edu/tag/014P
noncomputable def
CochainComplex.mappingCone.triangle
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
The standard triangle K ⟶ L ⟶ mappingCone φ ⟶ K⟦(1 : ℤ)⟧ in CochainComplex C ℤ
attached to a morphism φ : K ⟶ L. It involves φ, inr φ : L ⟶ mappingCone φ and
the morphism induced by the 1-cocycle -mappingCone.fst φ.
Instances For
@[simp]
theorem
CochainComplex.mappingCone.triangle_mor₂
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
@[simp]
theorem
CochainComplex.mappingCone.triangle_obj₂
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
@[simp]
theorem
CochainComplex.mappingCone.triangle_obj₁
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
@[simp]
theorem
CochainComplex.mappingCone.triangle_obj₃
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
(triangle φ).obj₃ = mappingCone φ
@[simp]
theorem
CochainComplex.mappingCone.triangle_mor₁
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
@[simp]
theorem
CochainComplex.mappingCone.inl_v_triangle_mor₃_f
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(p q : ℤ)
(hpq : p + -1 = q)
:
CategoryTheory.CategoryStruct.comp ((inl φ).v p q hpq) ((triangle φ).mor₃.f q) = -(K.shiftFunctorObjXIso 1 q p ⋯).inv
@[simp]
theorem
CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(p q : ℤ)
(hpq : p + -1 = q)
{Z : C}
(h : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (triangle φ).obj₁).X q ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((inl φ).v p q hpq) (CategoryTheory.CategoryStruct.comp ((triangle φ).mor₃.f q) h) = CategoryTheory.CategoryStruct.comp (-(K.shiftFunctorObjXIso 1 q p ⋯).inv) h
@[simp]
theorem
CochainComplex.mappingCone.inr_f_triangle_mor₃_f
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(p : ℤ)
:
@[simp]
theorem
CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(p : ℤ)
{Z : C}
(h : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (triangle φ).obj₁).X p ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((inr φ).f p) (CategoryTheory.CategoryStruct.comp ((triangle φ).mor₃.f p) h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
CochainComplex.mappingCone.inr_triangleδ
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
CategoryTheory.CategoryStruct.comp (inr φ) (triangle φ).mor₃ = 0
@[simp]
theorem
CochainComplex.mappingCone.inr_triangleδ_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
{Z : CochainComplex C ℤ}
(h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (triangle φ).obj₁ ⟶ Z)
:
@[reducible, inline]
noncomputable abbrev
CochainComplex.mappingCone.triangleh
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
The (distinguished) triangle in the homotopy category that is associated to
a morphism φ : K ⟶ L in the category CochainComplex C ℤ.
Instances For
noncomputable def
CochainComplex.mappingCone.homotopyToZeroOfId
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(K : CochainComplex C ℤ)
:
The mapping cone of the identity is contractible.
Instances For
noncomputable def
CochainComplex.mappingCone.mapOfHomotopy
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
The morphism mappingCone φ₁ ⟶ mappingCone φ₂ that is induced by a square that
is commutative up to homotopy.
Instances For
theorem
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
CategoryTheory.CategoryStruct.comp (inr φ₁) (mapOfHomotopy H) = CategoryTheory.CategoryStruct.comp b (inr φ₂)
theorem
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
{Z : CochainComplex C ℤ}
(h : mappingCone φ₂ ⟶ Z)
:
theorem
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
CategoryTheory.CategoryStruct.comp (mapOfHomotopy H) (triangle φ₂).mor₃ = CategoryTheory.CategoryStruct.comp (triangle φ₁).mor₃ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a)
theorem
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
{Z : CochainComplex C ℤ}
(h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (triangle φ₂).obj₁ ⟶ Z)
:
noncomputable def
CochainComplex.mappingCone.trianglehMapOfHomotopy
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
The morphism triangleh φ₁ ⟶ triangleh φ₂ that is induced by a square that
is commutative up to homotopy.
Instances For
@[simp]
theorem
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
(trianglehMapOfHomotopy H).hom₁ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a
@[simp]
theorem
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
(trianglehMapOfHomotopy H).hom₂ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map b
@[simp]
theorem
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
(trianglehMapOfHomotopy H).hom₃ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H)
noncomputable def
CochainComplex.mappingCone.map
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
:
The morphism mappingCone φ₁ ⟶ mappingCone φ₂ that is induced by a commutative square.
Instances For
theorem
CochainComplex.mappingCone.map_eq_mapOfHomotopy
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
:
map φ₁ φ₂ a b comm = mapOfHomotopy (Homotopy.ofEq comm)
theorem
CochainComplex.mappingCone.map_id
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
theorem
CochainComplex.mappingCone.map_comp
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(φ₃ : K₃ ⟶ L₃)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
(a' : K₂ ⟶ K₃)
(b' : L₂ ⟶ L₃)
(comm' : CategoryTheory.CategoryStruct.comp φ₂ b' = CategoryTheory.CategoryStruct.comp a' φ₃)
:
map φ₁ φ₃ (CategoryTheory.CategoryStruct.comp a a') (CategoryTheory.CategoryStruct.comp b b') ⋯ = CategoryTheory.CategoryStruct.comp (map φ₁ φ₂ a b comm) (map φ₂ φ₃ a' b' comm')
theorem
CochainComplex.mappingCone.map_comp_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(φ₃ : K₃ ⟶ L₃)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
(a' : K₂ ⟶ K₃)
(b' : L₂ ⟶ L₃)
(comm' : CategoryTheory.CategoryStruct.comp φ₂ b' = CategoryTheory.CategoryStruct.comp a' φ₃)
{Z : CochainComplex C ℤ}
(h : mappingCone φ₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(map φ₁ φ₃ (CategoryTheory.CategoryStruct.comp a a') (CategoryTheory.CategoryStruct.comp b b') ⋯) h = CategoryTheory.CategoryStruct.comp (map φ₁ φ₂ a b comm) (CategoryTheory.CategoryStruct.comp (map φ₂ φ₃ a' b' comm') h)
noncomputable def
CochainComplex.mappingCone.triangleMap
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
:
The morphism triangle φ₁ ⟶ triangle φ₂ that is induced by a commutative square.
Instances For
@[simp]
theorem
CochainComplex.mappingCone.triangleMap_hom₃
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
:
(triangleMap φ₁ φ₂ a b comm).hom₃ = map φ₁ φ₂ a b comm
@[simp]
theorem
CochainComplex.mappingCone.triangleMap_hom₁
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
:
(triangleMap φ₁ φ₂ a b comm).hom₁ = a
@[simp]
theorem
CochainComplex.mappingCone.triangleMap_hom₂
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ L₁ K₂ L₂ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
:
(triangleMap φ₁ φ₂ a b comm).hom₂ = b
noncomputable def
CochainComplex.mappingCone.rotateHomotopyEquiv
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
HomotopyEquiv ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj K) (mappingCone (inr φ))
Given φ : K ⟶ L, K⟦(1 : ℤ)⟧ is homotopy equivalent to
the mapping cone of inr φ : L ⟶ mappingCone φ.
Instances For
noncomputable def
CochainComplex.mappingCone.rotateHomotopyEquivComm₂Homotopy
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
Homotopy (CategoryTheory.CategoryStruct.comp (triangle φ).mor₃ (rotateHomotopyEquiv φ).hom) (inr (inr φ))
Auxiliary definition for rotateTrianglehIso.
Instances For
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ).mor₃)
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (rotateHomotopyEquiv φ).hom) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (inr φ))
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
{Z : HomotopyCategory C (ComplexShape.up ℤ)}
(h : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj (mappingCone (inr φ)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle φ).mor₃)
(CategoryTheory.CategoryStruct.comp
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (rotateHomotopyEquiv φ).hom) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (inr φ))) h
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
CategoryTheory.CategoryStruct.comp (rotateHomotopyEquiv φ).hom (triangle (inr φ)).mor₃ = -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
{Z : HomologicalComplex C (ComplexShape.up ℤ)}
(h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (triangle (inr φ)).obj₁ ⟶ Z)
:
noncomputable def
CochainComplex.mappingCone.rotateTrianglehIso
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
The canonical isomorphism of triangles (triangleh φ).rotate ≅ (triangleh (inr φ)).
Instances For
noncomputable def
CochainComplex.mappingCone.shiftIso
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(n : ℤ)
:
(CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj (mappingCone φ) ≅ mappingCone ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)
The canonical isomorphism (mappingCone φ)⟦n⟧ ≅ mappingCone (φ⟦n⟧').
Instances For
noncomputable def
CochainComplex.mappingCone.shiftTriangleIso
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(n : ℤ)
:
(CategoryTheory.Pretriangulated.Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ) ≅ triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)
The canonical isomorphism (triangle φ)⟦n⟧ ≅ triangle (φ⟦n⟧').
Instances For
noncomputable def
CochainComplex.mappingCone.shiftTrianglehIso
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(n : ℤ)
:
(CategoryTheory.Pretriangulated.Triangle.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).obj (triangleh φ) ≅ triangleh ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)
The canonical isomorphism (triangleh φ)⟦n⟧ ≅ triangleh (φ⟦n⟧').
Instances For
theorem
CochainComplex.mappingCone.map_δ
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Category.{v_2, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(G : CategoryTheory.Functor C D)
[G.Additive]
:
CategoryTheory.CategoryStruct.comp ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map (triangle φ).mor₃)
((CategoryTheory.Functor.commShiftIso (G.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app K) = CategoryTheory.CategoryStruct.comp (mapHomologicalComplexIso φ G).hom
(triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃
noncomputable def
CochainComplex.mappingCone.mapTriangleIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Category.{v_2, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(G : CategoryTheory.Functor C D)
[G.Additive]
:
(G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ) ≅ triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
If φ : K ⟶ L is a morphism of cochain complexes in C and G : C ⥤ D is an
additive functor, then the image by G of the triangle triangle φ identifies to
the triangle associated to the image of φ by G.
Instances For
noncomputable def
CochainComplex.mappingCone.mapTrianglehIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Category.{v_2, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{K L : CochainComplex C ℤ}
(φ : K ⟶ L)
(G : CategoryTheory.Functor C D)
[G.Additive]
:
(G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.obj (triangleh φ) ≅ triangleh ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
If φ : K ⟶ L is a morphism of cochain complexes in C and G : C ⥤ D is an
additive functor, then the image by G of the triangle triangleh φ identifies to
the triangle associated to the image of φ by G.
Instances For
def
HomotopyCategory.Pretriangulated.distinguishedTriangles
(C : Type u_1)
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
:
A triangle in HomotopyCategory C (ComplexShape.up ℤ) is distinguished if it is isomorphic to
the triangle CochainComplex.mappingCone.triangleh φ for some morphism of cochain
complexes φ.
Instances For
theorem
HomotopyCategory.Pretriangulated.isomorphic_distinguished
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T₁ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(hT₁ : T₁ ∈ distinguishedTriangles C)
(T₂ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(e : T₂ ≅ T₁)
:
T₂ ∈ distinguishedTriangles C
theorem
HomotopyCategory.Pretriangulated.distinguished_cocone_triangle
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X Y : HomotopyCategory C (ComplexShape.up ℤ)}
(f : X ⟶ Y)
:
∃ (Z : HomotopyCategory C (ComplexShape.up ℤ)) (g : Y ⟶ Z) (h :
Z ⟶ (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).obj X),
CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ distinguishedTriangles C
theorem
HomotopyCategory.Pretriangulated.rotate_distinguished_triangle'
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(hT : T ∈ distinguishedTriangles C)
:
T.rotate ∈ distinguishedTriangles C
theorem
HomotopyCategory.Pretriangulated.shift_distinguished_triangle
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(hT : T ∈ distinguishedTriangles C)
(n : ℤ)
:
theorem
HomotopyCategory.Pretriangulated.invRotate_distinguished_triangle'
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(hT : T ∈ distinguishedTriangles C)
:
theorem
HomotopyCategory.Pretriangulated.rotate_distinguished_triangle
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
:
T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C
theorem
HomotopyCategory.Pretriangulated.complete_distinguished_triangle_morphism
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T₁ T₂ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(hT₁ : T₁ ∈ distinguishedTriangles C)
(hT₂ : T₂ ∈ distinguishedTriangles C)
(a : T₁.obj₁ ⟶ T₂.obj₁)
(b : T₁.obj₂ ⟶ T₂.obj₂)
(fac : CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁)
:
∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₃
((CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃
@[implicit_reducible]
noncomputable instance
HomotopyCategory.instPretriangulatedIntUp
(C : Type u_1)
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Limits.HasZeroObject C]
:
theorem
HomotopyCategory.mappingCone_triangleh_distinguished
{C : Type u_1}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Limits.HasZeroObject C]
{X Y : CochainComplex C ℤ}
(f : X ⟶ Y)
:
instance
HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Category.{v_2, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasZeroObject D]
(G : CategoryTheory.Functor C D)
[G.Additive]
: