Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-26 09:37 ebf8ff42

View on Github →

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.

Estimated changes