English
Under a functor G, the image of the δ-differential of the mapping cone commutes with the corresponding natural isomorphisms: (G.mapHomologicalComplex (up ℤ)).map (triangle φ).mor₃ ≫ NatTrans.app ((Functor.mapHomologicalComplex G (up ℤ)).commShiftIso 1).hom K = (mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (up ℤ)).map φ)).mor₃.
Русский
При отображении через функционор G дифференциал δ в mapping cone вместе с соответствующими натурными изоморфизмами образуется commuting diagram: (G.mapHomologicalComplex (up ℤ)).map (triangle φ).mor₃ ≫ NatTrans.app ((Functor.mapHomologicalComplex G (up ℤ)).commShiftIso 1).hom K = (mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (up ℤ)).map φ)).mor₃.
LaTeX
$$$ (G.mapHomologicalComplex (ComplexShape.up\\,\\mathbb{Z})).map (\\mathrm{triangle} \\phi).mor_3 \\\\gg \\\\mathrm{app}((\\mathrm{Functor.mapHomologicalComplex} G (ComplexShape.up \\mathbb{Z})).commShiftIso 1).hom_K = (\\mathrm{mapHomologicalComplexIso} \\phi G).hom \\\\gg (\\mathrm{triangle} ((G.mapHomologicalComplex (ComplexShape.up \\mathbb{Z})).map φ)).mor_3 $$$
Lean4
theorem map_δ :
(G.mapHomologicalComplex (ComplexShape.up ℤ)).map (triangle φ).mor₃ ≫
NatTrans.app ((Functor.mapHomologicalComplex G (ComplexShape.up ℤ)).commShiftIso 1).hom K =
(mapHomologicalComplexIso φ G).hom ≫ (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃ :=
by
ext n
dsimp [mapHomologicalComplexIso]
rw [mapHomologicalComplexXIso_eq φ G n (n + 1) rfl, mapHomologicalComplexXIso'_hom]
simp only [Functor.mapHomologicalComplex_obj_X, add_comp, assoc, inl_v_triangle_mor₃_f, shiftFunctor_obj_X,
shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, comp_neg, comp_id, inr_f_triangle_mor₃_f,
comp_zero, add_zero]
dsimp [triangle]
rw [Cochain.rightShift_v _ 1 0 (by cutsat) n n (by cutsat) (n + 1) (by cutsat)]
simp only [shiftFunctor_obj_X, Cochain.neg_v, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv,
comp_id, Functor.map_neg]
