English
If h is a homotopy from f to g, and a is a scalar from a semiring R, then a • h is a homotopy from a • f to a • g. The homotopy components are given by a times the original components, with compatible zero and commutativity conditions under scalar action.
Русский
Если h — гомотопия от f к g, и a — скаляр из полускольного кольца R, то a • h является гомотопией от a • f к a • g. Компоненты гомотопии задаются умножением на a, сохраняются нулевые и коммутативные условия при скалярном действии.
LaTeX
$$$\text{smul}:\text{Homotopy}(f,g) \times R \to \text{Homotopy}(a f, a g),\ (h,a) \mapsto (a\cdot h)\,.$$$
Lean4
/-- the scalar multiplication of an homotopy -/
@[simps!]
def smul {R : Type*} [Semiring R] [Linear R V] (h : Homotopy f g) (a : R) : Homotopy (a • f) (a • g)
where
hom i j := a • h.hom i j
zero i j hij := by rw [h.zero i j hij, smul_zero]
comm
i := by
dsimp
rw [h.comm]
dsimp [fromNext, toPrev]
simp only [smul_add, Linear.comp_smul, Linear.smul_comp]
