English
For natural transformation τ: F ⇒ G between functors, the app at homology is given by composing the isomorphisms for F and G around the middle map
Русский
Для натурального преобразования τ: F ⇒ G между функторными отображениями приложение на гомологии задаётся композициями вокруг середины мапы
LaTeX
$$$\tau.app\,S_{\mathrm{homology}} = (S.mapHomologyIso\,F)^{-1} \circ ShortComplex.homologyMap (S.mapNatTrans\,\tau) \circ (S.mapHomologyIso\,G)_{\mathrm{hom}}$$$
Lean4
theorem app_homology {F G : C ⥤ D} (τ : F ⟶ G) (S : ShortComplex C) [S.HasHomology] [F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [G.PreservesLeftHomologyOf S]
[F.PreservesRightHomologyOf S] [G.PreservesRightHomologyOf S] :
τ.app S.homology =
(S.mapHomologyIso F).inv ≫ ShortComplex.homologyMap (S.mapNatTrans τ) ≫ (S.mapHomologyIso G).hom :=
by rw [ShortComplex.homologyMap_mapNatTrans, assoc, assoc, Iso.inv_hom_id, comp_id, Iso.inv_hom_id_assoc]
