mapCyclesIso_eq — Mathlib

English

For φ between ShortComplexs S1, S2 and hl1, hl2 left data with F preserving zero morphisms, the mapped cyclesMap' commutes with F: F.map (cyclesMap' φ hl1 hl2) = cyclesMap' (F.mapShortComplex.map φ) (hl1.map F) (hl2.map F).

Русский

Для φ между ShortComplex S1,S2 и данных левой гомологии hl1, hl2, с сохранением нулевых морфизмов F, отображение cyclesMap' коммутирует: F.map (cyclesMap' φ hl1 hl2) = cyclesMap' (F.mapShortComplex.map φ) (hl1.map F) (hl2.map F).

LaTeX

$$$F.map (ShortComplex.cyclesMap' \phi hl_1 hl_2) = ShortComplex.cyclesMap' (F.mapShortComplex.map \phi) (hl_1.map F) (hl_2.map F).$$$

Lean4

theorem mapCyclesIso_eq [S.HasLeftHomology] [F.PreservesLeftHomologyOf S] :
    S.mapCyclesIso F = (hl.map F).cyclesIso ≪≫ F.mapIso hl.cyclesIso.symm :=
  by
  ext
  dsimp [mapCyclesIso, cyclesIso]
  simp only [map_cyclesMap', ← cyclesMap'_comp, Functor.map_id, comp_id, Functor.mapShortComplex_obj]

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