English
For the opcycles, the same naturality holds for the hom part; see above.
Русский
Для операционных циклов в противоположной ориентации самособственный изоморфизм на однообъектном комплексе удовлетворяет естественности относительно отображения f:
LaTeX
$$$ (\\mathrm{singleObjOpcyclesSelfIso}\\ c j\\ A).\\mathrm{hom} \\; \\circ \\; \\mathrm{opcyclesMap}\\big((\\mathrm{single}\\ C\\ c\\ j).\\mathrm{map}(f)\\big)_j = f \\; \\circ \\; (\\mathrm{singleObjOpcyclesSelfIso}\\ c j\\ B).\\mathrm{hom} $$$
Lean4
@[reassoc (attr := simp)]
theorem singleObjOpcyclesSelfIso_hom_naturality :
(singleObjOpcyclesSelfIso c j A).hom ≫ opcyclesMap ((single C c j).map f) j =
f ≫ (singleObjOpcyclesSelfIso c j B).hom :=
by
rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc,
p_opcyclesMap, single_map_f_self, assoc, assoc, singleObjCyclesSelfIso_hom, singleObjOpcyclesSelfIso_hom, assoc]
