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 Presheaf #929

Closed mzeuner closed 2 years ago

mzeuner commented 2 years ago

This` PR contains two things:

  1. A proof that the right Kan-extension along a fully faithful functor gives a natural isomorphism.
  2. The correct construction of the structure sheaf on basic opens and its extension to the whole spectrum. It is also proved that the global section of the structure sheaf is the base ring using 1.

I'll put the proof that the structure sheaf on basic opens indeed satisfies the sheaf property (on a basis) in a separate PR.