fromOpcycles_op_cyclesOpIso_inv — Mathlib

English

Same content as the previous entry: h.rightHomologyIso.inv ≫ S.rightHomologyι = h.ι ≫ h.opcyclesIso.inv.

Русский

То же самое, что и предыдущее: h.rightHomologyIso.inv ≫ S.rightHomologyι = h.ι ≫ h.opcyclesIso.inv.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem fromOpcycles_op_cyclesOpIso_inv [S.HasRightHomology] : S.fromOpcycles.op ≫ S.cyclesOpIso.inv = S.op.toCycles :=
  by
  dsimp [cyclesOpIso, fromOpcycles]
  rw [← cancel_mono S.op.iCycles, assoc, toCycles_i, LeftHomologyData.cyclesIso_inv_comp_iCycles,
    RightHomologyData.op_i, ← op_comp, RightHomologyData.p_g', op_f]

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