fromSpecStalkOfMem — Mathlib

English

For a specialization h: x ⤳ y, the composition Spec.map (X.presheaf.stalkSpecializes h) with X.fromSpecStalk y equals X.fromSpecStalk x, echoing the naturality of stalk maps with specialization.

Русский

Для специализации h: x ⤳ y композиция Spec.map(stalkSpecializes h) с fromSpecStalk y даёт fromSpecStalk x.

LaTeX

$$Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x$$

Lean4

/-- The canonical map `Spec 𝒪_{X, x} ⟶ U` given `x ∈ U ⊆ X`. -/
noncomputable def fromSpecStalkOfMem {X : Scheme.{u}} (U : X.Opens) (x : X) (hxU : x ∈ U) :
    Spec (X.presheaf.stalk x) ⟶ U :=
  Spec.map (inv (U.ι.stalkMap ⟨x, hxU⟩)) ≫ U.toScheme.fromSpecStalk ⟨x, hxU⟩

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