English
Let S1, S2 be short complexes in a category C with right homology data, and F a functor preserving zero morphisms. For any morphism φ: S1 → S2, the naturality of the right homology map asserts that applying F to the right homology map of φ commutes with the isomorphism induced by F on S1 and S2.
Русский
Пусть S1, S2 — короткие комплексы в категории C с правыми данными однородности, и F — онтофунктор, сохраняющий нулевые морфизмы. Для любого отображения φ: S1 → S2 натуральность правой гомологии утверждает, что применение F к правовой гомологии отображения φ компонуется одинаково с соответствующим изоморфизмом, индуктивируемым F на S1 и S2.
LaTeX
$$$\mathrm{rightHomologyMap}(F\,\mathrm{mapShortComplex}.map\,\phi) \;\circ\; (S_2.mapRightHomologyIso\,F)_{\mathrm{hom}} \\= \\ (S_1.mapRightHomologyIso\,F)_{\mathrm{hom}} \circ F(\mathrm{rightHomologyMap}(\phi))$$
Lean4
@[reassoc]
theorem mapRightHomologyIso_hom_naturality [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂] :
rightHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapRightHomologyIso F).hom =
(S₁.mapRightHomologyIso F).hom ≫ F.map (rightHomologyMap φ) :=
by
dsimp only [rightHomologyMap, mapRightHomologyIso, RightHomologyData.rightHomologyIso, rightHomologyMapIso', Iso.refl]
simp only [RightHomologyData.map_rightHomologyMap', Functor.mapShortComplex_obj, ← rightHomologyMap'_comp, comp_id,
id_comp]
