English
Let K be a homological complex over a category with a fixed embedding e: c → c'. Then the natural square formed by the restriction on homology π_j, the restriction–homology isomorphism, and the restriction–cycles isomorphism commutes; i.e., composing π_j then the restriction isomorphism equals composing the cycles isomorphism then π_j'.
Русский
Пусть K — гомологический комплекс над категорией с фиксированным вложением e: c → c'. Тогда естественный квадрат, состоят из отображения ограничений на гомологию π_j, изоморфизма ограничение–гомология и изоморфизма ограничение–цикл, коммутирует; то есть композиция π_j затем ограничение совпадает с композицией по циклам затем π_j'.
LaTeX
$$$ (K_{|e})\\mathrm{homology\\pi}\\!\\big(j\\big) \\;\\circ\\; (K_{|e}\\mathrm{HomologyIso}\\,e\\,i\\,j\\,k\\,hi\\,hk\\,hi'\\,hj'\\,hk'\\,hi''\\,hk'')^.hom \;=\; (K_{|e}\\mathrm{CyclesIso}\\,e\\,j\\,k\\,hk\\,hj'\\,hk'\\,hk'').hom \\;\\circ\\; K_{\\mathrm{homology}\\pi}\\!\\big(j'\\big) $$$
Lean4
@[reassoc (attr := simp, nolint unusedHavesSuffices)]
theorem homologyπ_restrictionHomologyIso_hom :
(K.restriction e).homologyπ j ≫ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom =
(K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j' :=
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, ← cancel_mono (K.sc j').homologyι, assoc, assoc]
apply (ShortComplex.π_homologyMap_ι _).trans
dsimp
rw [comp_id, id_comp]
apply (K.restrictionCyclesIso_hom_iCycles_assoc e j k hk hj' hk' hk'' _).symm.trans
congr 1
symm
apply ShortComplex.homology_π_ι
