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 (with the better sign conventions from the introduction of Brian Conrad's book Grothendieck duality and base change).
References #
noncomputable def
CochainComplex.mappingCone.triangle
{C : Type u_1}
[CategoryTheory.Category.{u_3, 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 φ.
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 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 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 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 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 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 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 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 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 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 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 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 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₁ 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.
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₁ 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 φ₂))
:
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₁ 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 : 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₁ 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 φ₂))
:
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₁ 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 : 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₁ 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.
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₁ 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 φ₂))
:
(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₁ 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 φ₂))
:
(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₁ 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 φ₂))
:
noncomputable def
CochainComplex.mappingCone.map
{C : Type u_1}
[CategoryTheory.Category.{u_3, 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.
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₁ L₁ K₂ 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 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₁ 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' φ₃)
:
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₁ 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 : 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₁ 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.
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₁ L₁ K₂ 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₁ L₁ K₂ 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₁ L₁ K₂ 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 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 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 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 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 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 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 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 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 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 L : CochainComplex C ℤ}
(φ : K ⟶ L)
(n : ℤ)
:
The canonical isomorphism (triangleh φ)⟦n⟧ ≅ triangleh (φ⟦n⟧').
Equations
- One or more equations did not get rendered due to their size.
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 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 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 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 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₁ 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 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