The local-ring isomorphism induced by the open chart identifies its literal prime localization map with the canonical map from the original stalk.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U)
(p : Spec Γ(X, U))instance : p.asIdeal.IsPrimeThe stalk at the image of a point of an affine chart is its coordinate ring localized at the actual prime.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U)
(p : Spec Γ(X, U))
local instance : p.asIdeal.IsPrime := p.isPrimedef IsAffineOpen.stalkIsoLocalization :
X.presheaf.stalk (hU.fromSpec p) ≅ CommRingCat.of (Localization.AtPrime p.asIdeal)The affine-chart local-ring isomorphism intertwines the two actual maps back to the ambient scheme.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u
variable {X : Scheme.{u}} {U : X.Opens} (hU : IsAffineOpen U)
(p : Spec Γ(X, U))
local instance : p.asIdeal.IsPrime := p.isPrimetheorem IsAffineOpen.SpecMap_stalkIsoLocalization_fromSpecStalk :
Spec.map (hU.stalkIsoLocalization p).hom ≫ X.fromSpecStalk (hU.fromSpec p) =
Spec.map (CommRingCat.ofHom (algebraMap Γ(X, U) (Localization.AtPrime p.asIdeal))) ≫
hU.fromSpec