stalkToFiberRingHom_toStalk — Mathlib

English

The map to the stalk is compatible with passing to the stalk of the open and base ring, giving an isomorphism with localization to the stalk.

Русский

Совместимость перехода к stalk с переходом к открытому базовой локализации обеспечивает изоморфизм с локализацией к stalk.

LaTeX

$$$stalkToFiberRingHom\\_g x = toStalk(R, x) \\Rightarrow \\text{localizationToStalk}(x) \\cong \\mathcal{O}_{X,x}.$$$

Lean4

@[simp]
theorem stalkToFiberRingHom_toStalk (x : PrimeSpectrum.Top R) (f : R) :
    stalkToFiberRingHom R x (toStalk R x f) = algebraMap _ _ f :=
  RingHom.ext_iff.1 (CommRingCat.hom_ext_iff.mp (toStalk_comp_stalkToFiberRingHom R x)) _

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