extendCyclesIso_inv_iCycles — Mathlib

English

Compatibility of extended cycles iso with i-cycles: the inverse of the extend cycles iso composed with iCycles equals iCycles composed with the inverse of extendXIso.

Русский

Совместимость расширенного цикла ∼ с i-циклами: обратный extendCyclesIso, композиция с iCycles равна iCycles композиции inv extendXIso.

LaTeX

$$$ (K.extendCyclesIso e hj').inv \circ (K.extend e).iCycles j' = K.iCycles j \circ (K.extendXIso e hj').inv $$$

Lean4

@[reassoc (attr := simp)]
theorem extendCyclesIso_inv_iCycles :
    (K.extendCyclesIso e hj').inv ≫ (K.extend e).iCycles j' = K.iCycles j ≫ (K.extendXIso e hj').inv := by
  simp only [← cancel_epi (K.extendCyclesIso e hj').hom, Iso.hom_inv_id_assoc, extendCyclesIso_hom_iCycles_assoc,
    Iso.hom_inv_id, comp_id]

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