Feat(AlgebraicGeometry/FromSpecStalk): Given a scheme `X` and a point `x : X`, the canonical scheme morphism from `Spec(O_x)` to `X`.

[FMLJohn]

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.

[github-actions[bot]]

PR summary c53d86ee9d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicGeometry.Stalk	1536

---

Declarations diff

+ IsAffineOpen.fromSpecStalk + IsAffineOpen.fromSpecStalk_eq + IsAffineOpen.fromSpecStalk_eq_fromSpecStalk + Scheme.fromSpecStalk + Scheme.isoSpec_hom_naturality + Scheme.isoSpec_inv_naturality + map_fromSpec

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[kbuzzard]

This looks fine to me, I've left some comments which are mostly about docstrings.

[erdOne]

Thanks! maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style