English
For S1, S2 with left homology data and a morphism φ between them, the map of φ under F commutes with the left homology maps: F.map (ShortComplex.leftHomologyMap' φ hl1 hl2) = ShortComplex.leftHomologyMap' (F.mapShortComplex.map φ) (hl1.map F) (hl2.map F).
Русский
Для S1, S2 с данными левой гомологии и морфизмa φ между ними, отображение φ под F коммутирует с отображениями левой гомологии: F.map (ShortComplex.leftHomologyMap' φ ...) = ShortComplex.leftHomologyMap' (...).
LaTeX
$$$F\map (ShortComplex.leftHomologyMap' \phi \ hl_1 \ hl_2) = ShortComplex.leftHomologyMap' (F.mapShortComplex.map \phi) (hl_1.map F) (hl_2.map F).$$$
Lean4
theorem map_cyclesMap' :
F.map (ShortComplex.cyclesMap' φ hl₁ hl₂) =
ShortComplex.cyclesMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F) :=
by
have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default
rw [γ.cyclesMap'_eq, (γ.map F).cyclesMap'_eq, ShortComplex.LeftHomologyMapData.map_φK]
