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.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ 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⟧.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CochainComplex.mappingConeCompTriangleh {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ 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.

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

theorem CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) {Y₁ Y₂ 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 (mappingConeCompTriangle f' g').obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp (mappingCone.map g g' (φ.app 1) (φ.app 2) ⋯) (CategoryTheory.CategoryStruct.comp (mappingConeCompTriangle f' g').mor₃ h) = CategoryTheory.CategoryStruct.comp (mappingConeCompTriangle f g).mor₃ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.map f f' (φ.app 0) (φ.app 1) ⋯)) h)

noncomputable def CochainComplex.MappingConeCompHomotopyEquiv.hom {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : mappingCone g ⟶ mappingCone (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).

noncomputable def CochainComplex.MappingConeCompHomotopyEquiv.inv {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : mappingCone (mappingConeCompTriangle f g).mor₁ ⟶ 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.

@[simp]

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

@[simp]

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

noncomputable def CochainComplex.MappingConeCompHomotopyEquiv.homotopyInvHomId {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : Homotopy (CategoryTheory.CategoryStruct.comp (inv f g) (hom f g)) (CategoryTheory.CategoryStruct.id (mappingCone (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).

noncomputable def CochainComplex.mappingConeCompHomotopyEquiv {C : Type u_1} [CategoryTheory.Category.{v, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) : HomotopyEquiv (mappingCone g) (mappingCone (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).

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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