The mapping cone of a monomorphism, up to a quasi-isomophism

If S is a short exact short complex of cochain complexes in an abelian category, we construct a quasi-isomorphism descShortComplex S : mappingCone S.f ⟶ S.X₃.

We obtain this by comparing the homology sequence of S and the homology sequence of the homology functor on the homotopy category, applied to the distinguished triangle attached to the mapping cone of S.f.

theorem CochainComplex.homologySequenceδ_quotient_mapTriangle_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj T) n₀ n₁ h = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app T.obj₃) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯) ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app T.obj₁))

theorem CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {Z : C} (h✝ : ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).shift n₁).obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj T).obj₁ ⟶ Z) : CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj T) n₀ n₁ h) h✝ = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app T.obj₃) (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯) (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app T.obj₁) h✝))

noncomputable def CochainComplex.mappingCone.descShortComplex {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) : CochainComplex.mappingCone S.f ⟶ S.X₃

The canonical morphism mappingCone S.f ⟶ S.X₃ when S is a short complex of cochain complexes.

Equations

• CochainComplex.mappingCone.descShortComplex S = CochainComplex.mappingCone.desc S.f 0 S.g ⋯

@[simp]

theorem CochainComplex.mappingCone.inr_descShortComplex {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr S.f) (CochainComplex.mappingCone.descShortComplex S) = S.g

@[simp]

theorem CochainComplex.mappingCone.inr_descShortComplex_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) {Z : CochainComplex C ℤ} (h : S.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr S.f) (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.descShortComplex S) h) = CategoryTheory.CategoryStruct.comp S.g h

@[simp]

theorem CochainComplex.mappingCone.inr_f_descShortComplex_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (n : ℤ) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr S.f).f n) ((CochainComplex.mappingCone.descShortComplex S).f n) = S.g.f n

@[simp]

theorem CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (n : ℤ) {Z : C} (h : S.X₃.X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr S.f).f n) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.descShortComplex S).f n) h) = CategoryTheory.CategoryStruct.comp (S.g.f n) h

@[simp]

theorem CochainComplex.mappingCone.inl_v_descShortComplex_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (i j : ℤ) (h : i + -1 = j) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl S.f).v i j h) ((CochainComplex.mappingCone.descShortComplex S).f j) = 0

@[simp]

theorem CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (i j : ℤ) (h : i + -1 = j) {Z : C} (h✝ : S.X₃.X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl S.f).v i j h) (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.descShortComplex S).f j) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem CochainComplex.mappingCone.homologySequenceδ_triangleh {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) : (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) 0).homologySequenceδ (CochainComplex.mappingCone.triangleh S.f) n₀ n₁ h = CategoryTheory.CategoryStruct.comp ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₀).hom.app (CochainComplex.mappingCone S.f)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (CochainComplex.mappingCone.descShortComplex S) n₀) (CategoryTheory.CategoryStruct.comp (hS.δ n₀ n₁ h) ((HomotopyCategory.homologyFunctorFactors C (ComplexShape.up ℤ) n₁).inv.app S.X₁)))

theorem CochainComplex.mappingCone.quasiIso_descShortComplex {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact) : QuasiIso (CochainComplex.mappingCone.descShortComplex S)