English
For a constant section constructed as m/r on an open set U, the value at a point x in U is precisely the localization of m by r, i.e., the element m in the localization with denominator r.
Русский
Для константной секции, заданной как m/r на открытом множестве U, значение в точке x есть локализация m на знаменателе r.
LaTeX
$$$\text{const}\ M\ m\ r\ U\ hu\ x = \mathrm{LocalizedModule.mk\ } m ⟨r, hu x x.2⟩$$$
Lean4
/-- If `U` is an open subset of `Spec R`, `m` is an element of `M` and `r` is an element of `R`
that is invertible on `U` (i.e. does not belong to any prime ideal corresponding to a point
in `U`), this is `m / r` seen as a section of `M^~` over `U`.
-/
def const (m : M) (r : R) (U : Opens (PrimeSpectrum.Top R))
(hu : ∀ x ∈ U, r ∈ (x : PrimeSpectrum.Top R).asIdeal.primeCompl) : (tildeInModuleCat M).obj (op U) :=
⟨fun x => LocalizedModule.mk m ⟨r, hu x x.2⟩, fun x =>
⟨U, x.2, 𝟙 _, m, r, fun y =>
⟨hu _ y.2, by
simpa only [LocalizedModule.mkLinearMap_apply, LocalizedModule.smul'_mk, LocalizedModule.mk_eq] using
⟨1, by simp⟩⟩⟩⟩
