Spec_map_residue — Mathlib

English

For any scheme X and a point x ∈ X, the morphism Spec(κ(x)) → Spec(𝒪_{X,x}) induced by the residue map is a closed immersion.

Русский

Для любой схемы X и точки x ∈ X отображение Spec(κ(x)) → Spec(𝒪_{X,x}), индуцированное резидум-схемой, является замкнутым вложением.

LaTeX

$$$$IsClosedImmersion(\\mathrm{Spec.map}(X.residue(x))).$$$$

Lean4

instance Spec_map_residue {X : Scheme.{u}} (x) : IsClosedImmersion (Spec.map (X.residue x)) :=
  IsClosedImmersion.spec_of_surjective (X.residue x) Ideal.Quotient.mk_surjective

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