Formal Zariski topology: Positivity and points (Q2575775)

In the context of formal (pointfree) topology, i.e. predicative locale theory, the author considers the Zariski spectrum of a commutative ring. We recall that the Zariski spectrum is a solution to the following universal problem: for each commutative ring \(A\) with unit, find a topological space and a sheaf of local rings on it such that \(A\) is the ring of global sections of this sheaf. The author defines a formal Zariski topology. It is followed by a quest to define a positivity predicate on the Zariski spectrum, i.e.\ to consider it as an open locale. This is problematic since the natural candidate \(\forall n\in \mathbb{N}\) \(a^n\neq0\) is in general not a positivity predicate. It is one, precisely when the ring has recognizable nilpotents. In the context of \textit{basic} formal topology one can usually define the covering relation inductively and simultaneously define a positivity relation coinductively. This can be applied to the Zariski topology and indeed allows one to define a positivity relation. This relation can then be used to define a predicate which is equivalent with \(\neg (a \triangleleft \emptyset)\). However, in general this will fail to be open, and thus is not a positivity predicate. Finally, it is shown that Zariski topology is not spatial constructively, i.e. it `does not have enough points'.