English
The base map of the morphism fromSpecStalk at x sends the closed point of the stalk to x. In other words, the closed point of the stalk corresponds to the original point x under this morphism.
Русский
Базисное отображение из fromSpecStalk x отправляет закрытую точку локального кольца в x.
LaTeX
$$(h_U.fromSpecStalk hxU).base (closedPoint (X.presheaf.stalk x)) = x$$
Lean4
/-- The morphism from `Spec(O_x)` to `X` given by `IsAffineOpen.fromSpec` does not depend on the affine
open neighborhood of `x` we choose.
-/
theorem fromSpecStalk_eq (x : X) (hxU : x ∈ U) (hxV : x ∈ V) : hU.fromSpecStalk hxU = hV.fromSpecStalk hxV :=
by
obtain ⟨U', h₁, h₂, h₃ : U' ≤ U ⊓ V⟩ :=
Opens.isBasis_iff_nbhd.mp (isBasis_affine_open X) (show x ∈ U ⊓ V from ⟨hxU, hxV⟩)
transitivity fromSpecStalk h₁ h₂
· delta fromSpecStalk
rw [← hU.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_left).op]
erw [← Scheme.Spec_map (X.presheaf.map _).op, ← Scheme.Spec_map (X.presheaf.germ _ x h₂).op]
rw [← Functor.map_comp_assoc, ← op_comp, TopCat.Presheaf.germ_res, Scheme.Spec_map, Quiver.Hom.unop_op]
· delta fromSpecStalk
rw [← hV.map_fromSpec h₁ (homOfLE <| h₃.trans inf_le_right).op]
erw [← Scheme.Spec_map (X.presheaf.map _).op, ← Scheme.Spec_map (X.presheaf.germ _ x h₂).op]
rw [← Functor.map_comp_assoc, ← op_comp, TopCat.Presheaf.germ_res, Scheme.Spec_map, Quiver.Hom.unop_op]
