germ_stalkClosedPointTo — Mathlib

English

For any x in X and f: X.presheaf.stalk x → R with IsLocalHom f.hom, the germ formula aligns with stalk-closed-point construction after mapping via Spec.map φ and fromSpecStalk.

Русский

Для любого x в X и f: X.presheaf.stalk x → R с IsLocalHom f.hom, формула герма согласуется с конструированием stalk-closed-point после отображения через Spec.map φ и fromSpecStalk.

LaTeX

$$$\\text{germ}_{U} \\; (\\operatorname{Spec.map} f \\; \\gg \\; X.fromSpecStalk x) = \\text{germ}_{U}(x) \\; \\gg \\; f$$$

Lean4

@[reassoc]
theorem germ_stalkClosedPointTo (U : Opens X) (hU : f.base (closedPoint R) ∈ U) :
    X.presheaf.germ U _ hU ≫ stalkClosedPointTo f =
      f.app U ≫
        ((Spec R).presheaf.mapIso (eqToIso (preimage_eq_top_of_closedPoint_mem f hU).symm).op ≪≫ ΓSpecIso R).hom :=
  by
  rw [stalkClosedPointTo, Scheme.stalkMap_germ_assoc, Iso.trans_hom]
  congr 1
  rw [← Iso.eq_comp_inv, Category.assoc, ΓSpecIso_hom_stalkClosedPointIso_inv]
  simp only [Functor.mapIso_hom, Iso.op_hom, eqToIso.hom, TopCat.Presheaf.germ_res]

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