English
The inverse primed naturality statement holds: the inverse of the primed homology iso composed with F.map on the primed map equals the primed map after applying F.
Русский
Обратная натуральность для примарной мапы гомологии: обратное изоморфирования гомологии, сотыщенное с F.map, эквивалентно применению примарной мапы после F.
LaTeX
$$$F.map(\mathrm{homologyMap}'(\phi)) \;\circ\; (S_2.mapHomologyIso'\,F)^{-1} \\= (S_1.mapHomologyIso'\,F)^{-1} \circ \mathrm{homologyMap}'(F.mapShortComplex.map\,\phi)$$$
Lean4
@[reassoc]
theorem mapHomologyIso'_inv_naturality [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology]
[(S₂.map F).HasHomology] [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
F.map (homologyMap φ) ≫ (S₂.mapHomologyIso' F).inv =
(S₁.mapHomologyIso' F).inv ≫ @homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _ :=
by
rw [← cancel_epi (S₁.mapHomologyIso' F).hom, ← mapHomologyIso'_hom_naturality_assoc, Iso.hom_inv_id, comp_id,
Iso.hom_inv_id_assoc]
