Structure presheaf #699
Structure presheaf #699
Conversation
|
I'll restart the CI for this PR now just to check that things still work after merging that revert |
|
|
||
| -- The structure presheaf on BO | ||
| BOCat : Category (ℓ-suc ℓ) (ℓ-suc ℓ) | ||
| BOCat = ΣPropCat (DistLatticeCategory ZariskiLattice) BasicOpens |
There was a problem hiding this comment.
One problem that maybe should be discussed before merging:
Using general machinery to define the structure sheaf through the universal property of localization,
we view the basic opens to as a category in the above way. This unfolds to them being a JoinSemilatticeCategory.
In the file Cubical.Categories.DistLatticeSheaf, the basic opens are viewed as a MeetSemilatticeCategory.
The two definitions come from the two ways of defining the order relation on a distributive lattice
(x≤y as y=x\/y vs x=x/\y) and they're thus equivalent but not definitionally equal.
I just thought maybe want make things uniform in one way or the other...
There was a problem hiding this comment.
Good catch! It's probably easier to change the DistLatticeSheaf? I can try to remember to do it when working on that file
|
|
||
|
|
||
|
|
||
| -- the Algebra version of uaCompEquiv |
There was a problem hiding this comment.
Are these lemmas really useful?
This PP introduces the basic opens of the Zariski lattice and constructs the structure presheaf on them.