English
If a closed point x is chosen in U, then the prime ideal corresponding to x is maximal in Γ(X, U).
Русский
Если выбратьClosed точку x в U, то прайм-идеал, соответствующий x, является максимальным в Γ(X, U).
LaTeX
$$$\text{If } x\text{ is closed, then } (\text{primeIdealOf } x)\text{ is maximal in } Γ(X,U)$$$
Lean4
/-- If a point `x : U` is a closed point, then its corresponding prime ideal is maximal. -/
theorem primeIdealOf_isMaximal_of_isClosed (x : U) (hx : IsClosed {(x : X)}) : (hU.primeIdealOf x).asIdeal.IsMaximal :=
by
have hx₀ : IsClosed { x } := by
simpa [← Set.image_singleton, Set.preimage_image_eq _ Subtype.val_injective] using
hx.preimage U.isOpenEmbedding'.continuous
apply (hU.primeIdealOf x).isClosed_singleton_iff_isMaximal.mp
rw [primeIdealOf, ← Set.image_singleton]
refine (Topology.IsClosedEmbedding.isClosed_iff_image_isClosed <| IsHomeomorph.isClosedEmbedding ?_).mp hx₀
apply (TopCat.isIso_iff_isHomeomorph _).mp
infer_instance
