English
Let R be a commutative ring. For any open U in the prime spectrum of R and elements f,g in R, with g nonvanishing on U (i.e., g does not lie in any prime corresponding to a point of U), the value at any point x∈U of the section of the structure sheaf given by the Fractions-constant construction const R f g U hu equals the image of f/g in the localization of R at the prime corresponding to x.
Русский
Пусть R — коммутативное кольцо. Для любого открытого множества U в спектре Прайма кольца R и для элементов f, g в R, причём g не обращает нули на U (то есть g не лежит в ни одной из соответствующих точке x в U простых идеалов), значение секции структуры в точке x ∈ U константной конструкцией const R f g U hu равно образу дроби f/g в локализации R по соответствующему простому идеалу.
LaTeX
$$$\\forall R$ коммутативное кольцо, $U$ открытое множество в $\\operatorname{Spec} R$, $f,g \\in R$ и условие\\;hg: g\\notin\\mathfrak p(x)\\ (\\forall x\\in U)\\quad (\\mathrm{const}_{R}(f,g;U,hu))(x)=\\text{the class of } f/g \\text{ in } R_{\\mathfrak p(x)}.$$$
Lean4
theorem const_apply' (f g : R) (U : Opens (PrimeSpectrum.Top R))
(hu : ∀ x ∈ U, g ∈ (x : PrimeSpectrum.Top R).asIdeal.primeCompl) (x : U)
(hx : g ∈ (x : PrimeSpectrum.Top R).asIdeal.primeCompl) : (const R f g U hu).1 x = IsLocalization.mk' _ f ⟨g, hx⟩ :=
rfl
