mapHomologyIso'_eq — Mathlib

English

For right homology data, the mapRightHomologyIso of F equals the trans of (hr.map F).rightHomologyIso with F.mapIso hr.rightHomologyIso.symm.

Русский

Для правой гомологии отображение mapRightHomologyIso F равняется композиции (hr.map F).rightHomologyIso с F.mapIso hr.rightHomologyIso.symm.

LaTeX

$$$S.mapRightHomologyIso F = (hr.map F).rightHomologyIso \;\circ\; F.mapIso hr.rightHomologyIso.symm$$

Lean4

theorem mapHomologyIso'_eq [S.HasHomology] [(S.map F).HasHomology] [F.PreservesRightHomologyOf S] :
    S.mapHomologyIso' F = (hr.map F).homologyIso ≪≫ F.mapIso hr.homologyIso.symm :=
  by
  ext
  dsimp only [Iso.trans, Iso.symm, Iso.refl, Functor.mapIso, mapHomologyIso', homologyIso, rightHomologyIso,
    rightHomologyMapIso', ShortComplex.rightHomologyIso]
  simp only [assoc, F.map_comp, map_rightHomologyMap', ← rightHomologyMap'_comp_assoc]

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