English
For φ: S1 → S2 and a functor F preserving zero morphisms, the naturality relation also holds for the primed variant of the homology map and iso'
Русский
Для φ: S1 → S2 и функторa 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.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf 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 [Iso.trans, Iso.symm, Functor.mapIso, mapHomologyIso']
simp only [←
RightHomologyData.rightHomologyIso_hom_naturality_assoc _ ((homologyData S₁).right.map F)
((homologyData S₂).right.map F),
assoc, ← RightHomologyData.map_rightHomologyMap', ← F.map_comp,
RightHomologyData.rightHomologyIso_inv_naturality _ (homologyData S₁).right (homologyData S₂).right]
