English
The inverse of the restriction–homology iso intertwines with the homologyι maps via the inverse of the restriction–opcycles iso, establishing a natural compatibility between the restricted and original homologyι maps.
Русский
Обратный элемент к изоморфизму ограничения гомологий взаимодействует с отображениями гомологий-ι через обратное ограничение–opcycles изоморфизм, устанавливая естественную совместимость между ограниченными и исходными отображениями гомологий-ι.
LaTeX
$$$ (K_{|e}\\mathrm{RestrictionHomologyIso}\\,e\\,i\\,j\\,k\\,hi\\,hk\\,hi'\\,hj'\\,hk'\\,hi''\\,hk'')^{-1} \\;\\circ\\; (K_{|e}\\mathrm{restriction})\\mathrm{homology\\iota}\\,j \\\\ =\\\\ K_{\\mathrm{homology}\\iota}\\,j' \\,\\circ\\; (K_{|e}\\mathrm{restrictionOpcyclesIso}\\,e\\,i\\,j\\,hi\\,hi'\\,hj'\\,hi'').inv$$
Lean4
@[reassoc (attr := simp, nolint unusedHavesSuffices)]
theorem restrictionHomologyIso_inv_homologyι :
(K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv ≫ (K.restriction e).homologyι j =
K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv :=
by
have : ((K.restriction e).sc' i j k).HasHomology := by subst hi hk; assumption
have : (K.sc' i' j' k').HasHomology := by subst hi'' hk''; assumption
dsimp [restrictionHomologyIso, homologyIsoSc']
rw [← ShortComplex.homologyMap_comp, ← ShortComplex.homologyMap_comp, assoc, ← cancel_epi (K.sc j').homologyπ]
apply (ShortComplex.π_homologyMap_ι _).trans
dsimp
rw [comp_id, id_comp]
refine ((ShortComplex.homology_π_ι_assoc _ _).trans ?_).symm
congr 1
apply pOpcycles_restrictionOpcyclesIso_inv
