primeIdealOf_eq_map_closedPoint — Mathlib

English

For a point x in U, the prime ideal associated to x coincides with the image under the Spec map of the germ at x evaluated at a closed point.

Русский

Для точки x в U прайм-идеал, соответствующий x, совпадает с образом через отображение Spec призмы germ в точке, являющейся закрытой точкой.

LaTeX

$$$h_U.\text{primeIdealOf}(x) = \text{Spec.map}(X.presheaf.germ\_x).base(\text{closedPoint})$$$

Lean4

theorem primeIdealOf_eq_map_closedPoint (x : U) :
    hU.primeIdealOf x = (Spec.map (X.presheaf.germ _ x x.2)).base (closedPoint _) :=
  hU.isoSpec_hom_base_apply _

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