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 things
The Yoneda embedding has something that looks like a left adjoint, although not quite, because we run into a mismatch of universe levels.
To each ℤ-functor, we can associate the lattice of compact open subfunctors that are classified by the Zariski lattice. This can be used to define the notion of an affine cover.
There are still a bunch of TODOs in Categories.Instances.ZFunctors that will hopefully be proved in later PRs.
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)).
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 (https://github.com/agda/cubical/pull/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 https://github.com/agda/cubical/issues/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)).