English
For short complexes S1 and S2 with homology, and any morphism φ: S1 → S2, the opposite of the homology map is equal to the composite obtained by passing φ to the opposite, using the left/right homology data isomorphisms. This expresses how homology behaves with respect to taking opposites.
Русский
Для коротких комплексов S1 и S2 с гомологией и любого морфизма φ: S1 → S2, перестановка маппинга гомологии в противоположном смысле равна композиции, полученной при переходе φ к противоположному и использовании соответствующих изоморфизмов левой и правой гомологии. Это выражает, как гомология ведёт себя при взятии противоположного.
LaTeX
$$$(S_1.homologyπ) \circ homologyMap(φ) \circ (S_2.homologyι) = (S_1.iCycles) \circ φ.τ_2 \circ (S_2.pOpcycles)$$$
Lean4
@[reassoc]
theorem π_homologyMap_ι [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) :
S₁.homologyπ ≫ homologyMap φ ≫ S₂.homologyι = S₁.iCycles ≫ φ.τ₂ ≫ S₂.pOpcycles := by
simp only [homologyι_naturality, homology_π_ι_assoc, p_opcyclesMap]
