English
For any X and point x, the morphism X.fromSpecStalk x is a preimmersion. This is a structural property indicating that the map reflects a local isomorphism on stalks.
Русский
Для любой X и точки x отображение X.fromSpecStalk x является предиммерсионным.
LaTeX
$$IsPreimmersion (X.fromSpecStalk x)$$
Lean4
instance fromSpecStalk_isPreimmersion {X : Scheme.{u}} {U : Opens X} (hU : IsAffineOpen U) (x : X) (hx : x ∈ U) :
IsPreimmersion (hU.fromSpecStalk hx) :=
by
dsimp [IsAffineOpen.fromSpecStalk]
haveI : IsPreimmersion (Spec.map (X.presheaf.germ U x hx)) :=
letI : Algebra Γ(X, U) (X.presheaf.stalk x) := (X.presheaf.germ U x hx).hom.toAlgebra
haveI := hU.isLocalization_stalk ⟨x, hx⟩
IsPreimmersion.of_isLocalization (R := Γ(X, U)) (S := X.presheaf.stalk x)
(hU.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl
apply IsPreimmersion.comp