English
Given a natural transformation τ: F ⇒ G, the homology map of the induced map S.mapNatTrans τ expresses as a conjugation by the homology isomorphisms: homologyMap (S.mapNatTrans τ) = (S.mapHomologyIso F).hom ∘ τ.app S.homology ∘ (S.mapHomologyIso G).inv.
Русский
При натуральном преобразовании τ: F ⇒ G отображение гомологии гомологического отображения S.mapNatTrans τ выражается как сопряжение гомологическими изоморфизмами: homologyMap (S.mapNatTrans τ) = (S.mapHomologyIso F).hom ∘ τ.app S.homology ∘ (S.mapHomologyIso G).inv.
LaTeX
$$$\operatorname{homologyMap}(S.mapNatTrans(\tau)) = (S.mapHomologyIso F).hom \circ (\tau.app S.homology) \circ (S.mapHomologyIso G).inv$$$
Lean4
theorem homologyMap_mapNatTrans [S.HasHomology] (τ : F ⟶ G) :
homologyMap (S.mapNatTrans τ) = (S.mapHomologyIso F).hom ≫ τ.app S.homology ≫ (S.mapHomologyIso G).inv :=
(LeftHomologyMapData.natTransApp S.homologyData.left τ).homologyMap_eq
