isClosed_singleton_iff_isClosedImmersion

English

Let X be a scheme and x ∈ X. Then the singleton {x} is closed in the underlying topological space of X if and only if the canonical morphism from the residue field κ(x) to X is a closed immersion.

Русский

Пусть X — схема и x ∈ X. Тогда множество {x} замкнуто в топологическом пространстве X тогда и только тогда, когда канонический морфизм Spec κ(x) → X является замкнутым погружением.

LaTeX

$$$\mathrm{IsClosed}({x}) \iff \mathrm{IsClosedImmersion}\bigl(X.fromSpecResidueField(x)\bigr)$$$

Lean4

theorem isClosed_singleton_iff_isClosedImmersion {X : Scheme} {x : X} :
    IsClosed ({ x } : Set X) ↔ IsClosedImmersion (X.fromSpecResidueField x) :=
  by
  rw [← Scheme.range_fromSpecResidueField]
  exact ⟨fun H ↦ .of_isPreimmersion _ H, fun _ ↦ (X.fromSpecResidueField x).isClosedEmbedding.isClosed_range⟩

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