English
The map sending the inr φ component through H matches the inr φ map of the mapped morphism, up to the functorial isomorphisms.
Русский
Отображение компоненты inr φ через H совпадает с inr φ отображенного морфизма через изоморфизм Функторов.
LaTeX
$$$(H.mapHomologicalComplex(ComplexShape.up\\,\\mathbb{Z})).map(inr\\,φ) \\, = \\, inr\\,(H.mapHomologicalComplex(ComplexShape.up\\,\\mathbb{Z}).map\\,φ)$$$
Lean4
theorem map_inr :
(H.mapHomologicalComplex (ComplexShape.up ℤ)).map (inr φ) ≫ (mapHomologicalComplexIso φ H).hom =
inr ((Functor.mapHomologicalComplex H (ComplexShape.up ℤ)).map φ) :=
by
ext n
dsimp [mapHomologicalComplexIso]
simp only [mapHomologicalComplexXIso_eq φ H n (n + 1) rfl, mappingCone.ext_to_iff _ _ _ rfl,
Functor.mapHomologicalComplex_obj_X, mapHomologicalComplexXIso'_hom, comp_add, add_comp, assoc, inl_v_fst_v,
comp_id, inr_f_fst_v, comp_zero, add_zero, inl_v_snd_v, inr_f_snd_v, zero_add, ← H.map_comp, H.map_zero, H.map_id,
and_self]
