English
For any domain R, the function field of Spec R is the fraction field of R; i.e., IsFractionRing R (Spec R).functionField.
Русский
Для любой области R функция поле Spec R является дробно-обобщенным полем: IsFractionRing R (Spec R).functionField.
LaTeX
$$$\text{IsFractionRing }R (\operatorname{Spec} R).\mathrm{functionField}$ for every domain R.$$
Lean4
theorem functionField_isFractionRing_of_isAffineOpen [IsIntegral X] (U : X.Opens) (hU : IsAffineOpen U) [Nonempty U] :
IsFractionRing Γ(X, U) X.functionField := by
haveI : IsAffine _ := hU
haveI : IsIntegral U :=
@isIntegral_of_isAffine_of_isDomain _ _ _
(by rw [Scheme.Opens.toScheme_presheaf_obj, Opens.isOpenEmbedding_obj_top]; infer_instance)
delta IsFractionRing Scheme.functionField
convert
hU.isLocalization_stalk
⟨genericPoint X, (((genericPoint_spec X).mem_open_set_iff U.isOpen).mpr (by simpa using ‹Nonempty U›))⟩ using
1
rw [hU.primeIdealOf_genericPoint, genericPoint_eq_bot_of_affine]
ext; exact mem_nonZeroDivisors_iff_ne_zero
