Open subschemes

[mzeuner]

This builds on (#1082) and (#1086),
but even with those two merged it is still a long one, my apologies...

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

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: #1095
I'm postponing this for a separate PR though

[MatthiasHu]

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

[mzeuner]

@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]

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]

Is this PR intentionally open?

[felixwellen]

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]

Is this PR intentionally open?

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

[felixwellen]

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.

[MatthiasHu]

It seems weird to have this lemma only for Join and not for Meet. But this was already the case for other definitions in this file (and I find it pretty hard to see which ones)...

I guess this is part of the general question how to handle the duality between join and meet nicely.

[mzeuner]

I added the analogous case for meets of this one: ef4ae22

I did treat meets and joins symmetrically, but I never ended up using big meets, so a bunch of lemmas are only done for big joins. After all, they are what you need to define a "cover", so arguably the more useful one...

[felixwellen]

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.