English
Homotopy between short-complex morphisms is compatible with scalar multiplication: scaling a homotopy by a makes the component maps scale accordingly.
Русский
Гомотопия между морфизмами коротких комплексов совместима с умножением на скаляр: умножение на скаляр сохраняет соответствующую линейность компонент гомотопии.
LaTeX
$$Let h be a homotopy φ1 ↦ φ2. Then a·h is a homotopy a·φ1 ↦ a·φ2 with componentwise scaling.$$
Lean4
/-- Homotopy between morphisms of short complexes is compatible with the scalar multiplication. -/
@[simps]
def smul {φ₁ φ₂ : S₁ ⟶ S₂} (h : Homotopy φ₁ φ₂) (a : R) : Homotopy (a • φ₁) (a • φ₂)
where
h₀ := a • h.h₀
h₁ := a • h.h₁
h₂ := a • h.h₂
h₃ := a • h.h₃
comm₁ := by
dsimp
rw [h.comm₁]
simp only [smul_add, Linear.comp_smul]
comm₂ := by
dsimp
rw [h.comm₂]
simp only [smul_add, Linear.comp_smul, Linear.smul_comp]
comm₃ := by
dsimp
rw [h.comm₃]
simp only [smul_add, Linear.smul_comp]
