English
In general, Spec.fromSpecStalk x factors through the germ at x via the isomorphism ΓSpecIso R and the stalk germ, giving a canonical description of the Spec-map from the stalk to the base scheme.
Русский
Spec.fromSpecStalk x факторизуется через germ в точке x с помощью изоморфности ΓSpecIso и stalk germ.
LaTeX
$$Spec.map ( (ΓSpecIso R).inv ≫ (Spec R).presheaf.germ Top Opens.instCompleteLattice.top x trivial )$$
Lean4
@[reassoc (attr := simp)]
theorem Spec_map_stalkSpecializes_fromSpecStalk {x y : X} (h : x ⤳ y) :
Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x :=
by
obtain ⟨_, ⟨U, hU, rfl⟩, hyU, -⟩ := (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ y) isOpen_univ
have hxU : x ∈ U := h.mem_open U.2 hyU
rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU, IsAffineOpen.fromSpecStalk,
IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp, TopCat.Presheaf.germ_stalkSpecializes]
