rightHomologyIso_inv_comp_rightHomologyι

English

Same as the previous statement: 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\u03b9 = h.\u027e ≫ h.opcyclesIso.inv$$

Lean4

@[reassoc (attr := simp)]
theorem rightHomologyIso_inv_comp_rightHomologyι :
    h.rightHomologyIso.inv ≫ S.rightHomologyι = h.ι ≫ h.opcyclesIso.inv :=
  by
  dsimp only [rightHomologyι, rightHomologyIso, opcyclesIso, rightHomologyMapIso', opcyclesMapIso', Iso.refl]
  rw [rightHomologyι_naturality']

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