singleObjOpcyclesSelfIso_inv_naturality

English

The inverse-compatibility relation for opcycles under a map f is given by:

Русский

Обратная совместимость опциклов при отображении f задаётся следующим тождеством:

LaTeX

$$$ \\mathrm{opcyclesMap}\\big((\\mathrm{single}\\ C\\ c\\ j).\\mathrm{map}(f)\\big)_j \\circ (\\mathrm{singleObjOpcyclesSelfIso}\\ c j\\ B).\\mathrm{inv} = (\\mathrm{singleObjOpcyclesSelfIso}\\ c j\\ A).\\mathrm{inv} \\circ f $$$

Lean4

@[reassoc (attr := simp)]
theorem singleObjOpcyclesSelfIso_inv_naturality :
    opcyclesMap ((single C c j).map f) j ≫ (singleObjOpcyclesSelfIso c j B).inv =
      (singleObjOpcyclesSelfIso c j A).inv ≫ f :=
  by
  rw [← cancel_mono (singleObjOpcyclesSelfIso c j B).hom, assoc, assoc, Iso.inv_hom_id, comp_id, ←
    singleObjOpcyclesSelfIso_hom_naturality, Iso.inv_hom_id_assoc]

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