Joyal's construction of the spectrum of a commutative ring I am trying to understand bits and pieces of Lawvere's article Continuously Variable Sets; Algebraic Geometry = Geometric Logic. I'm not doing very well.
I know this is a lot to ask, but basically, I would like for someone to explain in more detail the whole construction described at the end of the paper. I was told the idea is to get a "free local ring", which is free simply because of the internal language of the corresponding sheaf topos which makes any ring locally free, but I really don't know what that means and I still don't understand the idea and details of the construction in the paper. I stress that I'm looking for a detailed explanation; I realize that the idea may be encapsulated in a short elegant statement, but I won't be able to decode it..
So... What the hell is going on there? :D
 A: Since I don't know precisely which parts of Lawvere's article you have difficulties with, this answer is a bit a long and tries to give a bit of context. If you want me to be more specific at some point, just say so.
Classically, the spectrum of a ring $A$ can be defined as the set of its prime ideals equipped with the Zariski topology. This topological space then has the following universal property: For any locally ringed space $X$ we have $\mathrm{Hom}_{\mathrm{LRS}}(X, \operatorname{Spec}(A)) \cong \mathrm{Hom}_{\mathrm{Ring}}(A, \Gamma(X,\mathcal{O}_X))$.
We can also express this property using the opposite categories $\mathrm{LRS}^{\mathrm{op}}$ and $\mathrm{RS}^{\mathrm{op}}$. These can be interpreted as the category of all local rings (with local homomorphisms) respectively as the category of all rings – where "all" means that not only ordinary rings are included, but also sheaves of rings on arbitrary topological spaces. The universal property then reads: $\mathrm{Hom}_{\mathrm{LRS}^{\mathrm{op}}}((\mathrm{Spec}(A),\mathcal{O}_{\mathcal{\mathrm{Spec}(A)}}), (X,\mathcal{O}_X)) \cong \mathrm{Hom}_{\mathrm{RS}^{\mathrm{op}}}((\mathrm{pt},A), (X,\mathcal{O}_X))$.
This says that $\mathcal{O}_{\mathrm{Spec}(A)}$ is the universal localization of $A$, that is the universal (initial) way to turn $A$ into a local ring. (In contrast, if you restrict your search to ordinary rings, i.e. sheaves of rings on the one-point space, then this optimization problem only has a solution if $A$ possesses exactly one prime ideal. See this MO answer by Peter Arndt for more on this point of view.)
Starting from this result, we might want to extend it to sheaves of rings $\mathcal{A}$. That is, given a sheaf of rings $\mathcal{A}$ on a topological space $Y$, we want to find a local sheaf of rings $\mathcal{A'}$ (living on some other space $Y'$) such that $\mathrm{Hom}_{\mathrm{LRS}^{\mathrm{op}}}(\mathcal{A}', \mathcal{O}_X) \cong \mathrm{Hom}_{\mathrm{RS}^{\mathrm{op}}}(\mathcal{A}, \mathcal{O}_X)$ for any local sheaf of rings $\mathcal{O}_X$ on any topological space $X$.
By the marvelous device of the internal language of a topos, to achieve this it suffices to give a construction of the spectrum of an ordinary ring for which the universal property stated in the beginning can be verified even in constructive mathematics.
Taken literally, this is not possible. Constructively, there may be nontrivial rings with no prime ideals, so that the spectrum as classically constructed is empty. This will then fail the universal property.
However, there is a remedy. In fact, there are multiple options. Joyal's is to construct the spectrum not as a topological space, but as a topos. (A topos may be nontrivial even if it has no global points, that is geometric morphisms from $\mathrm{Set}$ into the topos.) He does this by specifying a certain site (in fact the category of a certain preorder), constructing the sheaf topos on this site, and describing a certain local sheaf of rings in this topos. This topos is then a constructive replacement for the topological space $\mathrm{Spec}(A)$, and its local ring is the replacement for the structure sheaf of $\mathrm{Spec}(A)$.
Using the wonders of the internal language, Joyal's construction applies to any ring in any topos and yields a local ring in a (new) topos. In symbols, $\mathrm{Hom}_{\mathrm{LRT}^{\mathrm{op}}}(\mathrm{JoyalSpec}(\mathcal{A}), \mathcal{O}) \cong \mathrm{Hom}_{\mathrm{RT}^{\mathrm{op}}}(\mathcal{A},\mathcal{O})$ for any local ring $\mathcal{O}$ in any topos ($\mathrm{(L)RT}$ is the category of (locally) ringed toposes).
(Note that Joyal's construction is essentially the same as Hakim's in her thesis.)
A different remedy is to not go all the way to toposes, but construct $\mathrm{Spec}(A)$ as a locale. Its frame of opens can be neatly (and without recourse to prime ideals) described, it is the frame of radical ideals of $A$. The structure sheaf is then obtained by localizing the constant sheaf $\underline{A}$ at the generic filter, a certain subsheaf of $\underline{A}$. (A filter is a subset which fulfils precisely the dual axioms of that of a prime ideal, so that in classical logic a subset is a filter if and only if its complement is a prime ideal.) The universal property enjoyed by this construction is $\mathrm{Hom}_{\mathrm{LRL}^{\mathrm{op}}}(\mathrm{LocalicSpec}(\mathcal{A}), \mathcal{O}) \cong \mathrm{Hom}_{\mathrm{RL}^{\mathrm{op}}}(\mathcal{A},\mathcal{O})$ for any local sheaf of rings $\mathcal{O}$ on any locale ($\mathrm{(L)RL}$ is the category of (locally) ringed locales). The sheaf topos over $\mathrm{LocalicSpec}(\mathrm{A})$ coincides with the topos of Joyal's description.
To go full circle, a variant of this construction is to not give the frame of opens explicitly, but construct it as the Lindenbaum algebra of a certain propositional geometric theory. For any such theory, there is a locale whose points are precisely the models of the theory in $\mathrm{Set}$. In our context, we use the geometric theory of a filter in $A$. Its Lindenbaum algebra is then a locale (verifying the right universal property for the spectrum, even constructively) whose points are the filters in $A$ – so classically, its points are in one-to-one correspondence with the prime ideals of $A$. (See this math.SE answer for more details.)
Summarizing, we obtain a constructively sensible (topos-valid) construction of the spectrum (of any ring in any topos) simply by not considering the topological space of prime ideals (or filters), but by considering the locale of filters.
[Note for the curious: The locale of prime ideals yields the spectrum equipped with the flat topology. The locale of detachable prime ideals (or detachable filters, doesn't matter) yields the spectrum equipped with the constructible topology (sometimes called "patch topology"). In constructive mathematics, a subset $U$ of a set $X$ is detachable if and only if for any $x \in X$ either $x \in U$ or $x \not\in U$.]
