English
If φ: K → L is a morphism of cochain complexes and G: C → D is an additive functor, then the image by G of the triangle φ identifies with the triangle of the image of φ: (G.mapHomologicalComplex (up ℤ)).mapTriangle.obj (triangle φ) ≅ triangle ((G.mapHomologicalComplex (up ℤ)).map φ).
Русский
Если φ: K → L — морфизм коchain комплексoв и G: C → D — аддитивный функтор, то образ φ под G соответствует треугольнику образа φ: (G.mapHomologicalComplex (up ℤ)).mapTriangle.obj (triangle φ) ≅ triangle ((G.mapHomologicalComplex (up ℤ)).map φ).
LaTeX
$$$ (G.mapHomologicalComplex (ComplexShape.up \\mathbb{Z})).mapTriangle.obj (triangle \\phi) \\cong triangle ((G.mapHomologicalComplex (ComplexShape.up \\mathbb{Z})).map \\phi) $$$
Lean4
/-- 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`. -/
noncomputable def mapTrianglehIso :
(G.mapHomotopyCategory (ComplexShape.up ℤ)).mapTriangle.obj (triangleh φ) ≅
triangleh ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ) :=
(Functor.mapTriangleCompIso _ _).symm.app _ ≪≫
(Functor.mapTriangleIso (G.mapHomotopyCategoryFactors (ComplexShape.up ℤ))).app _ ≪≫
(Functor.mapTriangleCompIso _ _).app _ ≪≫
(HomotopyCategory.quotient D (ComplexShape.up ℤ)).mapTriangle.mapIso
(CochainComplex.mappingCone.mapTriangleIso φ G)
