cyclesOpIso_inv_op_iCycles — Mathlib

English

The inverse of cyclesOpIso composed with op.iCycles equals pOpcycles.op: S.cyclesOpIso.inv ∘ S.op.iCycles = S.pOpcycles.op.

Русский

Обратное cyclesOpIso, компонуемое с op.iCycles, равно pOpcycles.op: S.cyclesOpIso.inv ∘ S.op.iCycles = S.pOpcycles.op.

LaTeX

$$S.cyclesOpIso.inv \circ S.op.iCycles = S.pOpcycles.op$$

Lean4

@[reassoc (attr := simp)]
theorem cyclesOpIso_inv_op_iCycles [S.HasRightHomology] : S.cyclesOpIso.inv ≫ S.op.iCycles = S.pOpcycles.op :=
  by
  dsimp [cyclesOpIso]
  rw [← S.rightHomologyData.op.cyclesIso_hom_comp_i, Iso.inv_hom_id_assoc]
  rfl

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