germ_stalkClosedPointTo_Spec — Mathlib

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]

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