English
Let C be a category with zero morphisms and a zero object, and let c be a fixed complex shape on an index set ι with j ∈ ι. For objects A, B ∈ C and a morphism f: A → B, the j-th homology map induced by f is natural with respect to the canonical self-isomorphisms of the j-th homology of the single-object complex; i.e. the following equality of morphisms holds:
Русский
Пусть C — категория с нулевыми морфизмами и нулевым объектом, пусть c — фиксированная форма комплексa на компактности ι с элементом j ∈ ι. Для объектов A, B ∈ C и морфизма f: A → B естественность гомологического отображения на j-м уровне относительно канонических самопереносов j-й гомологии однообъектного комплекса; тождество
LaTeX
$$$ \\operatorname{homologyMap}\\big((\\mathrm{single}\\ C\\ c\\ j).\\mathrm{map}(f)\\big)_j \\circ (\\mathrm{singleObjHomologySelfIso}\\ c\\ j\\ B).\\hom \\\\ = \\\\ (\\mathrm{singleObjHomologySelfIso}\\ c\\ j\\ A).\\hom \\\\ \\circ \\\\ f. $$$$
Lean4
@[reassoc (attr := simp)]
theorem singleObjHomologySelfIso_hom_naturality :
homologyMap ((single C c j).map f) j ≫ (singleObjHomologySelfIso c j B).hom =
(singleObjHomologySelfIso c j A).hom ≫ f :=
by
rw [← cancel_epi (((single C c j).obj A).homologyπ j), homologyπ_naturality_assoc,
homologyπ_singleObjHomologySelfIso_hom, singleObjCyclesSelfIso_hom_naturality,
homologyπ_singleObjHomologySelfIso_hom_assoc]
