Replace "finite type" with "of finite presentation"

[felixwellen]

Until recently I thought a scheme of finite type is locally of the form $\mathrm{Spec}(R[X_1,\dots,X_n]/(f_1,\dots,f_m))$ - but that is actually called scheme of finite presentation. So this should be wrong in quite a lot of places. We should change all drafts accordingly:

• [ ] A1-homotopy
• [ ] cech
• [ ] diffgeo
• [ ] elliptic
• [x] foundations
• [ ] proper
• [ ] random-facts
• [ ] sheaves
• [ ] stacks
• [ ] topology
• [ ] slides

[iblech]

I agree, only in the Noetherian case do these coincide (and our generic ring R is never Noetherian, as else all rings would be). Good catch!

[felixwellen]

Yes, good catch - not mine though ;-)

[felixwellen]

I think I replaced that now everywhere. I chose to also replace it in archived slides, since they might be reused.

[xuanruiqi]

I believe schemes of finite type are useful too. A scheme is finite type if it's locally $\mathbf{Spec} \ A$ where $R \rightarrow A$ is of finite type.

Stacks gives the definition: $R \rightarrow A$ is finite type if there is a surjection $R[x_1, ..., x_n] \rightarrow A$. This should be constructively valid, and I think is a workable definition.

[mnieper]

I believe schemes of finite type are useful too. A scheme is finite type if it's locally Spec A where R→A is of finite type.

Stacks gives the definition: R→A is finite type if there is a surjection R[x1,...,xn]→A. This should be constructively valid, and I think is a workable definition.

In classical algebraic geometry, a scheme of finite type is locally a closed subset of affine space. This would not necessarily be true in our setting because a closed subset needs to be given by finitely many equations. Thus, I wonder whether the verbatim copy of the classical notion of finite type is really that much of interest.

[felixwellen]

This issue was just about a mistake of mine in saying which external schemes we expect to match our internal notion of scheme. I have nothing against schemes of finite type in general ;-)

[felixwellen]

But I agree with Marc, that it is unclear if we can say anything interesting about schemes of finite type in our current framework.

[mnieper]

We might have to introduce infinitary logic to be able to talk sensibly about non-finite intersections of closed subsets. But that's just a very wild guess.

[xuanruiqi]

I don't think we need infinitary logic if we're not explicitly writing out the conjunctions. That said, it's probably impossible to construct explicitly any non-finitely-generated algebra and prove it to be so.

[xuanruiqi]

or in other words we could perhaps safely ignore this issue: it's very likely that any scheme we could reasonably define synthetically is of finite type externally.

[iblech]

That said, it's probably impossible to construct explicitly any non-finitely-generated algebra and prove it to be so.

Hm, what do you mean with that? For instance, the algebra $R[X_1,X_2,\ldots]$ and the power series algebra $R[[X]]$ (definable without infinitary language as the ring of functions $\mathbb{N} \to R[[X]]$) are provably not finitely generated.