mathlib

ebf8ff42 - feat(algebraic_geometry/projective_spectrum/Scheme): the function from Spec to Proj restricted to basic open set. (#15259)

feat(algebraic_geometry/projective_spectrum/Scheme): the function from Spec to Proj restricted to basic open set. (#15259) We want to have a homeomorphism between $\mathrm{Proj}|_{D(f)}$ to $\mathrm{Spec}{A^0_f}$, we have the forward direction already. This PR is the underlying function of backward direction. Continuity will be proved separately.