The pretriangulated structure on the homotopy category of complexes
In this file, we shall define the pretriangulated structure on the homotopy
category HomotopyCategory C (ComplexShape.up ℤ) of an additive category C (TODO).
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
@[simp]
theorem
CochainComplex.mappingCone.triangle_obj₃
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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_2, 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_mor₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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.triangle_obj₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
(CochainComplex.mappingCone.triangle φ).obj₁ = K
noncomputable def
CochainComplex.mappingCone.triangle
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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.inl_v_triangle_mor₃_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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).toPrefunctor.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 (-(CochainComplex.shiftFunctorObjXIso K 1 q p (_ : p = q + 1)).inv) h
@[simp]
theorem
CochainComplex.mappingCone.inl_v_triangle_mor₃_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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) = -(CochainComplex.shiftFunctorObjXIso K 1 q p (_ : p = q + 1)).inv
@[simp]
theorem
CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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).toPrefunctor.obj (CochainComplex.mappingCone.triangle φ).obj₁).X
p ⟶ Z)
:
@[simp]
theorem
CochainComplex.mappingCone.inr_f_triangle_mor₃_f
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_triangleδ_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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).toPrefunctor.obj (CochainComplex.mappingCone.triangle φ).obj₁ ⟶ Z)
:
@[simp]
theorem
CochainComplex.mappingCone.inr_triangleδ
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
@[inline, reducible]
noncomputable abbrev
CochainComplex.mappingCone.triangleh
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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 φ = (CategoryTheory.Functor.mapTriangle (HomotopyCategory.quotient C (ComplexShape.up ℤ))).toPrefunctor.obj (CochainComplex.mappingCone.triangle φ)
Instances For
noncomputable def
CochainComplex.mappingCone.homotopyToZeroOfId
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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_2, 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).toPrefunctor.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).toPrefunctor.map a) h)
theorem
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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 φ₂))
:
CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.mapOfHomotopy H)
(CochainComplex.mappingCone.triangle φ₂).mor₃ = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ₁).mor₃
((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).toPrefunctor.map a)
@[simp]
theorem
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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 ℤ)).toPrefunctor.map (CochainComplex.mappingCone.mapOfHomotopy H)
@[simp]
theorem
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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 ℤ)).toPrefunctor.map b
@[simp]
theorem
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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 ℤ)).toPrefunctor.map a
noncomputable def
CochainComplex.mappingCone.trianglehMapOfHomotopy
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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
noncomputable def
CochainComplex.mappingCone.map
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
CochainComplex.mappingCone.map φ φ (CategoryTheory.CategoryStruct.id K) (CategoryTheory.CategoryStruct.id L)
(_ :
CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id K) φ) = CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone φ)
theorem
CochainComplex.mappingCone.map_comp_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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')
(_ :
CategoryTheory.CategoryStruct.comp φ₁ (CategoryTheory.CategoryStruct.comp b b') = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp a a') φ₃))
h = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₁ φ₂ a b comm)
(CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₂ φ₃ a' b' comm') h)
theorem
CochainComplex.mappingCone.map_comp
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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 φ₁ (CategoryTheory.CategoryStruct.comp b b') = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp a a') φ₃) = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₁ φ₂ a b comm)
(CochainComplex.mappingCone.map φ₂ φ₃ a' b' comm')
@[simp]
theorem
CochainComplex.mappingCone.triangleMap_hom₃
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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_2, 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.triangleMap
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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 = CategoryTheory.Pretriangulated.TriangleMorphism.mk a b (CochainComplex.mappingCone.map φ₁ φ₂ a b comm)
Instances For
noncomputable def
CochainComplex.mappingCone.rotateHomotopyEquiv
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
HomotopyEquiv ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).toPrefunctor.obj K)
(CochainComplex.mappingCone (CochainComplex.mappingCone.inr φ))
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_2, 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₂_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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 ℤ)).toPrefunctor.obj
(CochainComplex.mappingCone (CochainComplex.mappingCone.inr φ)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).toPrefunctor.map (CochainComplex.mappingCone.triangle φ).mor₃)
(CategoryTheory.CategoryStruct.comp
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).toPrefunctor.map
(CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom)
h) = CategoryTheory.CategoryStruct.comp
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).toPrefunctor.map
(CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ)))
h
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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 ℤ)).toPrefunctor.map (CochainComplex.mappingCone.triangle φ).mor₃)
((HomotopyCategory.quotient C (ComplexShape.up ℤ)).toPrefunctor.map
(CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).toPrefunctor.map
(CochainComplex.mappingCone.inr (CochainComplex.mappingCone.inr φ))
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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).toPrefunctor.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).toPrefunctor.map φ) h
@[simp]
theorem
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
:
CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom
(CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.inr φ)).mor₃ = -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).toPrefunctor.map φ
noncomputable def
CochainComplex.mappingCone.rotateTrianglehIso
{C : Type u_1}
[CategoryTheory.Category.{u_2, 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_2, 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).toPrefunctor.obj
(CochainComplex.mappingCone φ) ≅ CochainComplex.mappingCone ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).toPrefunctor.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_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(n : ℤ)
:
(CategoryTheory.Pretriangulated.Triangle.shiftFunctor (CochainComplex C ℤ) n).toPrefunctor.obj
(CochainComplex.mappingCone.triangle φ) ≅ CochainComplex.mappingCone.triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).toPrefunctor.map φ)
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_2, u_1} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasBinaryBiproducts C]
{K : CochainComplex C ℤ}
{L : CochainComplex C ℤ}
(φ : K ⟶ L)
(n : ℤ)
:
(CategoryTheory.Pretriangulated.Triangle.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).toPrefunctor.obj
(CochainComplex.mappingCone.triangleh φ) ≅ CochainComplex.mappingCone.triangleh ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).toPrefunctor.map φ)
The canonical isomorphism (triangleh φ)⟦n⟧ ≅ triangleh (φ⟦n⟧').
Equations
- One or more equations did not get rendered due to their size.