English
The sheafification construction yields a new sheaf of modules by extending the presheaf via the module structure and a compatible map functor.
Русский
Конструкция шейфификации порождает новую шару модулей, расширяя презапись через модульную структуру и совместимый вложенный функтор.
LaTeX
$$$\text{Sheafify}(\alpha, \varphi):= \text{SheafOfModules with val := (A.presheaf) \to (Sheaf of modules) via } smul_{\alpha,\varphi}.$$$
Lean4
/-- Assuming `α : R₀ ⟶ R.val` is the sheafification map of a presheaf of rings `R₀`
and `φ : M₀.presheaf ⟶ A.val` is the sheafification map of the underlying
sheaf of abelian groups of a presheaf of modules `M₀` over `R₀`, this is
the sheaf of modules over `R` which is obtained by endowing the sections of
`A.val` with a scalar multiplication. -/
noncomputable def sheafify : SheafOfModules.{v} R
where
val :=
letI := Sheafify.module α φ;
ofPresheaf A.val (Sheafify.map_smul _ _)
isSheaf := A.cond
