Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 14:26 b7626956

View on Github →

feat(algebraic_geometry/projective_spectrum): forward direction of homeomorphism between top_space of Proj and top_space of Spec (#13397) This pr is the start of showing that Proj is a scheme. In this pr, it will be shown that the locally on basic open set, there is a continuous function from the underlying topological space of Proj restricted to this open set to Spec of degree zero part of some localised ring. In the near future, it will be shown that this function is a homeomorphism.

Estimated changes