search

agda / cubical

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

Open subschemes #1096

Closed mzeuner closed 4 months ago

mzeuner commented 5 months ago

This builds on (https://github.com/agda/cubical/pull/1082) and (https://github.com/agda/cubical/pull/1086), but even with those two merged it is still a long one, my apologies...

The PR contains the following:

The file Cubical.Categories.Instances.ZFunctors has gotten quite big and type-checking it is starting to get slow. Ultimately, I think it should be split up into several files in a separate (functorial) AlgebraicGeometry directory, see this issue: https://github.com/agda/cubical/issues/1095 I'm postponing this for a separate PR though

MatthiasHu commented 4 months ago

@mzeuner Could you try to resolve the merge conflicts here or would you like me to do it?

mzeuner commented 4 months ago

@mzeuner Could you try to resolve the merge conflicts here or would you like me to do it?

This was harder than I expected, but now it should work...

MatthiasHu commented 4 months ago

In the future, it might be good to move the definition of support maps and related lemmas (currently in ZariskiLattice.UniversalProperty) to a separate file, since it does not depend on the Zariski lattice. But perhaps not in this PR. (Just discussed with @mzeuner .)

felixwellen commented 4 months ago

Is this PR intentionally open?

felixwellen commented 4 months ago

The PR contains the following:

* definition of standard (compact) open subfunctors of an affine scheme and proof that those are affine

* proof that any compact open subfunctor of an affine scheme is a qcqs-scheme

Do you have a reason for not putting these two (or maybe three?) points in different PRs?

MatthiasHu commented 4 months ago

Is this PR intentionally open?

Yes, @mzeuner and I discussed it a bit today and I am working on reviewing it.

felixwellen commented 4 months ago

Is this PR intentionally open?

Yes, @mzeuner and I discussed it a bit today and I am working on reviewing it.

Good - then I'll leave you to it.

felixwellen commented 4 months ago

ZFunctors should definitely be split up - no need to do it in this PR though. Otherwise it looks good to me and it still checks on current master -> merging.