mapOpcyclesIso_eq — Mathlib

English

For hr (RightHomologyData) and F, S.mapRightHomologyIso F equals (hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm.

Русский

Для hr и F: S.mapRightHomologyIso F = (hr.map F).rightHomologyIso ≪≫ F.mapIso hr.rightHomologyIso.symm.

LaTeX

$$$S.mapRightHomologyIso F = (hr.map F).rightHomologyIso \≪≫ F.mapIso hr.rightHomologyIso.symm.$$$

Lean4

theorem mapOpcyclesIso_eq [S.HasRightHomology] [F.PreservesRightHomologyOf S] :
    S.mapOpcyclesIso F = (hr.map F).opcyclesIso ≪≫ F.mapIso hr.opcyclesIso.symm :=
  by
  ext
  dsimp [mapOpcyclesIso, opcyclesIso]
  simp only [map_opcyclesMap', ← opcyclesMap'_comp, Functor.map_id, comp_id, Functor.mapShortComplex_obj]

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