English
The forward direction of the naturality: the homomorphism part of the restriction–homology iso composed with the homologyι j' equals the homologyι j composed with the inverse of the restriction–opcycles iso.
Русский
Прямая часть натуральности: отображение гомологии через изоморфизм ограничения, затем homologyι(j'), равно отображению гомологии через homologyι(j) после обратного изоморфизма restriction–opcycles.
LaTeX
$$$ (K_{|e}\\mathrm{RestrictionHomologyIso}\\,e\\,i\\,j\\,k\\,hi\\,hk\\,hi'\\,hj'\\,hk'\\,hi''\\,hk'').hom \\; \\circ \\; K_{\\mathrm{homology\\iota}}\\,j' \\\\ =\\\\ K_{|e}\\mathrm{homology\\iota}\\,j \\;\\circ \\; (K_{|e}\\mathrm{restrictionOpcyclesIso}\\,e\\,i\\,j\\,hi\\,hi'\\,hj'\\,hi'').inv$$
Lean4
@[reassoc (attr := simp)]
theorem restrictionHomologyIso_hom_homologyι :
(K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom ≫ K.homologyι j' =
(K.restriction e).homologyι j ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom :=
by
rw [← cancel_epi (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv, Iso.inv_hom_id_assoc,
restrictionHomologyIso_inv_homologyι_assoc, Iso.inv_hom_id, comp_id]
