English
Let C be as above and f: A → B. The inverse of the single-object homology self-iso also participates in a naturality relation with the j-th homology map:
Русский
Пусть C удовлетворяет условиям и есть f: A → B. Обратный изоморфизм самопереноса гомологии на j-м уровне удовлетворяет естественности с гомологическим отображением:
LaTeX
$$$ (\\mathrm{singleObjHomologySelfIso}\\ c j\\ A).\\mathrm{inv} \\; \\circ \\; \\operatorname{homologyMap}\\big((\\mathrm{single}\\ C\\ c\\ j).\\mathrm{map}(f)\\big)_j = \\; f \\; \\circ \\; (\\mathrm{singleObjHomologySelfIso}\\ c j\\ B).\\mathrm{inv} $$$
Lean4
@[reassoc (attr := simp)]
theorem singleObjHomologySelfIso_inv_naturality :
(singleObjHomologySelfIso c j A).inv ≫ homologyMap ((single C c j).map f) j =
f ≫ (singleObjHomologySelfIso c j B).inv :=
by
rw [← cancel_mono (singleObjHomologySelfIso c j B).hom, assoc, assoc, singleObjHomologySelfIso_hom_naturality,
Iso.inv_hom_id_assoc, Iso.inv_hom_id, comp_id]
