singleObjCyclesSelfIso_inv_naturality

English

Naturality of the inverse cycles self-iso with respect to a morphism f: A ⟶ B, via cyclesMap and the iCycles iso.

Русский

Единообразность обратного cycles self-iso по отношению к морфизму f: A ⟶ B через cyclesMap и iCycles iso.

LaTeX

$$$\\text{cyclesMap}((\\mathrm{single} \\, C \\, c \\, j).\\mathrm{map} f) \\, j \\gg (\\mathrm{singleObjCyclesSelfIso} \\, c \\, j \\, B).\\mathrm{hom} = (\\mathrm{singleObjCyclesSelfIso} \\, c \\, j \\, A).\\mathrm{hom} \\gg f$$$

Lean4

@[reassoc (attr := simp)]
theorem singleObjCyclesSelfIso_inv_naturality :
    (singleObjCyclesSelfIso c j A).inv ≫ cyclesMap ((single C c j).map f) j = f ≫ (singleObjCyclesSelfIso c j B).inv :=
  by
  rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, Iso.hom_inv_id_assoc, ←
    singleObjCyclesSelfIso_hom_naturality_assoc, Iso.hom_inv_id, comp_id]

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