English
A compatibility relation between germs and stalk-closed-point maps when passing to Spec R and X via a map φ: R → S.
Русский
Совместимость между гермом и стоячими точками при переходе к Spec R и X через отображение φ: R → S.
LaTeX
$$$X.\\mathrm{presheaf}.\\mathrm{germ} U \\_ h_U \\;\\gg\\; \\operatorname{stalkClosedPointTo}(\\mathrm{Spec.map}\\, φ \\;\\gg\\; X.fromSpecStalk x) = X.\\mathrm{presheaf}.\\mathrm{germ} U x \\;\\gg\\; φ$$$
Lean4
theorem germ_stalkClosedPointTo_Spec {R S : CommRingCat} [IsLocalRing S] (φ : R ⟶ S) :
(Spec R).presheaf.germ ⊤ _ trivial ≫ stalkClosedPointTo (Spec.map φ) = (ΓSpecIso R).hom ≫ φ :=
by
rw [stalkClosedPointTo, Scheme.stalkMap_germ_assoc, ← Iso.inv_comp_eq, ← ΓSpecIso_inv_naturality_assoc]
simp_rw [Opens.map_top]
rw [germ_stalkClosedPointIso_hom, Iso.inv_hom_id, Category.comp_id]