English
Definition of a degreewise isomorphism between the image of mappingCone φ under H and the mappingCone of the mapped φ.
Русский
Определение изоморфизма по степеням между образом отображающего конуса φ под H и отображающим конусом образованного φ.
LaTeX
$$$\\text{mapHomologicalComplexXIso' }(n,m,h) : ((H.mapHomologicalComplex(ComplexShape.up\\,ℤ)).obj(\\mathrm{mappingCone}\\,φ)).X_n \\cong (\\mathrm{mappingCone}((H.mapHomologicalComplex(ComplexShape.up\\,ℤ)).map\\,φ)).X_n$$$
Lean4
/-- If `H : C ⥤ D` is an additive functor and `φ` is a morphism of cochain complexes
in `C`, this is the comparison isomorphism (in each degree) between the image
by `H` of `mappingCone φ` and the mapping cone of the image by `H` of `φ`. -/
noncomputable def mapHomologicalComplexXIso (n : ℤ) :
((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).X n ≅
(mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).X n :=
mapHomologicalComplexXIso' φ H n (n + 1) rfl
