English
The section of structureSheaf R on an open U that maps each x ∈ U to the element f/g in the localization of R at x, provided g is invertible in the localization at x.
Русский
Раздел structureSheaf R на открытом U задаётся как f/g в локализации R в каждой точке x ∈ U, при условии, что g обращаемо в локализации в x.
LaTeX
$$$\\mathrm{const}\\;R\\;f\\;g\\;U\\;\\hu\\; : \\text{section} = \\big( x \\mapsto \\mathrm{IsLocalization.mk'}(\\mathrm{Localization.AtPrime} x.1.asIdeal)\\; f\\; \\langle g, \\hu x x.2\\rangle \\big)$$$
Lean4
/-- The section of `structureSheaf R` on an open `U` sending each `x ∈ U` to the element
`f/g` in the localization of `R` at `x`. -/
def const (f g : R) (U : Opens (PrimeSpectrum.Top R)) (hu : ∀ x ∈ U, g ∈ (x : PrimeSpectrum.Top R).asIdeal.primeCompl) :
(structureSheaf R).1.obj (op U) :=
⟨fun x => IsLocalization.mk' _ f ⟨g, hu x x.2⟩, fun x =>
⟨U, x.2, 𝟙 _, f, g, fun y => ⟨hu y y.2, IsLocalization.mk'_spec _ _ _⟩⟩⟩
