English
There is a natural isomorphism between the image by H of the mappingCone φ and the mappingCone of the image of φ, built from the componentwise isomorphisms.
Русский
Существует естественный изоморфизм между образом отображающего конуса φ под H и отображающим конусом образованного φ, скрепленный компонентами-изоморфизмами.
LaTeX
$$$(H.mapHomologicalComplex\\_ (ComplexShape.up\\,\\mathbb{Z})).obj(\\mathrm{mappingCone}\\,φ) \\cong \\mathrm{mappingCone}((H.mapHomologicalComplex(ComplexShape.up\\,\\mathbb{Z})).map\\,φ)$$$
Lean4
/-- If `H : C ⥤ D` is an additive functor and `φ` is a morphism of cochain complexes
in `C`, this is the comparison isomorphism between the image by `H`
of `mappingCone φ` and the mapping cone of the image by `H` of `φ`. -/
noncomputable def mapHomologicalComplexIso :
(H.mapHomologicalComplex _).obj (mappingCone φ) ≅ mappingCone ((H.mapHomologicalComplex _).map φ) :=
HomologicalComplex.Hom.isoOfComponents (mapHomologicalComplexXIso φ H)
(by
rintro n _ rfl
rw [ext_to_iff _ _ (n + 2) (by cutsat), assoc, assoc, d_fst_v _ _ _ _ rfl, assoc, assoc, d_snd_v _ _ _ rfl]
simp only [mapHomologicalComplexXIso_eq φ H n (n + 1) rfl,
mapHomologicalComplexXIso_eq φ H (n + 1) (n + 2) (by cutsat), mapHomologicalComplexXIso'_hom,
mapHomologicalComplexXIso'_hom]
constructor
· dsimp
simp only [Functor.mapHomologicalComplex_obj_X, comp_neg, add_comp, assoc, inl_v_fst_v_assoc, inr_f_fst_v_assoc,
zero_comp, comp_zero, add_zero, inl_v_fst_v, comp_id, inr_f_fst_v, ← H.map_comp,
d_fst_v φ n (n + 1) (n + 2) rfl (by cutsat), Functor.map_neg]
· dsimp
simp only [comp_add, add_comp, assoc, inl_v_fst_v_assoc, inr_f_fst_v_assoc, Functor.mapHomologicalComplex_obj_X,
zero_comp, comp_zero, add_zero, inl_v_snd_v_assoc, inr_f_snd_v_assoc, zero_add, inl_v_snd_v, inr_f_snd_v,
comp_id, ← H.map_comp, d_snd_v φ n (n + 1) rfl, Functor.map_add])
