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 [Verdiers'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.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{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 φ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CochainComplex.mappingCone.triangle_mor₂
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
@[simp]
theorem
CochainComplex.mappingCone.triangle_obj₁
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
(CochainComplex.mappingCone.triangle φ).obj₁ = K
@[simp]
theorem
CochainComplex.mappingCone.triangle_obj₂
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
(CochainComplex.mappingCone.triangle φ).obj₂ = L
@[simp]
theorem
CochainComplex.mappingCone.triangle_obj₃
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
@[simp]
theorem
CochainComplex.mappingCone.triangle_mor₁
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
(CochainComplex.mappingCone.triangle φ).mor₁ = φ
@[simp]
theorem
CochainComplex.mappingCone.inl_v_triangle_mor₃_f
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(p : ℤ)
(q : ℤ)
(hpq : p + -1 = q)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q hpq)
((CochainComplex.mappingCone.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.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(p : ℤ)
(q : ℤ)
(hpq : p + -1 = q)
{Z : C}
(h : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ).obj₁).X q ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v p q hpq)
(CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.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.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(p : ℤ)
:
CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
((CochainComplex.mappingCone.triangle φ).mor₃.f p) = 0
@[simp]
theorem
CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(p : ℤ)
{Z : C}
(h : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ).obj₁).X p ⟶ Z)
:
@[simp]
theorem
CochainComplex.mappingCone.inr_triangleδ
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
@[simp]
theorem
CochainComplex.mappingCone.inr_triangleδ_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
{Z : CochainComplex C ℤ}
(h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ).obj₁ ⟶ Z)
:
@[reducible, inline]
noncomputable abbrev
CochainComplex.mappingCone.triangleh
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{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 ℤ.
Equations
- CochainComplex.mappingCone.triangleh φ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj (CochainComplex.mappingCone.triangle φ)
Instances For
noncomputable def
CochainComplex.mappingCone.homotopyToZeroOfId
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(K : CochainComplex C ℤ)
:
The mapping cone of the identity is contractible.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CochainComplex.mappingCone.mapOfHomotopy
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
theorem
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{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 : CochainComplex.mappingCone φ₂ ⟶ Z)
:
theorem
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
theorem
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
{Z : HomologicalComplex C (ComplexShape.up ℤ)}
(h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ₂).obj₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.mapOfHomotopy H)
(CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ₂).mor₃ h) = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ₁).mor₃
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a) h)
noncomputable def
CochainComplex.mappingCone.trianglehMapOfHomotopy
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
(CochainComplex.mappingCone.trianglehMapOfHomotopy H).hom₁ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map a
@[simp]
theorem
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
(CochainComplex.mappingCone.trianglehMapOfHomotopy H).hom₂ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map b
@[simp]
theorem
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
{φ₁ : K₁ ⟶ L₁}
{φ₂ : K₂ ⟶ L₂}
{a : K₁ ⟶ K₂}
{b : L₁ ⟶ L₂}
(H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂))
:
noncomputable def
CochainComplex.mappingCone.map
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CochainComplex.mappingCone.map_eq_mapOfHomotopy
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
:
CochainComplex.mappingCone.map φ₁ φ₂ a b comm = CochainComplex.mappingCone.mapOfHomotopy (Homotopy.ofEq comm)
theorem
CochainComplex.mappingCone.map_id
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
theorem
CochainComplex.mappingCone.map_comp
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
{K₃ : CochainComplex C ℤ}
{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' φ₃)
:
CochainComplex.mappingCone.map φ₁ φ₃ (CategoryTheory.CategoryStruct.comp a a') (CategoryTheory.CategoryStruct.comp b b')
⋯ = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₁ φ₂ a b comm)
(CochainComplex.mappingCone.map φ₂ φ₃ a' b' comm')
theorem
CochainComplex.mappingCone.map_comp_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
{K₃ : CochainComplex C ℤ}
{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 : HomologicalComplex C (ComplexShape.up ℤ)}
(h : CochainComplex.mappingCone φ₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CochainComplex.mappingCone.map φ₁ φ₃ (CategoryTheory.CategoryStruct.comp a a')
(CategoryTheory.CategoryStruct.comp b b') ⋯)
h = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₁ φ₂ a b comm)
(CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₂ φ₃ a' b' comm') h)
noncomputable def
CochainComplex.mappingCone.triangleMap
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{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.
Equations
- CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm = { hom₁ := a, hom₂ := b, hom₃ := CochainComplex.mappingCone.map φ₁ φ₂ a b comm, comm₁ := comm, comm₂ := ⋯, comm₃ := ⋯ }
Instances For
@[simp]
theorem
CochainComplex.mappingCone.triangleMap_hom₃
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
:
(CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm).hom₃ = CochainComplex.mappingCone.map φ₁ φ₂ a b comm
@[simp]
theorem
CochainComplex.mappingCone.triangleMap_hom₂
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
:
(CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm).hom₂ = b
@[simp]
theorem
CochainComplex.mappingCone.triangleMap_hom₁
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K₁ : CochainComplex C ℤ}
{L₁ : CochainComplex C ℤ}
{K₂ : CochainComplex C ℤ}
{L₂ : CochainComplex C ℤ}
(φ₁ : K₁ ⟶ L₁)
(φ₂ : K₂ ⟶ L₂)
(a : K₁ ⟶ K₂)
(b : L₁ ⟶ L₂)
(comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂)
:
(CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm).hom₁ = a
noncomputable def
CochainComplex.mappingCone.rotateHomotopyEquiv
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
Given φ : K ⟶ L, K⟦(1 : ℤ)⟧ is homotopy equivalent to
the mapping cone of inr φ : L ⟶ mappingCone φ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CochainComplex.mappingCone.rotateHomotopyEquivComm₂Homotopy
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
Auxiliary definition for rotateTrianglehIso.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
CategoryTheory.CategoryStruct.comp
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃)
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
(CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ))
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
{Z : HomotopyCategory C (ComplexShape.up ℤ)}
(h : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (CochainComplex.mappingCone.inr φ)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃)
(CategoryTheory.CategoryStruct.comp
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom)
h) = CategoryTheory.CategoryStruct.comp
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
(CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ)))
h
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
{Z : HomologicalComplex C (ComplexShape.up ℤ)}
(h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj
(CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.inr φ)).obj₁ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom
(CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.inr φ)).mor₃
h) = CategoryTheory.CategoryStruct.comp (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ) h
noncomputable def
CochainComplex.mappingCone.rotateTrianglehIso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
The canonical isomorphism of triangles (triangleh φ).rotate ≅ (triangleh (inr φ)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CochainComplex.mappingCone.shiftIso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(n : ℤ)
:
(CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj (CochainComplex.mappingCone φ) ≅ CochainComplex.mappingCone ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)
The canonical isomorphism (mappingCone φ)⟦n⟧ ≅ mappingCone (φ⟦n⟧').
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CochainComplex.mappingCone.shiftTriangleIso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(n : ℤ)
:
The canonical isomorphism (triangle φ)⟦n⟧ ≅ triangle (φ⟦n⟧').
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CochainComplex.mappingCone.shiftTrianglehIso
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(n : ℤ)
:
The canonical isomorphism (triangleh φ)⟦n⟧ ≅ triangleh (φ⟦n⟧').
Instances For
theorem
CochainComplex.mappingCone.map_δ
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_1} C]
[CategoryTheory.Category.{u_3, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(G : CategoryTheory.Functor C D)
[G.Additive]
:
CategoryTheory.CategoryStruct.comp
((G.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle φ).mor₃)
(((G.mapHomologicalComplex (ComplexShape.up ℤ)).commShiftIso 1).hom.app K) = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.mapHomologicalComplexIso φ G).hom
(CochainComplex.mappingCone.triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃
noncomputable def
CochainComplex.mappingCone.mapTriangleIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(G : CategoryTheory.Functor C D)
[G.Additive]
:
(G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (CochainComplex.mappingCone.triangle φ) ≅ CochainComplex.mappingCone.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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CochainComplex.mappingCone.mapTrianglehIso
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Preadditive D]
[CategoryTheory.Limits.HasBinaryBiproducts D]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(G : CategoryTheory.Functor C D)
[G.Additive]
:
(G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.obj (CochainComplex.mappingCone.triangleh φ) ≅ CochainComplex.mappingCone.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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
HomotopyCategory.Pretriangulated.distinguishedTriangles
(C : Type u_1)
[CategoryTheory.Category.{u_3, 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 φ.
Equations
- HomotopyCategory.Pretriangulated.distinguishedTriangles C T = ∃ (X : CochainComplex C ℤ) (Y : CochainComplex C ℤ) (φ : X ⟶ Y), Nonempty (T ≅ CochainComplex.mappingCone.triangleh φ)
Instances For
theorem
HomotopyCategory.Pretriangulated.isomorphic_distinguished
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T₁ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(hT₁ : T₁ ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C)
(T₂ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(e : T₂ ≅ T₁)
:
theorem
HomotopyCategory.Pretriangulated.distinguished_cocone_triangle
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{X : HomotopyCategory C (ComplexShape.up ℤ)}
{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 ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
theorem
HomotopyCategory.Pretriangulated.rotate_distinguished_triangle'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(hT : T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C)
:
theorem
HomotopyCategory.Pretriangulated.shift_distinguished_triangle
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(hT : T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C)
(n : ℤ)
:
theorem
HomotopyCategory.Pretriangulated.invRotate_distinguished_triangle'
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(hT : T ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C)
:
T.invRotate ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
theorem
HomotopyCategory.Pretriangulated.complete_distinguished_triangle_morphism
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
(T₁ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(T₂ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
(hT₁ : T₁ ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C)
(hT₂ : T₂ ∈ HomotopyCategory.Pretriangulated.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₃
instance
HomotopyCategory.instPretriangulatedIntUp
(C : Type u_1)
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Limits.HasZeroObject C]
:
Equations
- One or more equations did not get rendered due to their size.
theorem
HomotopyCategory.mappingCone_triangleh_distinguished
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
[CategoryTheory.Limits.HasZeroObject C]
{X : CochainComplex C ℤ}
{Y : CochainComplex C ℤ}
(f : X ⟶ Y)
:
CochainComplex.mappingCone.triangleh f ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
instance
HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, 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]
:
(G.mapHomotopyCategory (ComplexShape.up ℤ)).IsTriangulated
Equations
- ⋯ = ⋯