English
For an open U in Spec R and a prime x ∈ U, the fiber/stalk construction M^~ gives a natural module structure on the localization at x, forming a module over the structure sheaf at U.
Русский
Для открытого U в Spec R и точки x ∈ U, построение M^~ образует естественную модульную структуру на локализации в x, образующую модуль над структурной оболочкой на U.
LaTeX
$$$\forall (R: Type) [\mathrm{CommRing} R] (M: \mathrm{ModuleCat} R)\; (U: \mathrm{Opens}(\mathrm{PrimeSpectrum.Top}\,R))\; (x: U),\; (M^~(U))_x \in \mathrm{Mod}$$$
Lean4
/-- For any open subset `U ⊆ Spec R`, `IsFraction` is the predicate expressing that a function
`f : ∏_{x ∈ U}, Mₓ` is such that for any `𝔭 ∈ U`, `f 𝔭 = m / s` for some `m : M` and `s ∉ 𝔭`.
In short `f` is a fraction on `U`. -/
def isFraction {U : Opens (PrimeSpectrum R)} (f : ∀ 𝔭 : U, Localizations M 𝔭.1) : Prop :=
∃ (m : M) (s : R), ∀ x : U, s ∉ x.1.asIdeal ∧ s • f x = LocalizedModule.mkLinearMap x.1.asIdeal.primeCompl M m
