English
The homologyι map on the single-object construction is adjoint to the inverse of the opcycles iso when composed with pOpcycles.
Русский
Гомологияι в конструкции с одиночным объектом сопряжена с противоположным изоморфизмом pOpcycles при композиции с pOpcyclesSelfIso.
LaTeX
$$$(\\mathrm{homology\\iota}_j) \\circ (\\mathrm{singleObjOpcyclesSelfIso} \\, c \\, j \\, A)^{-1} = (\\mathrm{singleObjHomologySelfIso} \\, c \\, j \\, A).hom$$$
Lean4
@[reassoc (attr := simp)]
theorem singleObjCyclesSelfIso_hom_naturality :
cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom = (singleObjCyclesSelfIso c j A).hom ≫ f :=
by
rw [← cancel_mono (singleObjCyclesSelfIso c j B).inv, assoc, assoc, Iso.hom_inv_id, comp_id, ←
cancel_mono (iCycles _ _)]
simp only [cyclesMap_i, singleObjCyclesSelfIso, Iso.trans_hom, iCyclesIso_hom, Iso.trans_inv, assoc,
iCyclesIso_inv_hom_id, comp_id, single_map_f_self]
