The Stacks project

Still didn't fix it correctly. Sigh!

Thanks to 李一笑

OK, I will try not to make a habit of fixing things wrong...

Fix missing arguments in proof OCXU

Thanks to 李一笑 who writes:

"The proof implicitly used that any dense subset of a noetherian
topological space contains a countable dense subset. Maybe this should
be made explicit and be formulated into a lemma."

After asking more 李一笑 also pointed out that

"What's more, it may not be the case that $E$ is infinite, for example
if there is an element of $E$ whose closure contains $u_{0}$. This case
should also be considered in 0CXS."

The first problem is addressed in this commit and the previous one
(7f41eb8f but I could only prove the existence of the countable dense
subset in the case of Noetherian schemes). The second problem was
addressed in 3e7633b0

Split out a lemma in artin and apply it

Thanks to 李一笑

Since finite type points aren't closed there can be specializations
between them. Thus we can ask if versality of objects "generalizes".

We missed this point in the proof of 0CXU as well as another one which
we will fix in the next commit

Tags: Added new tags

Strong formal effectiveness => openness versality

Actually not hard to prove and you only need to check on first order
thickenings.

Bhargav's example from c31011d shows that strong formal effectiveness
does not always hold. But what about strong formal effectiveness
where the thickenings are always first order (between any two, not
just between consecutive indices)? This is the only thing needed for
the argument here, so it would be nice if it was true for algebraic
stacks in general.