pOpcycles_extendOpcyclesIso_hom — Mathlib

English

Describes the forward compatibility between pOpcycles and extendOpcyclesIso as a natural transformation.

Русский

Обозначает естественную трансформацию совместимости между pOpcycles и extendOpcyclesIso.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem pOpcycles_extendOpcyclesIso_hom :
    (K.extend e).pOpcycles j' ≫ (K.extendOpcyclesIso e hj').hom = (K.extendXIso e hj').hom ≫ K.pOpcycles j := by
  simp only [← cancel_mono (K.extendOpcyclesIso e hj').inv, assoc, Iso.hom_inv_id, comp_id,
    pOpcycles_extendOpcyclesIso_inv, Iso.hom_inv_id_assoc]

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