English
The inverse of the restriction–homology isomorphism interacts with the homology projection and the cycles isomorphism, giving a natural inverse compatibility between the restricted and original homology objects.
Русский
Обратный к изоморфизму ограничения по гомологиям совместим с отображением проекции гомологий и с изоморфизмом циклов; то есть^{-1} обеспечивает естественную совместимость между ограниченными и исходными гомологическими объектами.
LaTeX
$$$ (K_{|e}\\mathrm{HomologyIso}\\,e\\,i\\,j\\,k\\,hi\\,hk\\,hi'\\,hj'\\,hk'\\,hi''\\,hk'')^.inv \\;\\circ\\; K_{|e}\\mathrm{homology\\pi}\\,j \;=\; (K_{|e}\\mathrm{RestrictionCyclesIso}\\,e\\,j\\,k\\,hk\\,hj'\\,hk'\\,hk'').inv \\;\\circ\\; K_{\\mathrm{restriction}}\\mathrm{homology\\pi}\\,j$$
Lean4
@[reassoc]
theorem homologyπ_restrictionHomologyIso_inv :
K.homologyπ j' ≫ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv =
(K.restrictionCyclesIso e j k hk hj' hk' hk'').inv ≫ (K.restriction e).homologyπ j :=
by
rw [← cancel_mono (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom, assoc, assoc, Iso.inv_hom_id,
homologyπ_restrictionHomologyIso_hom, comp_id, Iso.inv_hom_id_assoc]
