The Stacks project

Upgrade lemma-check-closed-infinitesimally Tag 0896

Ugly edit to make sure the lemma applies in the only spot it is used.
Really, we should add a bunch of results of the following kind. Given

X' ---> X
|       |
v       V
S' ---> S

a cartesian square of algebraic spaces or schemes where S' --> S is a
thickening and X' ---> S' satisfies P then X ---> S satisfies P.

This works for P="affine" in general and for
P="closed immersion", "finite", and more if the thickening has finite order
which is really the correct generality for the lemma (but it comes too early
in the stacks project so we can't use this terminology yet).

Tags: Added new tags

Reformulation of GET

Also: algebraization of formal closed subspaces...