English
Let φ and φ′ be morphisms with fixed right homology data h1,h2. Then the opcyclesMap' is additive in φ: opcyclesMap'(φ+φ') h1 h2 = opcyclesMap'(φ) h1 h2 + opcyclesMap'(φ') h1 h2.
Русский
Пусть φ и φ′ — морфизмы с фиксированными правыми данными гомологии h1,h2. Тогда opcyclesMap' аддитивна по φ: opcyclesMap'(φ+φ') h1 h2 = opcyclesMap'(φ) h1 h2 + opcyclesMap'(φ') h1 h2.
LaTeX
$$$\mathrm{opcyclesMap}'(\varphi+\varphi')\, h_1\, h_2 = \mathrm{opcyclesMap}'(\varphi)\, h_1\, h_2 + \mathrm{opcyclesMap}'(\varphi')\, h_1\, h_2$$$
Lean4
@[simp]
theorem opcyclesMap'_add : opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂ :=
by
have γ : RightHomologyMapData φ h₁ h₂ := default
have γ' : RightHomologyMapData φ' h₁ h₂ := default
simp only [γ.opcyclesMap'_eq, γ'.opcyclesMap'_eq, (γ.add γ').opcyclesMap'_eq, RightHomologyMapData.add_φQ]
