pOpcycles_extendOpcyclesIso_inv — Mathlib

English

Relates the inverse of extendOpcyclesIso with the inverse of extendXIso through pOpcycles in the left homology data.

Русский

Связь обратного extendOpcyclesIso с обратным extendXIso через pOpcycles в левой гомологической структуре.

LaTeX

$$K.pOpcycles j ≫ (K.extendOpcyclesIso e hj').inv = (K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j'$$

Lean4

@[reassoc (attr := simp)]
theorem pOpcycles_extendOpcyclesIso_inv :
    K.pOpcycles j ≫ (K.extendOpcyclesIso e hj').inv = (K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j' :=
  by
  rw [← cancel_mono (K.extendOpcyclesIso e hj').hom, assoc, assoc, Iso.inv_hom_id, comp_id]
  dsimp [extendOpcyclesIso, pOpcycles]
  rw [ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc]
  dsimp
  rw [assoc, Iso.inv_hom_id_assoc, ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv]
  rfl

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