English
Let U be an open subset of the projective spectrum and x a point of U. For any section s of the structure sheaf over U, when we view its germ at x in the fiber ring and apply the canonical stalk-to-fiber map, we obtain the value of s at x.
Русский
Пусть U — открытое подмножество проективного спектра и x—точка в U. Для любого секционного элемента s структуры пучка на U, при рассмотрении его germ в стеке над x и применении канонического отображения из стека в локальный кольцевой плод, получаем значение s в x.
LaTeX
$$$\operatorname{stalkToFiberRingHom}_{\mathcal{A}}(x,\operatorname{germ}_{x}(s)) = s^{(1)}\langle x,\text{hx}\rangle,$$$
Lean4
@[simp]
theorem stalkToFiberRingHom_germ (U : Opens (ProjectiveSpectrum.top 𝒜)) (x : ProjectiveSpectrum.top 𝒜) (hx : x ∈ U)
(s : (Proj.structureSheaf 𝒜).1.obj (op U)) :
stalkToFiberRingHom 𝒜 x ((Proj.structureSheaf 𝒜).presheaf.germ _ x hx s) = s.1 ⟨x, hx⟩ :=
RingHom.ext_iff.1 (CommRingCat.hom_ext_iff.mp (germ_comp_stalkToFiberRingHom 𝒜 U x hx)) s
