William Lawvere, in his 2015 CT talk "Alexander Grothendieck & the Concept of Space", introduced the "Barr-Boole-Galois topos", which plays the role that sets do for topological spaces (with respect to axiomatic cohesion), but for schemes instead (emphasis added):
In a topos of set-valued functors on the category of finitely-presentable algebras, each space X has, thanks to Yoneda, an 'inside' whose objects are (in general singular) figures of representable shapes, with incidence relations given by commutative triangles. This can be viewed as a discretely-opfibered category, but such is equivalent to a set-valued functor. [I disagree with the term 'functor of points' for this, because it is a functor whose actual values include all the figures of X. Of course, 'points' of some other space associated to X may represent figures in X, but for X itself the points of it are just the restriction of X to the category of finite field extensions. That category generates the Boolean part of the big topos. The usual definition of point is unwieldy because it amounts to taking the non-exact direct limit of that restricted points functor. In general, this Boolean topos is much better suited than the category of abstract sets to serve as 'base topos' in the case of non-algebraically closed ground field. Conflating 'figures in X' with 'points of X' has a sort of science fiction air he probably did not intend. Volterra called them 'elements'.] A better version of the 'underlying topological space' is internal to the Barr-Boole-Galois topos where the actual points functor lands; this choice is also necessary for a product preserving components functor.
It is evidently the "boolean part" of the topos of sheaves on the Big Zariski site. So one could think of it as modifying $\mathrm{Set}$ to some other category $C$. For one thing, this modification gives an actual contravariant adjunction $\mathrm{Sch}/\mathrm{Spec}(k) \leftrightarrow C$. But it gets much better: this adjunction has further adjoints on either side of each of the functors, and it serves as a setting for Lawvere's cohesion.
Can anyone define the "boolean part" of a topos? It should be a subtopos of a topos which is a boolean topos.
According to Lawvere, Barr showed that the boolean part of the big Zariski topos over $\mathrm{Spec}(k)$ is generated by sheaves on finite $k$-algebras. Does anyone know of a reference for this?
For those who have not heard of cohesion, here is the go-to example: the categories $\mathrm{Set}$ and $\mathrm{Top}$ sit in a sort of relation to one another, as naturally expressed with four separate functor: the functor $\pi_0$ taking a topological space to its connected components, the functor $D$ taking a set to the corresponding discrete topological space, the forgetful functor $U$, and the functor $C$ taking a set to the corresponding indiscrete topological space. $\pi_0$ is left adjoint to $D$, which is left adjoint to $U$, which is left adjoint to $C$ ($C$ for codiscrete). This, with a further few properties such as that $\pi_0$ preserves finite products, is a common phenomenon, and is what Lawvere calls a "cohesion". Cohesion is roughly an axiomatization of "when one can meaningfully talk about connected components", the connected components intuitively cohere with themselves like droplets of oil in water.
Vaguely, what is going on with Lawvere's definition that I am trying to work out is that Schemes over $\mathrm{Spec}(k)$ experience a cohesion, except for that sets must be modified to something like sheaves over the opposite category of the site of finite $k$-algebras to get this cohesion setup. One of these functors in the cohesion setup is like "the improved version of $\mathrm{Spec}$".
