English
There is a natural isomorphism in each degree between the image by H of the X-component of the mapping cone φ and the X-component of the mapping cone of the mapped φ.
Русский
В каждой степени существует естественное изоморфизм между X-компонентой отображающего конуса φ после применения к нему контура H и X-компонентой конуса образованного φ после применения H.
LaTeX
$$$\\forall n:\\mathbb{Z},\\ ((H.mapHomologicalComplex(\\mathrm{up}\\,\\mathbb{Z}).obj(\\mathrm{mappingCone}\\,φ)).X_n) \\cong (\\mathrm{mappingCone}((H.mapHomologicalComplex(\\mathrm{up}\\,\\mathbb{Z}).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 `n`) between the image
by `H` of `mappingCone φ` and the mapping cone of the image by `H` of `φ`.
It is an auxiliary definition for `mapHomologicalComplexXIso` and
`mapHomologicalComplexIso`. This definition takes an extra
parameter `m : ℤ` such that `n + 1 = m` which may help getting better
definitional properties. See also the equational lemma `mapHomologicalComplexXIso_eq`. -/
@[simps]
noncomputable def mapHomologicalComplexXIso' (n m : ℤ) (hnm : n + 1 = m) :
((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).X n ≅
(mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).X n
where
hom :=
H.map ((fst φ).1.v n m (by omega)) ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n (by omega) +
H.map ((snd φ).v n n (add_zero n)) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n
inv :=
(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).1.v n m (by omega) ≫ H.map ((inl φ).v m n (by omega)) +
(snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n (add_zero n) ≫ H.map ((inr φ).f n)
hom_inv_id :=
by
simp only [Functor.mapHomologicalComplex_obj_X, comp_add, add_comp, assoc, inl_v_fst_v_assoc, inr_f_fst_v_assoc,
zero_comp, comp_zero, add_zero, inl_v_snd_v_assoc, inr_f_snd_v_assoc, zero_add, ← Functor.map_comp,
← Functor.map_add]
rw [← H.map_id]
congr 1
simp [ext_from_iff _ _ _ hnm]
inv_hom_id :=
by
simp only [Functor.mapHomologicalComplex_obj_X, comp_add, add_comp, assoc, ← H.map_comp_assoc, inl_v_fst_v,
CategoryTheory.Functor.map_id, id_comp, inr_f_fst_v, inl_v_snd_v, inr_f_snd_v]
simp [ext_from_iff _ _ _ hnm]
