p_comp_opcyclesIso_inv — Mathlib

English

For a RightHomologyData h on a short complex S with right homology, the equality h.p ≫ h.opcyclesIso.inv = S.pOpcycles holds.

Русский

Для правой гомологической структуры h на коротком комплексе S с правой гомологией выполняется равенство h.p ∘ h.opcyclesIso.inv = S.pOpcycles.

LaTeX

$$h.p \circ h.opcyclesIso.inv = S.pOpcycles$$

Lean4

@[reassoc (attr := simp)]
theorem p_comp_opcyclesIso_inv : h.p ≫ h.opcyclesIso.inv = S.pOpcycles :=
  by
  dsimp [pOpcycles, RightHomologyData.opcyclesIso]
  simp only [p_opcyclesMap', id_τ₂, id_comp]

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