English
There is a canonical module structure on the sections of the sheafification of the underlying presheaf of abelian groups of a presheaf of modules, with scalar multiplication defined via smul.
Русский
Существует каноническая структура модуля на секциях шейфификации базового афинного презаписи модуля над абелевой группой, где скалярное умножение задаётся через smul.
LaTeX
$$$\text{For each } X, \ A(X) \text{ is a } R(X)\text{-module with } (r,m) \mapsto smul_{\alpha,\varphi}(r, m).$$$
Lean4
/-- The module structure on the sections of the sheafification of the underlying
presheaf of abelian groups of a presheaf of modules. -/
noncomputable def module : Module (R.val.obj X) (A.val.obj X)
where
smul r m := smul α φ r m
one_smul := Sheafify.one_smul α φ
zero_smul := Sheafify.zero_smul α φ
smul_zero := Sheafify.smul_zero α φ
smul_add := Sheafify.smul_add α φ
add_smul := Sheafify.add_smul α φ
mul_smul := Sheafify.mul_smul α φ
