English
There is a ring isomorphism between the stalk of the Proj structure sheaf at a point and the corresponding homogeneous localization at that point.
Русский
Существует изоморфизм колец между стоком пучка структуры Proj в точке и соответствующей однородной локализацией в этой точке.
LaTeX
$$$\text{Proj.stalkIso}'_{\mathcal{A}}(x): (\mathrm{stalk}_{x}) \cong \mathrm{AtPrime}_{\mathcal{A}} x$$$
Lean4
/-- Using `homogeneousLocalizationToStalk`, we construct a ring isomorphism between stalk at `x`
and homogeneous localization at `x` for any point `x` in `Proj`. -/
def stalkIso' (x : ProjectiveSpectrum.top 𝒜) : (Proj.structureSheaf 𝒜).presheaf.stalk x ≃+* at x
where
__ := (stalkToFiberRingHom _ x).hom
invFun := homogeneousLocalizationToStalk 𝒜 x
left_inv := homogeneousLocalizationToStalk_stalkToFiberRingHom 𝒜 x
right_inv := stalkToFiberRingHom_homogeneousLocalizationToStalk 𝒜 x
