The triangulated structure on the homotopy category of complexes

In this file, we show that for any additive category C, the pretriangulated category HomotopyCategory C (ComplexShape.up ℤ) is triangulated.

noncomputable def CochainComplex.mappingConeCompTriangle {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)

Given two composable morphisms f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ in the category of cochain complexes, this is the canonical triangle mappingCone f ⟶ mappingCone (f ≫ g) ⟶ mappingCone g ⟶ (mappingCone f)⟦1⟧.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CochainComplex.mappingConeCompTriangle_mor₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : (CochainComplex.mappingConeCompTriangle f g).mor₁ = CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁) g ⋯

@[simp]

theorem CochainComplex.mappingConeCompTriangle_obj₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : (CochainComplex.mappingConeCompTriangle f g).obj₃ = CochainComplex.mappingCone g

@[simp]

theorem CochainComplex.mappingConeCompTriangle_obj₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : (CochainComplex.mappingConeCompTriangle f g).obj₂ = CochainComplex.mappingCone (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem CochainComplex.mappingConeCompTriangle_mor₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : (CochainComplex.mappingConeCompTriangle f g).mor₃ = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle g).mor₃ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.inr f))

@[simp]

theorem CochainComplex.mappingConeCompTriangle_mor₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : (CochainComplex.mappingConeCompTriangle f g).mor₂ = CochainComplex.mappingCone.map (CategoryTheory.CategoryStruct.comp f g) g f (CategoryTheory.CategoryStruct.id X₃) ⋯

@[simp]

theorem CochainComplex.mappingConeCompTriangle_obj₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : (CochainComplex.mappingConeCompTriangle f g).obj₁ = CochainComplex.mappingCone f

noncomputable def CochainComplex.mappingConeCompTriangleh {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))

Given two composable morphisms f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ in the category of cochain complexes, this is the canonical triangle mappingCone f ⟶ mappingCone (f ≫ g) ⟶ mappingCone g ⟶ (mappingCone f)⟦1⟧ in the homotopy category. It is a distinguished triangle, see HomotopyCategory.mappingConeCompTriangleh_distinguished.

Equations

• CochainComplex.mappingConeCompTriangleh f g = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj (CochainComplex.mappingConeCompTriangle f g)

theorem CochainComplex.mappingConeCompTriangle_mor₃_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Y₁ : CochainComplex C ℤ} {Y₂ : CochainComplex C ℤ} {Y₃ : CochainComplex C ℤ} (f' : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) (φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map g g' (φ.app 1) (φ.app 2) ⋯) (CochainComplex.mappingConeCompTriangle f' g').mor₃ = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₃ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.map f f' (φ.app 0) (φ.app 1) ⋯))

theorem CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Y₁ : CochainComplex C ℤ} {Y₂ : CochainComplex C ℤ} {Y₃ : CochainComplex C ℤ} (f' : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) (φ : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingConeCompTriangle f' g').obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map g g' (φ.app 1) (φ.app 2) ⋯) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f' g').mor₃ h) = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₃ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (CochainComplex.mappingCone.map f f' (φ.app 0) (φ.app 1) ⋯)) h)

noncomputable def CochainComplex.MappingConeCompHomotopyEquiv.hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CochainComplex.mappingCone g ⟶ CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁

Given two composable morphisms f and g in the category of cochain complexes, this is the canonical morphism (which is an homotopy equivalence) from mappingCone g to the mapping cone of the morphism mappingCone f ⟶ mappingCone (f ≫ g).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CochainComplex.MappingConeCompHomotopyEquiv.inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁ ⟶ CochainComplex.mappingCone g

Given two composable morphisms f and g in the category of cochain complexes, this is the canonical morphism (which is an homotopy equivalence) from the mapping cone of the morphism mappingCone f ⟶ mappingCone (f ≫ g) to mappingCone g.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CategoryTheory.CategoryStruct.comp (CochainComplex.MappingConeCompHomotopyEquiv.hom f g) (CochainComplex.MappingConeCompHomotopyEquiv.inv f g) = CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone g)

@[simp]

theorem CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : CochainComplex.mappingCone g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.MappingConeCompHomotopyEquiv.hom f g) (CategoryTheory.CategoryStruct.comp (CochainComplex.MappingConeCompHomotopyEquiv.inv f g) h) = h

noncomputable def CochainComplex.MappingConeCompHomotopyEquiv.homotopyInvHomId {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : Homotopy (CategoryTheory.CategoryStruct.comp (CochainComplex.MappingConeCompHomotopyEquiv.inv f g) (CochainComplex.MappingConeCompHomotopyEquiv.hom f g)) (CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁))

Given two composable morphisms f and g in the category of cochain complexes, this is the homotopyInvHomId field of the homotopy equivalence mappingConeCompHomotopyEquiv f g between mappingCone g and the mapping cone of the morphism mappingCone f ⟶ mappingCone (f ≫ g).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CochainComplex.mappingConeCompHomotopyEquiv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : HomotopyEquiv (CochainComplex.mappingCone g) (CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁)

Given two composable morphisms f and g in the category of cochain complexes, this is the homotopy equivalence mappingConeCompHomotopyEquiv f g between mappingCone g and the mapping cone of the morphism mappingCone f ⟶ mappingCone (f ≫ g).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).hom (CochainComplex.mappingConeCompHomotopyEquiv f g).inv = CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone g)

@[simp]

theorem CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : CochainComplex.mappingCone g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).hom (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).inv h) = h

theorem CochainComplex.mappingConeCompHomotopyEquiv_comm₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁) g ⋯)) (CochainComplex.mappingConeCompHomotopyEquiv f g).inv = (CochainComplex.mappingConeCompTriangle f g).mor₂

theorem CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Z : CochainComplex C ℤ} (h : CochainComplex.mappingCone g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr (CochainComplex.mappingCone.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X₁) g ⋯)) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).inv h) = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₂ h

theorem CochainComplex.mappingConeCompHomotopyEquiv_comm₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).hom (CochainComplex.mappingCone.triangle (CochainComplex.mappingConeCompTriangle f g).mor₁).mor₃ = (CochainComplex.mappingConeCompTriangle f g).mor₃

theorem CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Z : HomologicalComplex C (ComplexShape.up ℤ)} (h : (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle (CochainComplex.mappingConeCompTriangle f g).mor₁).obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).hom (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle (CochainComplex.mappingConeCompTriangle f g).mor₁).mor₃ h) = CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₃ h

@[simp]

theorem CochainComplex.mappingConeCompTriangleh_comm₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangleh f g).mor₂ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingConeCompHomotopyEquiv f g).hom) = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr (CochainComplex.mappingConeCompTriangle f g).mor₁)

@[simp]

theorem CochainComplex.mappingConeCompTriangleh_comm₁_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Z : HomotopyCategory C (ComplexShape.up ℤ)} (h : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangleh f g).mor₂ (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingConeCompHomotopyEquiv f g).hom) h) = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.inr (CochainComplex.mappingConeCompTriangle f g).mor₁)) h

theorem HomotopyCategory.mappingConeCompTriangleh_distinguished {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ : CochainComplex C ℤ} {X₂ : CochainComplex C ℤ} {X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) [CategoryTheory.Limits.HasZeroObject C] : CochainComplex.mappingConeCompTriangleh f g ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

noncomputable instance HomotopyCategory.instIsTriangulatedIntUp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.IsTriangulated (HomotopyCategory C (ComplexShape.up ℤ))

Equations

• ⋯ = ⋯