mapHomologyIso_eq — Mathlib

English

Under preservation assumptions, the mapHomologyIso of F equals the composition of (hl.map F).homologyIso with F.mapIso hl.homologyIso.symm.

Русский

При сохранении свойств отображение гомологии совпадает с композиционным изображением: S.mapHomologyIso F = (hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm.

LaTeX

$$$S.mapHomologyIso F = (hl.map F).homologyIso \;\circ\; F.mapIso hl.homologyIso.symm$$

Lean4

theorem mapHomologyIso_eq [S.HasHomology] [(S.map F).HasHomology] [F.PreservesLeftHomologyOf S] :
    S.mapHomologyIso F = (hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm :=
  by
  ext
  dsimp only [mapHomologyIso, homologyIso, ShortComplex.leftHomologyIso, leftHomologyMapIso', leftHomologyIso,
    Functor.mapIso, Iso.symm, Iso.trans, Iso.refl]
  simp only [map_leftHomologyMap', ← leftHomologyMap'_comp, comp_id, Functor.map_id, Functor.mapShortComplex_obj]

Похожие утверждения