English
Let X be integral and U ⊂ X an affine open nonempty. Then the prime ideal of the generic point of X under the IsAffineOpen primeIdealOf equals the generic point of Spec Γ(X,U).
Русский
Пусть X целый, U ⊂ X афинное открытое непустое. Тогда прайм-идеал общего пункта X относительно IsAffineOpen равенgenericPoint Spec Γ(X,U).
LaTeX
$$$h_U^{\text{primeIdealOf}}(\langle \text{genericPoint}(X), \; \cdots \rangle) = \text{genericPoint}(\operatorname{Spec} \Gamma(X,U)).$$$
Lean4
theorem primeIdealOf_genericPoint {X : Scheme} [IsIntegral X] {U : X.Opens} (hU : IsAffineOpen U) [h : Nonempty U] :
hU.primeIdealOf ⟨genericPoint X, ((genericPoint_spec X).mem_open_set_iff U.isOpen).mpr (by simpa using h)⟩ =
genericPoint (Spec Γ(X, U)) :=
by
haveI : IsAffine _ := hU
delta IsAffineOpen.primeIdealOf
convert
genericPoint_eq_of_isOpenImmersion
(U.toScheme.isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top).op))
-- Porting note: this was `ext1`
apply Subtype.ext
exact (genericPoint_eq_of_isOpenImmersion U.ι).symm
