Commit 2024-05-31 11:34 d52741c6

feat(AlgebraicGeometry/StructureSheaf): add two useful lemmas (#13398) Let $f : R \to S$ be a ring map

1. The preimage of some basic open set $D(x)$ under $\mathrm{Spec}f$ is $D(f(x))$ (proof is rfl)
2. the ring map $\Gamma(\mathcal{O} _ {\mathrm{Spec}R}, D(x)) \to \Gamma(\mathcal{O}_{\mathrm{Spec} S}, D(f(x))$ is the map between localizations R_x and S_{f(x)}. These are lemmas are found useful in #12371 by Andrew.