English
Under the same hypotheses as the previous item, the inverse of the right homology isomorphism behaves naturally with respect to φ: applying F to the rightHomologyMap and then inverting the isomorphism equals inverting the isomorphism first and then applying the map φ inside F.
Русский
При тех же предположениях, что и в предыдущем пункте, обратный изоморфизм правой гомологии ведет себя натурально по отношению к φ: применение F к rightHomologyMap и взятие обратного изоморфизма эквивалентно взятию обратного изоморфизма прежде и затем применению отображения φ внутри F.
LaTeX
$$$F\,\mathrm{map}(\mathrm{rightHomologyMap}(\phi)) \;\circ\; (S_2.mapRightHomologyIso\,F)^{-1} \\= (S_1.mapRightHomologyIso\,F)^{-1} \circ \mathrm{rightHomologyMap}(F\,\mathrm{mapShortComplex}.map\,\phi)$$$
Lean4
@[reassoc]
theorem mapRightHomologyIso_inv_naturality [S₁.HasRightHomology] [S₂.HasRightHomology] [F.PreservesRightHomologyOf S₁]
[F.PreservesRightHomologyOf S₂] :
F.map (rightHomologyMap φ) ≫ (S₂.mapRightHomologyIso F).inv =
(S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ) :=
by
rw [← cancel_epi (S₁.mapRightHomologyIso F).hom, ← mapRightHomologyIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id,
Iso.hom_inv_id_assoc]
