English
Given a section s of the structure sheaf over an open U, and a point x∈U, there exists a smaller open V⊆U containing x, a restriction i: V→U, and elements f,g∈R with an appropriate nonvanishing condition such that the const_R f g V hu equals the pullback of s along i.
Русский
Пусть дана секция s структуры оболочки над открытым множеством U и точка x∈U. Тогда существует ущеcшееся открытое V ⊆ U, содержащее x, отображение i: V→U и элементы f,g ∈ R с соответствующим условием ненулевости, такие что const_R f g V hu равна переносу секции s по i.
LaTeX
$$$\\exists V \\subseteq U, x\\in V, i: V\\to U, f,g\\in R, hg\\;:\\; g\\in V.asIdeal.primeCompl, \\text{ such that }\\; const(R,f,g,V,hg) = (structureSheaf R).1.map i^{op} s.$$$
Lean4
theorem exists_const (U) (s : (structureSheaf R).1.obj (op U)) (x : PrimeSpectrum.Top R) (hx : x ∈ U) :
∃ (V : Opens (PrimeSpectrum.Top R)) (_ : x ∈ V) (i : V ⟶ U) (f g : R) (hg : _),
const R f g V hg = (structureSheaf R).1.map i.op s :=
let ⟨V, hxV, iVU, f, g, hfg⟩ := s.2 ⟨x, hx⟩
⟨V, hxV, iVU, f, g, fun y hyV => (hfg ⟨y, hyV⟩).1,
Subtype.eq <| funext fun y => IsLocalization.mk'_eq_iff_eq_mul.2 <| Eq.symm <| (hfg y).2⟩
