English
There is a natural equation linking X.fromSpecStalk x with the morphism to the corresponding Γ-constructed Spec, showing that the stalk-to-Γ map is compatible with base changes and the Spec functor.
Русский
Существует естественное равенство между X.fromSpecStalk x и отображением в SpecΓ, показывающее совместимость stalk→Γ с изменениями базиса и функцией Spec.
LaTeX
$$fromSpecStalk_toSpecΓ (X) (x) : X.fromSpecStalk x ≫ X.toSpecΓ = Spec.map (X.presheaf.germ ⊤ x trivial)$$
Lean4
/-- For a local ring `(R, 𝔪)`,
this is the isomorphism between the stalk of `Spec R` at `𝔪` and `R`. -/
noncomputable def stalkClosedPointIso : (Spec R).presheaf.stalk (closedPoint R) ≅ R :=
StructureSheaf.stalkIso _ _ ≪≫
(IsLocalization.atUnits R (closedPoint R).asIdeal.primeCompl fun _ ↦ not_not.mp).toRingEquiv.toCommRingCatIso.symm
