search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
454 stars 139 forks source link

The Structure Sheaf #941

Closed mzeuner closed 2 years ago

mzeuner commented 2 years ago

In this PR we construct the structure sheaf on the Zariski lattice of a commutative ring and prove the sheaf property. This builds on #929 but diverges a bit, so it might be best to close that PR.

The older and weaker "pullback" version can probably be removed now.

mzeuner commented 2 years ago

OK, hope the checks pass and the PR is ready to merge now.