specializes_closedPoint — Mathlib

English

In the spectrum of a local ring, every prime ideal specializes to the unique closed point (maximal ideal).

Русский

В спектре локального кольца каждая идеалprime (\n) специализируется к единственной замкнутой точке.

LaTeX

$$$\\forall x \\in \\mathrm{Spec}(R),\\ x \\Rightarrow^* \\mathrm{closedPoint}(R)$$$

Lean4

theorem specializes_closedPoint (x : PrimeSpectrum R) : x ⤳ closedPoint R :=
  (PrimeSpectrum.le_iff_specializes _ _).mp (IsLocalRing.le_maximalIdeal x.2.1)

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