pOpcycles_restrictionOpcyclesIso_hom

English

The inverse of restrictionOpcyclesIso composed with pOpcycles equals the restrictionXIso inverse composed with restriction pOpcycles.

Русский

Обратный к restrictionOpcyclesIso после pOpcycles равен inv restrictionXIso после restriction pOpcycles.

LaTeX

$$$$ K.pOpcycles j' \;\circ\; (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv = (K.restrictionXIso e hj').inv \circ (K.restriction e).pOpcycles j $$$$

Lean4

@[reassoc (attr := simp)]
theorem pOpcycles_restrictionOpcyclesIso_hom :
    (K.restriction e).pOpcycles j ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom =
      (K.restrictionXIso e hj').hom ≫ K.pOpcycles j' :=
  by simp [restrictionOpcyclesIso]

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