stalkToFiberRingHom_germ — Mathlib

English

Evaluating the stalk-to-fiber hom on a germ recovers its value in the localized ring at the point.

Русский

Оценивание гомоморфа stalkToFiberRingHom на герме восстанавливает значение в локализации.

LaTeX

$$$stalkToFiberRingHom(R, x)(germ_{U,x}(s)) = s(x).$$$

Lean4

@[simp]
theorem stalkToFiberRingHom_germ (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R) (hx : x ∈ U)
    (s : (structureSheaf R).1.obj (op U)) :
    stalkToFiberRingHom R x ((structureSheaf R).presheaf.germ U x hx s) = s.1 ⟨x, hx⟩ :=
  RingHom.ext_iff.mp (CommRingCat.hom_ext_iff.mp (germ_comp_stalkToFiberRingHom R U x hx)) s

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