leftHomologyMap_op — Mathlib

English

There is a formula for (leftHomologyMap φ).op expressed by S2.rightHomologyOpIso.inv, rightHomologyMap (opMap φ), and S1.rightHomologyOpIso.hom.

Русский

Существует формула для (leftHomologyMap φ).op через S2.rightHomologyOpIso.inv, rightHomologyMap (opMap φ) и S1.rightHomologyOpIso.hom.

LaTeX

$$(leftHomologyMap φ).op = S2.rightHomologyOpIso.inv ≫ rightHomologyMap (opMap φ) ≫ S1.rightHomologyOpIso.hom$$

Lean4

theorem leftHomologyMap_op (φ : S₁ ⟶ S₂) [S₁.HasLeftHomology] [S₂.HasLeftHomology] :
    (leftHomologyMap φ).op = S₂.rightHomologyOpIso.inv ≫ rightHomologyMap (opMap φ) ≫ S₁.rightHomologyOpIso.hom :=
  by
  dsimp [rightHomologyOpIso, RightHomologyData.rightHomologyIso, rightHomologyMap, leftHomologyMap]
  simp only [← rightHomologyMap'_comp, comp_id, id_comp, leftHomologyMap'_op]

Похожие утверждения