instIsFractionRingCarrierStalkCommRingCatPresheafFunctionField

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)

Похожие утверждения