What is the correct condition corresponding externally to "X is a scheme over a field"?

[xuanruiqi]

So, in algebraic geometry we're often interested in varieties which are usually defined as an integral, separated scheme of finite type over an (algebraically closed) field $k$. Basically, we're studying schemes over $k$ in this case, so I assume we want to be working in the big Zariski topos of $\mathrm{Spec} \ k$ in this case.

Now, we know very well that $R$ is just the internal view of $\underline{\mathbb{A}}^1_{\mathrm{Spec} \ k} = \underline{\mathrm{Spec} \ k[t]}$ (i.e. the functor of points of $\mathrm{Spec} \ k[t]$). The question is, what internal properties would characterize this fact?

[felixwellen]

Good question! Have you seen @iblech 's talk at the last meeting in Augsburg? It is available on youtube. I don't know if Ingo has any updates on the idea presented there.

[xuanruiqi]

Sure, we can discuss it at the coming meeting!

[iblech]

Great question, @xuanruiqi. My position is unchanged from the last Augsburg meeting which Felix referenced: In cases where classically we would use or require that the base ring is a field, in SAG we can use an appropriate modality. In most cases this should have the same effect (and still be a bit more general than literally requiring the base ring to be a field).

At least for propositions, the modality is simple to describe: "∇p" means that there merely exist some elements x_1, ..., x_n of R such that p holds under the condition that all of these are each zero or invertible. So ∇ is exactly what you need in order to get unstuck in proofs which would like R to be a field.

[xuanruiqi]

Sure, I'm pretty convinced that requiring $R$ to be a literal field is not the right condition. Still, I'm wondering if it is doable with direct axioms on $R$.

I would conjecture that if $k$ is algebraically closed then all non-constant monic polynomials in $R[x]$ should have at least one zero. But of course I have no proof yet.

[markrd-williams]

I think this is true because for a polynomial $g$ the $k$-points of $\mathrm{Spec}(k[x]/g)$ correspond to roots of $g$ in $k[x]$. So since externally we have $\mathrm{Spec}(k[x]/g)$ has a $k$-point by algebraic closure, then internally $\mathrm{Spec}(R[x]/g)$ has a point, and so internally $g$ has a root.

[MatthiasHu]

@markrd-williams This is true if you want to prove the statement for all (external) polynomials over $k$. But it does not prove the internal statement "Every monic polynomial of positive degree has a root.". Here we have an internal quantification over $R[X]$ instead of an external quantification over $k[X]$.

[MatthiasHu]

@xuanruiqi

Indeed, the internal statement "$R$ is a decidable field." (that is, "Every element of $R$ is 0 or invertible.") is always wrong. (Its negation is modeled.)

The internal statement "Every monic polynomial of positive degree has (merely) a root." is also always wrong! [See Example A.0.3 in the appendix of Foundations.]

On the other hand, the internal statement "Every monic polynomial of positive degree does not not have a root." is always true, even if $k$ is not algebraically closed or even a field. [See Proposition 18.32 in Ingo's thesis or Lemma 2.2.4 in Foundations.]

[markrd-williams]

@MatthiasHu Ah yes, makes sense, thanks for clearing that up!

[hmoeneclaey]

Hi just wanted to add that I think that monic polynomial merely having roots should hold interpreted inside fppf sheaves, the same way that the ring being local holds interpreted in Zariski sheaves, no matter what the base ring is.

So assuming monic polynomial have roots + Zariski local choice sounds reasonable assuming that "every Zariski sheaf is an fppf sheaf". I have no clue over which base ring this holds if any.

But feel free to work with the modality forcing monic polynomials to have roots, which I (optimistically) call the the fppf modality in the notes on sheaves!

[MatthiasHu]

I understand the opening question as: What is an internal statement that is modeled if and only if the external base ring $k$ is a field?

Such a characterization is impossible: if k = 0 (the trivial ring) then every statement at all is modeled internally -- but the trivial ring is not a field.

Here is a perhaps more convincing reason: If some internal statement is modeled in a topos, then it is also modeled in every slice topos of that topos. (*) And among the slice toposes of the big Zariski topos of Spec $k$ is the big Zariski topos of Spec $A$ for every $k$-algebra $A$. And if $k$ is a field, then for example $A = k[X]$ is not a field.

(*) Caveat: I can say this for sure if by "internal statement" we mean a first-order formula, so for example a property of $R$ expressed in the first-order language of rings. For general type-theoretic "statements" something similar should be true, but I don't know the details (or how they depend on the specific model of type theory one builds out of the given topos/site).

[MatthiasHu]

Something positive we can say internally if $k$ is a field is this: if $\mathrm{char}(k) = 0$, then internally " $\mathrm{char}(R) = 0$ " in the sense that every prime number has an inverse in $R$ (in other words: $R$ is a $\mathbb{Q}$-algebra). And if $\mathrm{char}(k) = p$, then $p = 0$ in $R$ and all other prime numbers have inverses in $R$. But of course this is far from expressing that $k$ is a field. It could for example also be an algebra over a field of the respective characteristic.

In general (for any external base ring $k$), we can say that $R$ is a $k$-algebra. (Slightly confusingly, because $k$ is an external ring and $R$ is an internal ring.) The above follows from this.

[xuanruiqi]

Fortunately we can always do some reverse mathematics: e.g., if we define a planar algebraic curve to be a subtype of $\mathbb{P}^2$ such that some homogeneous polynomial $f$ on $\mathbb{P}^2$ vanishes. Of course, we want it to be non-empty, but I guess we can also put inhabitedness in the definition.

On the other hand, "every prime number has an inverse in $R$" seems like an useful axiom in some cases.

[xuanruiqi]

Here is a perhaps more convincing reason: If some internal statement is modeled in a topos, then it is also modeled in every slice topos of that topos. (*) And among the slice toposes of the big Zariski topos of Spec k is the big Zariski topos of Spec A for every k-algebra A. And if k is a field, then for example A=k[X] is not a field.

In a type-theoretic setting, this should still be true b/c this follows is a consequence of the fact that a slice of a sheaf is a sheaf on a slice if I understand correctly.