English
Let R act on the target module V2 in a distributive way compatible with the base ring k. Then the collection of affine maps P1 →ᵃ[k] V2 inherits a left action of R defined pointwise by (r · f)(p) = r · f(p). This makes the space of affine maps an R-set, compatible with the affine structure, i.e., (r · f).linear = r · f.linear.
Русский
Пусть R действует на модуль V2 согласованно с кольцом k. Тогда множество аффинных отображений P1 →ᵃ[k] V2 наследует левое действие R, задаваемое точечно: (r · f)(p) = r · f(p). Это образует множество аффинных отображений как пространство с действием R, совместимое с линейной частью: (r · f).linear = r · f.linear.
LaTeX
$$$\forall r \in R,\ f:\,P_1 \to^{\mathrm{aff}}_k V_2\;\Rightarrow\; (r \cdot f)(p) = r \cdot f(p)\quad\text{and}\quad (r \cdot f)_{\mathrm{lin}} = r \cdot f_{\mathrm{lin}}$$$
Lean4
/-- The space of affine maps to a module inherits an `R`-action from the action on its codomain. -/
instance mulAction : MulAction R (P1 →ᵃ[k] V2)
where
smul c f := ⟨c • ⇑f, c • f.linear, fun p v => by simp [smul_add]⟩
one_smul _ := ext fun _ => one_smul _ _
mul_smul _ _ _ := ext fun _ => mul_smul _ _ _
