English
For X integral and x ∈ X, the stalk O_{X,x} is a localization of the function field X.functionField; i.e., IsFractionRing (X.presheaf.stalk x) X.functionField.
Русский
Для целого X и точки x локальный стержень O_{X,x} является локализацией поля функций X.functionField; т.е. IsFractionRing O_{X,x} X.functionField.
LaTeX
$$$[\operatorname{IsIntegral} X]\; (x:\,X)\Rightarrow \operatorname{IsFractionRing}(X.presheaf.stalk x) X.functionField.$$$
Lean4
instance [IsIntegral X] (x : X) : IsFractionRing (X.presheaf.stalk x) X.functionField :=
let U : X.Opens := (X.affineCover.f ((X.affineCover.idx x))).opensRange
have hU : IsAffineOpen U := isAffineOpen_opensRange (X.affineCover.f _)
let x : U := ⟨x, X.affineCover.covers x⟩
have : Nonempty U := ⟨x⟩
let M := (hU.primeIdealOf x).asIdeal.primeCompl
have := hU.isLocalization_stalk x
have := functionField_isFractionRing_of_isAffineOpen X U hU
let _hA := Presheaf.algebra_section_stalk X.presheaf x
have := functionField_isScalarTower X U x
.isFractionRing_of_isDomain_of_isLocalization M ↑(Presheaf.stalk X.presheaf x) (Scheme.functionField X)