English
Let S1 and S2 be short complexes with homology data, and φ: S1 → S2 a morphism. Then the composite built from the left homology data of S1, the inverse of its homology isomorphism, and the homology map through S2, followed by the right homology data of S2, equals the composition of the left data with φ in the middle and the right data of S2. In other words, a certain naturality relation holds for the homology maps with respect to φ.
Русский
Пусть S1 и S2 — короткие комплексы с гомологическими данными, и φ: S1 → S2 — морфизм. Тогда композиция, складывающаяся из левого гомологического данных S1, обратного изоморфизма гомологии, отображения гомологии через φ и правых данных S2, эквивалентна композиции через φ с левыми и правыми данными S2. Иными словами, выполняется естественная совместимость гомологии по отношению к φ.
LaTeX
$$$h_1.\pi \circ h_1.homologyIso^{-1} \circ homologyMap(\phi) \circ h_2.homologyIso.hom \circ h_2.ι = h_1.i \circ φ.τ_2 \circ h_2.p$$$
Lean4
@[reassoc]
theorem comp_homologyMap_comp [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData)
(h₂ : S₂.RightHomologyData) :
h₁.π ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom ≫ h₂.ι = h₁.i ≫ φ.τ₂ ≫ h₂.p :=
by
dsimp only [LeftHomologyData.homologyIso, RightHomologyData.homologyIso, Iso.symm, Iso.trans, Iso.refl,
leftHomologyIso, rightHomologyIso, leftHomologyMapIso', rightHomologyMapIso', LeftHomologyData.cyclesIso,
RightHomologyData.opcyclesIso, LeftHomologyData.leftHomologyIso, RightHomologyData.rightHomologyIso, homologyMap,
homologyMap']
simp only [assoc, rightHomologyι_naturality', rightHomologyι_naturality'_assoc, leftHomologyπ_naturality'_assoc,
HomologyData.comm_assoc, p_opcyclesMap'_assoc, id_τ₂, p_opcyclesMap', id_comp, cyclesMap'_i_assoc]
