English
Let S1, S2 be short complexes with left and right homology data, and F a functor preserving zero morphisms. For φ: S1 → S2, the homology maps commute with the homology isomorphisms under F:
Русский
Пусть S1, S2 — короткие комплексы с данными левой и правой гомологии, и F — функтор, сохраняющий нулевые морфизмы. Для φ: S1 → S2 гомологические отображения коммутируют с гомологическими изоморфизмами под F.
LaTeX
$$$\mathrm{homologyMap}(F.mapShortComplex.map\,\phi) \;\circ\; (S_2.mapHomologyIso\,F)_{\mathrm{hom}} \\= (S_1.mapHomologyIso\,F)_{\mathrm{hom}} \circ F(\mathrm{homologyMap}(\phi))$$$
Lean4
@[reassoc]
theorem mapHomologyIso_hom_naturality [S₁.HasHomology] [S₂.HasHomology] [(S₁.map F).HasHomology]
[(S₂.map F).HasHomology] [F.PreservesLeftHomologyOf S₁] [F.PreservesLeftHomologyOf S₂] :
@homologyMap _ _ _ (S₁.map F) (S₂.map F) (F.mapShortComplex.map φ) _ _ ≫ (S₂.mapHomologyIso F).hom =
(S₁.mapHomologyIso F).hom ≫ F.map (homologyMap φ) :=
by
dsimp only [homologyMap, homologyMap', mapHomologyIso, LeftHomologyData.homologyIso, LeftHomologyData.leftHomologyIso,
leftHomologyMapIso', leftHomologyIso, Iso.symm, Iso.trans, Iso.refl]
simp only [LeftHomologyData.map_leftHomologyMap', ← leftHomologyMap'_comp, comp_id, id_comp]
