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