If $X$ is an integral scheme, then in the internal logic, does $\mathscr{O}_X$ have decidable equality and is it an integral domain?

36 Views Asked by At

(Loosely inspired by: Decide if an element in a ring is zero or not to prove that $a*b=0\rightarrow a=0\lor b=0$ )

So, we know for example that in the ringed space $(\mathbb{R}, C(\mathbb{R}))$, equality of elements of $C(\mathbb{R})$ is not decidable in the internal logic, and $C(\mathbb{R})$ is not an integral domain in any sense either. Similarly, if we consider the scheme $\operatorname{Spec}(\mathbb{C}[x,y] / \langle xy \rangle)$, then $x=0$ evaluates to $D(y)$ and $x\ne 0$ evaluates to $D(x)$, so $x=0 \lor x\ne 0$ evaluates to $D(x) \cup D(y)$ and not the whole space; and definitely the structure sheaf on that scheme is not an integral domain.

However, if we take an irreducible scheme $X$, it seems like equality of elements of $\mathscr{O}_X$ should be decidable; and furthermore, if $X$ is integral, then $\mathscr{O}_X$ should be a model of an integral domain. To prove these, it's easy to reduce to the case where $X$ is an affine scheme. Past that, though, I keep getting bogged down in the details of how to evaluate the truth value of $f = 0$ in $\operatorname{Spec}(R)$ in general. My conjecture is that if $f$ is not a zero section, and the ideal of nilpotents is prime in $R$, then it evaluates to false.

(I also find myself wondering about the situation in other Grothendieck sites that are commonly used in algebraic geometry, such as 'etale sites, the fppf topology, the crystalline (or infinitesimal) site, etc. Certainly, in the crystalline site of a relative scheme $X / S$, then $\mathscr{O}_{X/S}$ is definitely not a model of an integral domain. Beyond that, my guess is that decidability of equality remains decidable in the nice cases, and the structure ring is an integral domain for the 'etale and fppf topologies; but again I get bogged down in the details.)