fromSpecStalk_isPreimmersion — Mathlib

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

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