opcyclesOpIso_hom_toCycles_op — Mathlib

English

For h with rightHomology, the inverse of the rightHomology isomorphism composed with the rightHomology morphism equals the morphism ι followed by the opcyclesIso inverse.

Русский

Для h с правой гомологией, композиция обратного изоморфизма правой гомологии и правого гомологического отображения равна морфизму ι затем инверсу OpCycles.

LaTeX

$$h.rightHomologyIso.inv \circ S.rightHomologyι = h.ι \circ h.opcyclesIso.inv$$

Lean4

@[reassoc (attr := simp)]
theorem opcyclesOpIso_hom_toCycles_op [S.HasLeftHomology] : S.opcyclesOpIso.hom ≫ S.toCycles.op = S.op.fromOpcycles :=
  by
  dsimp [opcyclesOpIso, toCycles]
  rw [← cancel_epi S.op.pOpcycles, p_fromOpcycles, RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc,
    LeftHomologyData.op_p, ← op_comp, LeftHomologyData.f'_i, op_g]

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