Commit 2024-07-06 04:54 8a82ae6b
View on Github →Feat(AlgebraicGeometry/FromSpecStalk): Given a scheme X and a point x : X, the canonical scheme morphism from Spec(O_x) to X. (#13885)
In this pull request, we define:
Given a scheme X and a point x : X.carrier, AlgebraicGeometry.Scheme.fromSpecStalk X x is the canonical scheme morphism from Spec(O_x) to X.
This is helpful for constructing the canonical map from the spectrum of the residue field of a point to the original scheme.