English
Let e be an embedding between complex shapes and K a homological complex with j-th homology. The isomorphism between the j-th left cycles of K after extending along e and the j'-th left cycles of the extended complex is compatible with the i-cycles map; precisely, (K.extendCyclesIso e hj').hom followed by K.iCycles j equals the i'-th left cycles map followed by (K.extendXIso e hj').hom.
Русский
Пусть e — вложение между комплексными формами, K — гомологический комплекс с j-й гомологией. Изоморфия между j-ой левой циклической группой K после расширения по e и j'-й левой циклической группой расширенного комплекса совместима с отображением i-циклов: (K.extendCyclesIso e hj').hom ∘ K.iCycles j = (K.extend e).iCycles j' ∘ (K.extendXIso e hj').hom.
LaTeX
$$$ (K.extendCyclesIso e hj').hom \circ K.iCycles j = (K.extend e).iCycles j' \circ (K.extendXIso e hj').hom $$$
Lean4
@[reassoc (attr := simp)]
theorem extendCyclesIso_hom_iCycles :
(K.extendCyclesIso e hj').hom ≫ K.iCycles j = (K.extend e).iCycles j' ≫ (K.extendXIso e hj').hom :=
by
rw [← cancel_epi (K.extendCyclesIso e hj').inv, Iso.inv_hom_id_assoc]
dsimp [extendCyclesIso, iCycles]
rw [assoc, ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc]
dsimp
rw [assoc, Iso.inv_hom_id, comp_id, ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i]
