ℤ-Functors #1068
Merged
ℤ-Functors #1068
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
mortberg
reviewed
Oct 25, 2023
mortberg
reviewed
Oct 25, 2023
mortberg
requested changes
Oct 25, 2023
mortberg
approved these changes
Oct 27, 2023
LuuBluum
pushed a commit
to LuuBluum/cubical
that referenced
this pull request
Oct 29, 2023
* use improved ringsolver * delete one more line * get started * functorial action * identity action * Zar latt presheaf * ring structure on global section * unit and conunit of adjunction * new approach * reorganize and tidy up * def affine cover * remove FP stuff * collect TODOs * refacor * standard basic opens * more cleaning up * Structure sheaf * requested changes
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR introduces the category of ℤ-functors, i.e. functors from commutative rings to sets (of a given size), i.e. presheaves on
CommRing ^op. We show/introduce two thingsThere are still a bunch of TODOs in
Categories.Instances.ZFunctorsthat will hopefully be proved in later PRs.Once we have sites (#1031), we can define the Zariski topology on ℤ-functors and define quasi-compact, quasi-separated schemes as the Zariski sheaves that have an affine cover in the sense of this PR. See also the discussion in #657.
The ultimate goal is to do all of that for finitely presented algebras, where we can avoid the size issues. This would give us a predicative and constructive account of schemes of finite presentation (over some base
Spec(A)).