Gamma Spec duality

[kbuzzard]

Maps from a scheme to an affine scheme Spec(R) are the same as maps from R to the global sections of the scheme. This result, which extends to locally ringed spaces, would be a fine thing to type into Lean, because it would put the definition of a scheme through its paces.

https://stacks.math.columbia.edu/tag/01I1

is the result in the stacks project.

I have no plans to work on this right now, but it would be good to do it at some point, as a proof of concept (both that Lean can handle this sort of mathematics and that we've got the definitions straight).