Naturality of the mapping cone triangles of composable morphisms in the homotopy category

For composable morphisms f : X₁ ⟶ X₂ and g : X₂ ⟶ X₃ of cochain complexes, Mathlib's CochainComplex.mappingConeCompTriangleh f g is the distinguished triangle mappingCone f ⟶ mappingCone (f ≫ g) ⟶ mappingCone g ⟶ (mappingCone f)⟦1⟧ in the homotopy category, the image of CochainComplex.mappingConeCompTriangle f g under the quotient functor. Mathlib's CochainComplex.mappingConeCompTriangle_mor₃_naturality states the naturality of the third morphism of mappingConeCompTriangle f g at the level of cochain complexes; this file records the corresponding naturality of the third morphism of mappingConeCompTriangleh f g.

Main results

• CochainComplex.mappingConeCompTriangleh_mor₃_naturality: naturality in (f, g) of the third morphism of mappingConeCompTriangleh f g.

theorem CochainComplex.mappingConeCompTriangleh_mor₃_naturality {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (f' : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) (a : X₁ ⟶ Y₁) (b : X₂ ⟶ Y₂) (c : X₃ ⟶ Y₃) (h₁ : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') (h₂ : CategoryTheory.CategoryStruct.comp g c = CategoryTheory.CategoryStruct.comp b g') : CategoryTheory.CategoryStruct.comp (mappingConeCompTriangleh f g).mor₃ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingCone.map f f' a b h₁)⟦1⟧') = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingCone.map g g' b c h₂)) (mappingConeCompTriangleh f' g').mor₃

The third morphisms of the distinguished triangles mappingConeCompTriangleh f g of mapping cones in the homotopy category are natural in the pair of composable morphisms (f, g).

theorem CochainComplex.mappingConeCompTriangleh_mor₃_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃) (f' : Y₁ ⟶ Y₂) (g' : Y₂ ⟶ Y₃) (a : X₁ ⟶ Y₁) (b : X₂ ⟶ Y₂) (c : X₃ ⟶ Y₃) (h₁ : CategoryTheory.CategoryStruct.comp f b = CategoryTheory.CategoryStruct.comp a f') (h₂ : CategoryTheory.CategoryStruct.comp g c = CategoryTheory.CategoryStruct.comp b g') {Z : HomotopyCategory C (ComplexShape.up ℤ)} (h : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj (mappingCone f')⟦1⟧ ⟶ Z) : CategoryTheory.CategoryStruct.comp (mappingConeCompTriangleh f g).mor₃ (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingCone.map f f' a b h₁)⟦1⟧') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingCone.map g g' b c h₂)) (mappingConeCompTriangleh f' g').mor₃) h

The third morphisms of the distinguished triangles mappingConeCompTriangleh f g of mapping cones in the homotopy category are natural in the pair of composable morphisms (f, g).