English
Let C be a category with zero morphisms and S1, S2 be short complexes with right homology. For any morphism φ: S1 ⟶ S2, the opposite of the induced right homology map is given by the composite S2.leftHomologyOpIso^{-1} ∘ leftHomologyMap(opMap φ) ∘ S1.leftHomologyOpIso.hom.
Русский
Пусть C - категория с нулевыми морфизмами, и S1, S2 — короткие комплексы, обладающие правой гомологией. Для отображения φ: S1 ⟶ S2 противобразная карта правой гомологии равна композиции S2.leftHomologyOpIso^{-1} ∘ leftHomologyMap(opMap φ) ∘ S1.leftHomologyOpIso.hom.
LaTeX
$$$ (\\mathrm{rightHomologyMap}\\ φ)^{op} = S_2.leftHomologyOpIso^{-1} \\circ \\mathrm{leftHomologyMap}(\\mathrm{opMap}\\ φ) \\circ S_1.leftHomologyOpIso.hom $$$
Lean4
theorem rightHomologyMap_op (φ : S₁ ⟶ S₂) [S₁.HasRightHomology] [S₂.HasRightHomology] :
(rightHomologyMap φ).op = S₂.leftHomologyOpIso.inv ≫ leftHomologyMap (opMap φ) ≫ S₁.leftHomologyOpIso.hom :=
by
dsimp [leftHomologyOpIso, LeftHomologyData.leftHomologyIso, leftHomologyMap, rightHomologyMap]
simp only [← leftHomologyMap'_comp, comp_id, id_comp, rightHomologyMap'_op]
