instIsPreimmersionFromSpecResidueField

English

For any point x of a scheme X, the morphism from Spec of the residue field κ(x) to X, given by X.fromSpecResidueField x, is a preimmersion.

Русский

Для любой точки x схемы X отображение Spec κ(x) в X, заданное X.fromSpecResidueField x, является предиммersion.

LaTeX

$$$\\text{IsPreimmersion}(X.fromSpecResidueField\\;x)$$$

Lean4

instance {X : Scheme.{u}} (x : X) : IsPreimmersion (X.fromSpecResidueField x) :=
  by
  dsimp only [Scheme.fromSpecResidueField]
  rw [IsPreimmersion.comp_iff]
  infer_instance

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