instIsPreimmersionFromSpecStalk — Mathlib

English

Let X be a scheme and x a point in X. The canonical morphism from the spectrum of the stalk of the structure sheaf at x to X is a preimmersion.

Русский

Пусть X — схема и x — точка на X. Каноническое отображение от спектра локального кольца 𝒪_{X,x} к X является предиммерсией.

LaTeX

$$$\operatorname{Spec}(\mathcal{O}_{X,x}) \to X$ is a preimmersion for every $x \in X$.$$

Lean4

instance {X : Scheme.{u}} (x : X) : IsPreimmersion (X.fromSpecStalk x) :=
  IsAffineOpen.fromSpecStalk_isPreimmersion _ _ _

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