Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-08 16:28 9b3fec55

View on Github →

feat(algebraic_geometry): Gamma-Spec adjunction (#9802) Define the adjunction between the functors Gamma (global sections) and Spec (to LocallyRingedSpace). I'm currently working on a more general version in http://arxiv.org/pdf/1103.2139.pdf (Theorem 2), which may require refactoring structure_sheaf and Spec.

Estimated changes