restrictionCyclesIso_hom_iCycles — Mathlib

English

The inverse of restrictionCyclesIso composed with restriction iCycles equals iCycles' composed with restrictionXIso inverse.

Русский

Обратный к restrictionCyclesIso, затем iCycles составляется с inv restrictionXIso.

LaTeX

$$$$ (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv \;\circ\; (K.restriction e).iCycles j = K.iCycles j' \;\circ\; (K.restrictionXIso e hj').inv $$$$

Lean4

@[reassoc (attr := simp)]
theorem restrictionCyclesIso_hom_iCycles :
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.iCycles j' =
      (K.restriction e).iCycles j ≫ (K.restrictionXIso e hj').hom :=
  by simp [restrictionCyclesIso]

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