homomorphism $G^\ab \to M$ rendering the diagram

\[ \xymatrix{
G \ar[rd] \ar[rrr] &&& {\substack{\text{abelian}\\\text{\normalsize$\!M$}\\\phantom{\text{abelian}}}} \\
& {\substack{\text{\normalsize$G^\ab$}\\\text{abelian}}} \ar@{-->}_[@!29]{}[rru]
} \]

commutative. In textbooks, the abelianization is usually constructed as $G^\ab
= G/[G,G]$, that is as the quotient by the subgroup generated by the
commutators. This explicit construction makes it appear that abelianization
is a specific result in algebra pertaining to groups.

We can also cast the construction in logical language. This change in perspective makes it evident
that abelianization is just a special case of a more general procedure.
The free abelian group over $G$ can be obtained as the term model of the
theory of abelian groups extended by a constant $x_g$ for each element $g \in
G$ and the axioms

\begin{align*}
\top &\vdash x_{g \circ h} = x_g \circ x_h & \text{(for each~$g,h \in G$)} \\
\top &\vdash x_{g^{-1}} = x_g^{-1} & \text{(for each~$g \in G$)} \\
\top &\vdash x_e = e
\end{align*}

That is, $G^\ab$ contains exactly those elements and exactly those
identifications between elements such that $G^\ab$ is an abelian group and such
that $G$ can be interpreted in it (that is, that there is a homomorphism $G \to
G^\ab$), and nothing more.

In exactly the same manner, we can construct the free group over a monoid, the
free $\ZZ/(2)$-algebra over a ring, the free ring over a set or the free
Heyting algebra over a partially ordered set. This is all well-understood; a
particularly perspicuous account in the general setting of partial Horn
theories is due to Erik Palmgren and Steve Vickers <cit.>.

However, this procedure cannot be carried out for any pair of theories. For
instance, there are no free fields. The free field on a set $M$ would be
a field $K$ together with a map $M \to K$ such that any map $M \to L$ into a field $L$ factors
over the given map $M \to K$ by a unique field homomorphism $K \to L$.

For instance, in the case $M = \{ t \}$, the field $\QQ(t)$ of rational
functions comes close, but fails because there are no field homomorphisms $\QQ(t)
\to L$ which could map $t$ to an algebraic element. We could also try to
concoct a term model, but the set of terms in the language of a field extended
by a constant $t$ modulo provable equivalence is only the ring $\ZZ[t]$, not a

The non-existence of free fields is put into perspective by the observation that the
theory of fields is, for any of its variants, not a partial Horn theory.

Free local rings. The theory of local rings, that is the theory of
rings extended by the two coherent axioms

\begin{align*}
1 = 0 &\vdash \bot \\
(\exists z\?R\+ (x+y)z = 1) &\seq{x:R,y:R} (\exists z\?R\+ xz = 1) \vee
(\exists z\?R\+ yz = 1),
\end{align*}

is also not a partial Horn theory. Hence there is no reason to expect that free
local rings exist, and indeed, in general they do not. However, despite this
negative outlook, we want to analyze the situation in more detail.

The correct notion of a morphism between local rings is that of a local
ring homomorphism, a ring homomorphism $f : R \to S$ which reflects
invertibility, that is for which $f(x)$ being invertible implies that $x$ is

Hence a free local ring over a ring $A$ is to be a local ring $A'$
together with a ring homomorphism $A \to A'$ such that the following universal
property holds: Any ring homomorphism $A \to B$ into a local ring uniquely
factors via a local ring homomorphism over $A \to A'$ as indicated in the diagram.

\[ \xymatrix{
A \ar[rd] \ar[rrr] &&& {\substack{\text{local}\\\text{\normalsize$\!\!\!B$}\\\phantom{\text{local}}}} \\
& {\substack{\text{\normalsize$\!\!A'$}\\\text{local}}} \ar@{-->}_[@!31]{\text{local}}[rru]
} \]

To develop intuition for what this universal property requests, let a
homomorphism $f : A \to B$ into a local ring be given. The subset $B^\times
\subseteq B$ is a prime filter, due to the locality of $B$. Its
preimage $\fff \defeq f^{-1}[B^\times]$ is a prime filter of $A$. Hence the
localization $A_\fff = A[\fff^{-1}]$ is a local ring and $f$ factors via the
well-defined map $f' : A_\fff \to B,\,\frac{x}{s} \mapsto f(s)^{-1}f(x)$ over
the localization morphism $A \to A_\fff,\,x \mapsto \frac{x}{1}$. Furthermore,
this map is local.

Hence the stalks $A_\fff$, where $\fff$ ranges over the prime filters of $A$,
can be regarded as approximations to the hypothetical true local ring over $A$.
Each of these stalks is local, but might not validate the universal property
for all homomorphisms $A \to B$ into local rings. We are thus led to the
following conclusions.

* A free local ring $A \to A'$ over $A$ exists if $A$ has exactly one prime
filter. (The converse also holds.) In classical mathematics, this condition is
satisfied if and only if $A$ is local ring of Krull dimension zero. In this
case, the unique prime filter is $A^\times$ and the free local ring over $A$ is given
by $A$ itself. Hence in general, the problem of constructing the free local
ring over a given ring is not solvable.

* However, we could solve the problem in full generality if we would have a
special prime filter $\fff_0$ which could somehow shift shape, that is, turn into any
specific prime filter $\fff$ on demand.

The existence of such a shape-shifting prime filter $\fff_0$ is not a pipe dream.
While it does not exist as a set, it can be realized as a sheaf.

The generic prime filter $\fff_0$ of a ring $A$ is the
generic model of the theory of prime filters of $A$.

According to this definition, the generic prime filter is a particular
sheaf model over the classifying locale of prime filters of $A$, the
spectrum $\Spec(A)$ of $A$. By localizing at the generic prime filter, we solve
the problem of constructing the free local ring in a generalized sense: The
free local ring over $A$ exists as a certain sheaf of rings. It has a
universal property not only with respect to all ordinary rings, but also with respect to all
sheaves of rings on arbitrary locales.

Constructing the sheaf $A^\sim$. We recall from Section <ref> that the given ring $A$
has a simple counterpart in the universe of sheaves over $\Spec(A)$, namely the
constant sheaf $\underline{A}$. We construct the sheaf $A^\sim$ as

\[ A^\sim \defeq \underline{A}[\fff_0^{-1}], \]

that is as the localization of $\underline{A}$ at its prime
filter $\fff_0$.[This description contains a slight abuse of notation.
According to Definition <ref>, the generic prime
filter $\fff_0$ is a model of the theory of prime filters, hence a
family $(U_x)_{x \in A}$ of opens of $\Spec(A)$, one for each nullary relation
symbol of the theory. In fact, by the construction of the generic model, the
open $U_x$ is simply the element $[D(x)]$ of the Lindenbaum algebra. We
turn this family into the subsheaf of $\underline{A}$ given by $U \mapsto \{ g
\in \Hom(U,A) \,|\, \forall x \in A\+ g^{-1}[\{a\}] \preceq [D(a)] \}$. Abusing
notation, we denote this subsheaf also as “$\fff_0$”. The
statement “$\fff_0$ is a prime filter” is then validated by the sheaf semantics.]

With this definition, a number of statements from
Section <ref> are immediate.

Let $A$ be a ring. Then the statements (<ref>), (<ref>) and
(<ref>) displayed above hold:

The ring $A^\sim$ has every property $\varphi$ that $A$ has, assuming
that $\varphi$ is a property of rings which can be put in the formal
higher-order language of toposes; that there is an intuitionistic proof
that $\varphi$ is localization-stable; and that every element of $A$ is
nilpotent or not.

If a geometric sequent holds for $A^\sim$, then it also holds for all
stalks $A_\fff$ at prime filters. The converse holds if $\Spec(A)$ is spatial,
for instance if is available.

(<ref>) The ring $A^\sim$ is local.

(<ref>) The ring $A^\sim$ is local as it is the
localization at a prime filter.

(<ref>) The assumption on $A$ implies that $\Spec(A)$ is
overt. For overt locales, it is a standard fact that any (infinitary)
first-order property of sets passes to the induced constant sheaves. Hence the
claim follows by observing that $A^\sim$ is a localization of $\underline{A}$.

(<ref>) We recall that the points of $\Spec(A)$ are
precisely the prime filters of $A$. The sheaf-theoretic stalk of the constant
sheaf $\underline{A}$ at any point is precisely $A$, and by construction, the
stalk of the generic prime filter $\fff_0$ (considered as a subsheaf
of $\underline{A}$) at a prime filter $\fff$ is $\fff$. Since localization is a
geometric construction, it is preserved by the operation of computing
(sheaf-theoretic) stalks. Hence the stalk of $A^\sim$ at a point $\fff$ is
$A[\fff^{-1}]$, that is, the ring-theoretic stalk of $A$ at $\fff$. The claim
therefore follows from Proposition <ref>.

Furthermore, the sheaf $A^\sim$ is the free local ring over $A$ in the
following sense. If $R$ is a sheaf of rings on a locale $X$ and $S$ is a sheaf
of rings on a locale $Y$, then by a morphism $R \to S$ we mean a pair
consisting of a morphism $f : Y \to X$ of locales together with a
morphism $f^\sharp : f^{-1}R \to S$ of sheaves of rings on $Y$. (The
sheaf $f^{-1}R$ is the pullback sheaf of $R$ along $f$.)
In this way a category of sheaves of rings on arbitrary locales is set up, into
which the category of ordinary rings embeds.

For $A^\sim$ to be the local ring over $A$, there has to be a morphism $A \to
A^\sim$. For this we take the pair $\langle g, g^\sharp \rangle$ where $g :
\Spec(A) \to \pt$ is the unique morphism into the one-point locale
and $g^\sharp : g^{-1}A = \underline{A} \to A^\sim$ is the localization

If $\langle f,f^\sharp \rangle : A \to B$ is a morphism into a local sheaf of
rings on an arbitrary locale $X$, we can construct, in the universe of sheaves
over $X$, the factorization $\underline{A} \to
\underline{A}[\fff^{-1}] \to B$ where $\fff \defeq
(f^\sharp)^{-1}[B^\times]$. Since $\fff$ is a model of the theory of prime
filters of $A$, there is a unique morphism $g : X \to \Spec(A)$ of locales such
that $g^{-1}\fff_0 = \fff$. Since $g^{-1}A^\sim = \underline{A}[\fff^{-1}]$,
the localization just constructed gives rise to a morphism $A^\sim \to B$ of
local sheaves of rings.

There is general topos-theoretic machinery for generalized free
constructions of this kind [89, 90], and
this machinery can be used to construct several kinds of spectra, including the
ordinary spectrum of a ring. However, this machinery does have limitations, and
in particular it cannot be used to construct free fields.

Given a ring $A$, there is the geometric theory of local
localizations of $A$. This is the theory of local rings extended by constants $e_a$
for each element $a \in A$ and the following axioms:

\begin{align*}
\top &\vdash e_0 = 0 \\
\top &\vdash e_1 = 1 \\
\top &\vdash e_{a + b} = e_a + e_b & \text{(for each~$a,b \in A$)} \\
\top &\vdash e_{ab} = e_a e_b & \text{(for each~$a,b \in A$)} \\
\top &\vdash e_{-a} = -e_a & \text{(for each~$a \in A$)} \\
\top &\vdash_{x:R} \bigvee_{a \in A} \bigvee_{s \in A} \bigl((\exists z\?R\+
e_s z = 1) \wedge e_s x = e_a\bigr) \\
e_a = 0 &\vdash \bigvee_{\substack{s \in A\\sa = 0}} (\exists z\?R\+ e_s z = 1) & \text{(for each~$a \in A$)}
\end{align*}

By the first five listed entries, a model $R$ of this theory comes equipped
with a ring homomorphism $f : A \to R$. The remaining two entries ensure that $R$ is
a localization of $A$, more precisely that it is the localization of $A$
at $f^{-1}R^\times$.

Since this theory is not propositional, Section <ref>
does not apply. There is, however, still a classifying topos of this theory, and it turns
out that it coincides with the topos of sheaves over $\Spec(A)$ – mainly
because the theory of local localizations of $A$ is equivalent to the theory of
prime filters of $A$. Under this identification, the generic model of the local
localization is precisely the sheaf $A^\sim$, and it validates first-order
sequents not expected from a local localization; as repeatedly stressed
(statement (<ref>)), it is a field, even though the theory of local
localizations does not prove the field condition.

§.§ Understanding the sheaf model

In Section <ref>, we constructed the sheaf $A^\sim$ as the free
local ring over $A$, more specifically as the localization of the constant
sheaf $\underline{A}$ on $\Spec(A)$ at the generic prime filter $\fff_0$
of $A$. Several of the properties mentioned in
Section <ref> are immediate consequences of this
abstract description.

However, for a more detailed identification of $A^\sim$ – especially for
verifying its field property – we require a more concrete description. In
particular, we require a concrete description of the underlying frame
of $\Spec(A)$. Since this frame is defined as the Lindenbaum algebra of the
theory of prime filters of $A$, we need a thorough grasp of the set of sequents proved by
this theory.

Such an understanding is imparted by the following theorem. It is the
central workhorse of our approach.

Let $A$ be a ring. The Lindenbaum algebra of the theory $\TT$ of prime filters
of $A$ is canonically isomorphic to the frame of radical ideals in $A$, via an
isomorphism which maps

\[ [D(f)] \longmapsto \sqrt{(f)}. \]

In particular:

\[
\textnormal{$\TT$ proves~$D(f) \vdash \bigvee_{i \in I} D(g_i)$} \quad\text{iff}\quad
f \in \sqrt{(g_i)_i}. \]

The set of radical ideals $\Rad(A)$ is ordered by inclusion. Its
least element is $\sqrt{(0)}$, the meet $\aaa \wedge \bbb$ of two radical
ideals is their intersection and the join $\bigvee_i \aaa_i$ of radical ideals
is $\sqrt{\sum_i \aaa_i}$. In this way the radical ideals form a frame.

The Lindenbaum algebra of $\TT$ is the free frame generated by the symbols $D(x)$,
where $x$ ranges over the elements of $A$, modulo the axioms for a prime
filter. Hence to give a frame homomorphism $\OOO(\Spec(A)) \to \Rad(A)$, we need
to specify images in $\Rad(A)$ for each generator in such a way that the
axioms for a prime filter are satisfied. This is achieved by declaring $D(f)
\mapsto \sqrt{(f)}$:

\begin{align*}
D(0) &\vdash \bot & \sqrt{(0)} &\subseteq \sqrt{(0)} \\
D(f+g) &\vdash D(f) \vee D(g) & \sqrt{(f+g)} &\subseteq\textstyle \sqrt{\sqrt{(f)} + \sqrt{(g)}} \\
\top &\vdash D(1) & \sqrt{(1)} &\subseteq \sqrt{(1)} \\
D(f) \wedge D(g) \dashv\!&\vdash D(fg) & \sqrt{(f)} \cap \sqrt{(g)} &= \sqrt{(fg)}
\end{align*}

The most interesting of these radical inclusions is probably $\sqrt{(f)} \cap
\sqrt{(g)} \subseteq \sqrt{(fg)}$, as this inclusion illustrates why passing to the
radical is vital; in general, we do not have $(f) \cap (g) \subseteq (fg)$.

The frame homomorphism obtained in this manner is surjective, since a preimage
for a radical ideal $\aaa$ is given by $\bigvee_{f \in \aaa} [D(f)]$. By
Exercise <ref>, it
remains to show that the homomorphism reflects the ordering.

To this end, let an element $f \in A$ and a family $(g_i)_{i \in I}$ of elements be
given and assume $\sqrt{(f)} \subseteq \sqrt{\sum_i \sqrt{(g_i)}}$. Then there
are values $n,m \in \NN$, $i_1,\ldots,i_m \in I$ and $u_1,\ldots,u_m \in
A$ such that $f^n = u_1 g_{i_1} + \cdots + u_m g_{i_m}$. We then have the
following chain of entailments.

\[
D(f) \vdash
D(f^n) \vdash
\bigvee_{k=1}^m D(u_k g_{i_k}) \vdash
\bigvee_{k=1}^m D(g_{i_k}) \vdash
\bigvee_i D(g_i). \qedhere
\]

Theorem <ref> shows that any derivation in the theory of prime
filters of $A$ can be put into a normal form. An expression of the
form “$f^n = u_1 g_{i_1} + \cdots + u_m g_{i_m}$” can be regarded as an
algebraic certificate of the entailment $D(f) \vdash \bigvee_i D(g_i)$.

An immediate corollary of Theorem <ref> is
that $\Spec(A)$ is compact, since if $f \in \sqrt{(g_i)_i}$ then also $f \in
\sqrt{(g_{i_1},\ldots,g_{i_m})}$ for suitable indices $i_1,\ldots,i_m$.
However, the stronger result that $\Spec(A)$ is
even a coherent locale can also be deduced from a general theorem
since the theory of prime filters is a coherent theory
(Exercise <ref>).

A further corollary of Theorem <ref> is that the theory of prime
filters of $A$ is inconsistent (that it, that it proves the sequent $\top
\vdash \bot$, which can also be written as $D(1) \vdash D(0)$) if and only
if $A$ is the trivial ring. Contrapositively, if $A$ is not the trivial ring,
then the theory is consistent. This observation can be regarded as a finitary
substitute of the statement (equivalent to in general) “nontrivial rings contain prime filters”.

Given the importance of Theorem <ref>, it is
natural to wonder where the proof stems from. Our proof proceeded in an ad hoc
fashion, verifying that the frame of radical ideals has the required properties
– but where does the idea to use radical ideals come from? In general, determining the set
of provable sequents of a geometric theory is a challenging problem. Our most
efficient tool is probably the theory of entailment relations. We refer
to Refs. rinaldi-schuster-wessel:edde,cederquist-coquand:entrel and
the references therein and also strongly recommend the literature on dynamical
methods in commutative
algebra coste-lombardi-roy:dynamical-method,coquand-lombardi:logical-approach,coquand:site.

Having identified the underlying frame of $\Spec(A)$, the second workhorse is
an explicit description of the sheaf $A^\sim$.

Let $A$ be a ring. For any $f \in A$, there is a canonical isomorphism

\[ A[f^{-1}] \longrightarrow A^\sim([D(f)]). \]

In particular, for $f = 1$, we obtain statement (<ref>) from
Section <ref>.

For $f \in A$, we set $S_f \defeq \{ g \in A \,|\, \exists n \in
\NN\+ \exists u \in A\+ f^n = ug \} \subseteq A$. This multiplicative system is
the saturation of $\{ f^0, f^1, \ldots \}$. The localization $A[S_f^{-1}]$
is canonically isomorphic to $A[f^{-1}]$, but has the advantage that for
elements $f,g \in A$ such that $\sqrt{(f)} = \sqrt{(g)}$, the
rings $A[S_f^{-1}]$ and $A[S_g^{-1}]$ are actually the same
while $A[f^{-1}]$ and $A[g^{-1}]$ are merely canonically isomorphic. This
property eases formalization in set theory; it is otherwise not important.

On the basis of $\Spec(A)$ given by the opens of the form $[D(f)]$, we define a partial
presheaf by

\[ [D(f)] \longmapsto A[S_f^{-1}]. \]

This partial presheaf is, on the basis where it is defined, a sheaf. Unraveling
the definitions, this claim boils down to the following basic result in
commutative algebra:
Let $B$ be a ring. Let $1 = f_1 + \cdots + f_m \in B$ be a partition of unity. Let
elements $s_i \in B[f_i^{-1}]$ be given. Assume that $s_j = s_k$
in $B[(f_jf_k)^{-1}]$ for all pairs of indices. Then there is exactly one
element $s \in B$ such that, for all indices $i$, $s = s_i$ in $B[f_i^{-1}]$.

The remainder of the argument is by sheaf-theoretic generalities.

More generally, for any $A$-module $M$, we can construct the
localization $M^\sim \defeq \underline{M}[\fff_0^{-1}]$. In the special case
that $M$ is $A$, this definition coincides with our original definition
of $A^\sim$. The proof of Proposition <ref> carries over to
show that $M^\sim([D(f)]) \cong M[f^{-1}]$.

An elementary reformulation.
As a corollary of Theorem <ref> and
Proposition <ref>, we can unwind the definitions to recast
the sheaf semantics in entirely explicit algebraic terms, with no locales or
sheaves in sight. Notwithstanding the impredicative nature of locale theory,
the resulting formulation will even make sense in metatheories without a
powerset operation such as czf [91, 92] or arithmetic
universes [34, 35]. In
fact, it is then a purely syntactic translation procedure which can be carried
out within pra.

The approach using locales and sheaves provides two ingredients which go beyond
mere syntax: Firstly, they give motivation for setting up the semantics in
the way we do (Section <ref>). Secondly, they
conceptualize $A^\sim$ as a single entity, just as rings like $A/\mmm$
or $A_\ppp$ are single entities; nevertheless, after unrolling the definitions,
any statement about $A^\sim$ is merely a (logically more complex) statement
about $A$ and its localizations $A[f^{-1}]$.

By a formula over a ring element $f \in A$, we mean a
first-order formula over the signature which has

* a sort “$A^\sim$” and function symbols for the structure of a ring,

* for each $A$-module $M$, a sort “$M^\sim$” and function symbols for the
structure of an $A^\sim$-module,

* for each linear map $M \to N$, a function symbol $M^\sim \to N^\sim$,

* a constant of sort $A^\sim$ for each element of $A[f^{-1}]$ and

* for any $A$-module $M$, a constant of sort $M^\sim$ for each element of $M[f^{-1}]$.

Let $A$ be a ring. Let $\varphi$ be a formula over $f \in A$.
Then $[D(f)] \models \varphi$ in the sense of Table <ref> if and only
if $f \models \varphi$ in the sense of Table <ref>.

Induction on the structure of $\varphi$, harnessing the explicit
descriptions provided by Theorem <ref> and
Proposition <ref>.

A purely algebraic presentation of the sheaf semantics of $\Spec(A)$
$f \models \top$    iff    true

$f \models \bot$    iff    $f$ is nilpotent

$f \models x =_{M^\sim} y$    iff    $x = y \in M[f^{-1}]$

$f \models \varphi \wedge \psi$    iff
$f \models \varphi$ and $f \models \psi$

$f \models \varphi \vee \psi$    iff
there exists a partition $f^n = fg_1 + \cdots + fg_m$ such that,

for each $i$, $fg_i \models \varphi$ or $fg_i \models \psi$

$f \models \varphi \Rightarrow \psi$    iff
for all $g \in A$, $fg \models \varphi$ implies $fg \models \psi$

$f \models \forall x\?A^\sim\+ \varphi(x)$    iff
for all $g \in A$ and all $x_0 \in A[(fg)^{-1}]$, $fg \models \varphi(x_0)$

$f \models \exists x\?A^\sim\+ \varphi(x)$    iff
there exists a partition $f^n = fg_1 + \cdots + fg_m$ such that,

for each $i$, $fg_i \models \varphi(x_0)$ for some $x_0 \in A[(fg_i)^{-1}]$

The analogue of Theorem <ref> for the new
formulation of the sheaf semantics reads as follows.

Let $A$ be a ring. Let $f \in A$. Let $\varphi$ be a formula over $f$.

* Let $g \in A$. If $f \models \varphi$, then $fg \models \varphi$.

* Let $f^n = fg_1 + \cdots + fg_m$. If $fg_i \models \varphi$ for all
indices $i$, then $f \models \varphi$.

* Let $\psi$ be a further formula over $f$. If $f \models
\varphi$ and if $\varphi$ entails $\psi$ intuitionistically, then also $f
\models \psi$.

Combination of Theorem <ref>
and Corollary <ref>, or alternatively direct proof
by induction without using any preliminaries from earlier sections of this

The field property. We are now in a position to verify
statement (<ref>) of Section <ref>.

Let $A$ be a reduced ring. Then $A^\sim$ is a field in that

\[ 1 \models \forall x\?A^\sim\+ \bigl((\neg(\exists y\?A^\sim\+ xy = 1)) \Rightarrow
x = 0\bigr). \]

By Table <ref>, we have to verify the
following claim.

For any element $f \in A$ and any element $x \in A[f^{-1}]$,

${\qquad}$ for any element $g \in A$,

${\qquad\qquad}$ if for any element $h \in A$,

${\qquad\qquad\qquad}$ if there is $(fgh)^n = \sum_{i=1}^m fghp_i$
such that for each $i$,

${\qquad\qquad\qquad\qquad}$ there exists $y \in
A[(fghp_i)^{-1}]$ such that

${\qquad\qquad\qquad\qquad\qquad}$ $xy = 1$ in $A[(fghp_i)^{-1}]$,

${\qquad\qquad\qquad}$ then $fgh$ is nilpotent,

${\qquad\qquad}$ then $x = 0$ in $A[(fg)^{-1}]$.

Hence let elements $f \in A$, $x \in A[f^{-1}]$ and $g \in A$ be given and
assume that for any $h \in A$, the displayed condition holds. We are to show
that $x = 0$ in $A[(fg)^{-1}]$.

Write $x = \frac{x'}{f}$. For $h \defeq x'$, we have the
partition $(fgh)^1 = fgh \cdot 1$ with $m = 1$ and $p_1 = 1$. For $y \defeq
\frac{f}{x'} = \frac{f^2gp_1}{fghp_1}$, we have $xy = 1$ in $A[(fghp_1)^{-1}]$.
By assumption, the element $fgh$ is nilpotent, hence zero. Thus $x' = 0$
in $A[(fg)^{-1}]$. This implies that $x = 0$ in $A[(fg)^{-1}]$.

The proof of Proposition <ref> visibly demonstrates that
unwinding the definition of the sheaf semantics quickly results in formulas
which are quite convoluted. This behavior is a basic consequence of the fact
that, with the exception of the clauses for “$\top$” and “$\wedge$”, all
clauses in Table <ref> introduce additional

This increase in complexity should be properly appreciated: The sheaf semantics
allows us to harness convoluted properties in simple language. The unrolled
monstrosity in the proof of Proposition <ref> is not
memorable at all and unlikely to find its way into human-written proofs.
However, in the form “$A^\sim$ is a field”, it becomes easily accessible.
This state of affairs becomes the more pronounced the more negations and especially
double negations occur in the proof.

For future reference, and also for giving a different
perspective on statement (<ref>), we unroll here the
interpretation of $f \models \neg\neg\varphi$. It is:

For any element $g \in A$,

${\qquad}$ if for any element $h \in A$,

${\qquad\qquad}$ if $fgh \models \varphi$,

${\qquad\qquad}$ then $fgh$ is nilpotent,

${\qquad}$ then $fg$ is nilpotent.

In the case that $A$ is reduced and $f$ is the unit element of $A$, this
condition implies (by setting $g \defeq 1$): “If $h = 0$ is the only element of $A$
such that $h \models \varphi$, then $1 = 0$ in $A$.”

§.§ Evaluating test cases

Size of injective and surjective matrices.

On page par:appl-constr-alg, we presented a classical proof of the
following theorem.
Theorem. Let $M$ be an injective matrix with more columns than rows
over a reduced ring $A$. Then $1 = 0$ in $A$.

We are now in a position to show how the reduction technique developed in
Section <ref> can be used to recast the classical proof so that it
becomes constructive:

Proof. Since localization is exact, the matrix $M$ is also injective when
considered as a matrix over $A^\sim$ (statement (<ref>)).
Since $A^\sim$ is a field, this is a contradiction to basic (intuitionistic)
linear algebra.[We are referencing the following theorem: “Let $M$ be
an injective matrix with more columns than rows over a field $k$ in the sense
that any element of $k$ is either zero or invertible. Then $\bot$.” This
theorem is proven by repeatedly applying elementary row and column
transformations until the matrix is of the
form $\left(\begin{smallmatrix}I&0\\0&0\end{smallmatrix}\right)$. By assumption
on the size of $M$, there is at least one zero column. This contradicts

However, since the ring $A^\sim$ is only a field in the weaker sense that
nonunits are zero, this theorem does not apply directly. We only have that any
element of $A^\sim$ is zero or invertible. We hence employ the
trick described in the section on double negation stability
(page par:double-negation-stability).]
In other words, $1 \models \bot$. By
Remark <ref> or Table <ref>, this amounts to $1 = 0$ in $A$.

If desired, the proof can be mechanically unwound to a fully explicit proof
which does not refer to the sheaf semantics. In this case, unwinding yields
exactly the proof by Fred Richman <cit.> (only
that he needs one additional paragraph to deal with the possibility that the
ring is not reduced, which we for conciseness simply assumed):

Proof. Over the localized
ring $A[M_{ij}^{-1}]$, the matrix element $M_{ij}$ is invertible and hence $M$ can be
put into the form $\left(\begin{smallmatrix}1&0\\0&M'\end{smallmatrix}\right)$
by elementary row and column transformations. The matrix $M'$ is injective and
has more columns than rows, hence by induction, applied to this submatrix
over $A[M_{ij}^{-1}]$, we have $1 = 0$ in $A[M_{ij}^{-1}]$. Since $A$ is
reduced, this amounts to $M_{ij} = 0$ in $A$.

Hence $M$ is the zero matrix. Thus $M(1,0,\ldots,0)^t = 0$ and by
injectivity $1 = 0$ in $A$.

In exactly the same fashion, the dual statement about surjective matrices can
be proven.

Concluding, one can well ask what the computational content of the equation $1
= 0$ is. The answer depends on the ring in question. In rings where we know a
priori that $1 \neq 0$, the two statements are most useful in their
contrapositive form. But in rings of the form $R[f^{-1}]$ or $R/(f)$, learning
that $1 = 0$ can indeed be useful: In the former case, this tells us that $f$
is nilpotent (and a computational witness of $1 = 0$ can be transformed into a
number $n$ such that $f^n = 0$), and in the latter case, this tells us that $f$
is invertible.

Grothendieck's generic freeness lemma. This theorem is a basic
theorem in algebraic geometry, used for instance for developing the theory of
moduli spaces. When phrased for the affine situation in a constructively
sensible way, a simple version of this theorem reads as follows. We recall
from Section <ref> that
the notation $M[f^{-1}]$ makes sense for any element $f \in A$; in case $f$ is
zero or nilpotent, the localized module $M[f^{-1}]$ will be the trivial module.
Let $A$ be a reduced ring. Let $M$ be a finitely generated $A$-module.
If $f = 0$ is the only element of $A$ such that $M[f^{-1}]$ is a
free $A[f^{-1}]$-module, then $1 = 0$ in $A$.

This theorem is particularly interesting for the program of constructivizing
classical commutative algebra, as it is an example where the constructive proof
is much shorter and arguably more perspiciuous than classical proofs (for which
see for instance Refs. <cit.>,
<cit.> or
<cit.>, which only cover the case of
Noetherian integral domains, or Refs. staats:generic-freeness,
which proceed in a series of intermediate steps, reducing to that case).
Proof. By Example <ref> and
Exercise <ref>(<ref>), the claim amounts to the statement that $M^\sim$ is free. Since $A^\sim$ is a field, this statement follows from
basic (intuitionistic) linear algebra.[A standard result of linear
algebra is: “Any finitely generated vector space over a field is finite free
(that is, has a finite basis).” The proof proceeds by considering a given
generating family and using the law of excluded middle to determine whether one
of the generators can be expressed using the others or not. In the latter case,
the family is linearly independent and hence a basis; in the former case, the
proof removes the redundant generator and continues by induction.

Intuitionistically, we only have the double negation of the law of excluded
middle available; this is why intuitionistically we only have that finitely
generated vector spaces are finite free. The field condition required
by the proof is exactly the one satisfied by $A^\sim$.]
Again, the proof can be unwound if
desired <cit.>:

We proceed by induction on the length of a given generating family
of $M$. Let $M$ be generated by $(v_1,\ldots,v_m)$.

We show that the family $(v_1,\ldots,v_m)$ is linearly independent. Let $\sum_i
a_i v_i = 0$. Over $A[a_i^{-1}]$, the vector $v_i \in M[a_i^{-1}]$ is a linear
combination of the other generators. Thus $M[a_i^{-1}]$ can be generated as
an $A[a_i^{-1}]$-module by fewer than $m$ generators. The induction hypothesis,
applied to this module over $A[a_i^{-1}]$, yields that $1 = 0$ in $A[a_i^{-1}]$. Since $A$ is
reduced, this amounts to $a_i = 0$.

We finish by using the assumption for $f = 1$.
The full version of Grothendieck's generic freeness lemma, and a constructive
proof of it, read as follows.
Let $A$ be a reduced ring. Let $B$ be an $A$-algebra of finite type. Let $M$ be
a finitely generated $B$-module.
If $f = 0$ is the only element of $A$ such that

* $B[f^{-1}]$ and $M[f^{-1}]$ are free modules over $A[f^{-1}]$,

* $A[f^{-1}] \to B[f^{-1}]$ is of finite presentation and

* $M[f^{-1}]$ is finitely presented as a module over $B[f^{-1}]$,

then $1 = 0$ in $A$.

Proof. One can check that the claim is the interpretation by the sheaf
semantics of the following statement about the sheaves: It is the case that

* $B^\sim$ and $M^\sim$ are free modules over $A^\sim$,

* $A^\sim \to B^\sim$ is of finite presentation, and

* $M^\sim$ is finitely presented as a module over $B^\sim$,

Item (1) is by basic linear algebra as in the proof of
simple version of Grothendieck's generic freeness lemma, but a bit more involved as we now need to
deal with countable generating
families <cit.>. Item (2) is because finitely
generated algebras over anonymously Noetherian rings are finitely
presented (in a description of the form $R[X_1,\ldots,X_n]/\aaa$, the
ideal $\aaa$ is finitely generated).
Item (3) is because finitely generated modules over anonymously Noetherian are
finitely presented.
A variant of this proof where the reference to the Noetherian condition has
been replaced by an explicit computation has been unwound in
Ref. blechschmidt:generic-freeness.

McCoy's theorem.
It is a familiar fact from linear algebra that an injective $(n \times
m)$-matrix $M$ over a geometric field has at least one invertible $m$-minor.
Like many proofs in linear algebra, the proof proceeds by first applying
elementary row and column transformations to put $M$ into the form $N \defeq
\left(\begin{smallmatrix}I&0\\0&M'\end{smallmatrix}\right)$ where all entries
in the submatrix $M'$ are zero. This step exploits
that any element is zero or invertible. Since $M$ is injective, the number of columns of $M'$ is zero.
Hence $N = \left(\begin{smallmatrix}I\\0\end{smallmatrix}\right)$ has an
invertible $m$-minor, and thus $M$ has well.

A version of McCoy's theorem states that this fact
generalizes to arbitrary rings:

Theorem. Let $M \in A^{n \times m}$ be an injective matrix.
Then $(\Lambda^m M)$, the ideal of $m$-minors of $M$, is regular.

The sheaf-theoretic reduction technique allows us to give a constructive proof
of McCoy's theorem which is close to the linear algebra proof. In case that the
ring $A$ is reduced, we can even copy the original proof almost word for word;
for the general case, we require the following lemma.

Lemma. Let $M \in A^{n \times m}$ be an injective matrix with $m > 0$. Assume that all entries
of $M$ are nilpotent. Then $1 = 0$ in $A$.

Proof of the lemma. Let $(M)$ be the ideal generated by the entries
of $M$. The assumption implies that there is a exponent $K \in \NN$ such that $(M)^K = (0)$.
If $K \geq 1$, then also $(M)^{K-1} = (0)$, since for $x \in (M)^{K-1}$ the
entries of $M (x,0,\ldots,0)^t$ are elements of $(M)^K$, hence zero,
and $M$ is injective. We may thus assume $K = 0$. So $1 \in (M)^0 = (0)$.
Because we want to work in the generality of
a ring which might not be reduced, we cannot use that $A^\sim$ is a field.
Instead we will employ the generalization established in
Exercise <ref>: Any nonunit of $A^\sim$ is nilpotent. The
proof then proceeds as follows.
Proof of the theorem. Let $x \in A$ be such that $x (\Lambda^m M) = (0)$. We are to
show $x = 0$. By passing to the factor ring $A/\ann(x)$, we may
assume $(\Lambda^m M) = (0)$ and $x = 1$; the new goal is to verify $1 = 0$. We
do this by validating $\bot$ in the sheaf semantics.

We may employ the law of excluded middle a finite number of times because we
are to verify $\bot$. By repeatedly exploiting that any matrix entry is
invertible or not, we may use row and column transformations to put $M$ into
the form $N \defeq \left(\begin{smallmatrix}I&0\\0&M'\end{smallmatrix}\right)$ where all
entries of $M'$ are not invertible. Since nonunits of $A^\sim$ are nilpotent, the entries of $M'$ are
nilpotent, and since $M'$ is injective and since $1 \neq 0$, the preceding lemma
shows that the number of columns of $M'$ is zero.

Hence $N = \left(\begin{smallmatrix}I\\0\end{smallmatrix}\right)$ and $(1) =
(\Lambda^m N) = (\Lambda^m M) = (0)$, a contradiction.

Not of pragmatic, but of logical interest is that the proof can
also be recast as follows. Instead of reducing to the factor ring $A/\ann(x)$,
we continue considering $A$. Working under the sheaf semantics, we then
introduce a variant of the usual negation $\neg\varphi \equiv (\varphi
\Rightarrow \bot)$, namely $\negg\varphi \equiv (\varphi \Rightarrow x = 0)$.
We may still use the law of excluded middle for this new negation and hence
exploit that any element $f$ of $A^\sim$ is invertible or “not” invertible. By
Exercise <ref>, this amounts to saying that some power
of $f$ annihilates $x$. The remainder of the proof carries over with minor

As with the other examples, the proof can mechanically be unwound to obtain a proof
which is fully explicit:

Proof of the theorem. Let $x \in A$ be such that $x (\Lambda^m M) = (0)$. We are to
show $x = 0$. By passing to the factor ring $A/\ann(x)$, we may
assume $(\Lambda^m M) = (0)$ and $x = 1$; the new goal is to verify $1 = 0$.

If $m = 0$, the claim is immediate because in this case $(1) = (\Lambda^m M) =
(0)$. So assume $m > 0$.

Over the localized ring $A[M_{ij}^{-1}]$, the matrix entry $M_{ij}$ is
invertible and hence $M$ can be put into the
form $\left(\begin{smallmatrix}1&0\\0&M'\end{smallmatrix}\right)$ by elementary
row and column transformations. The matrix $M'$ is still injective,
and $(\Lambda^{m-1} M') = (\Lambda^m M)$, hence we may assume by induction
that $1 = 0$ in $A[M_{ij}^{-1}]$.

Hence all entries of $M$ are nilpotent and the claim follows from the preceding

Other short and explicit proofs of McCoy's theorem are given in
Refs. blocki:mccoy,
<cit.> and
<cit.>. The proof in
Ref. <cit.> employs the law of excluded
middle. We were not able to discern that these proofs are just different
presentations of the same idea that ours is based on; these proofs all employ
computations with Cramer-like formulas, while our proof stresses the similarity
to the field case.

It is on purpose that the (sheaf-theoretic version of) our proof contains case
distinctions, to closely mimic the proof in the field case. It is also
possible to do without, as already our unrolled proof demonstrates. Thierry
Coquand and Claude Quitté gave a beautiful proof without case distinctions by
applying a local–global
principle <cit.>;
if desired, their proof can also be cast in the sheaf-theoretic framework
(Exercise <ref>).

§.§ Exercises

[Noetherian properties of the integers]

* Show that the law of excluded middle holds if the ring $\ZZ$ of integers
is Noetherian in the sense that any ideal is finitely generated.

Hint. For a truth value $\varphi$, consider the ideal $\{ x
\in \ZZ \,|\, x = 0 \vee \varphi \}$.

* Give an example of a space $X$ and a subsheaf $F$ of the constant
sheaf $\underline{\ZZ}$ such that, under the sheaf semantics, the subsheaf $F$
is an ideal, and such that it is not the case that, again under the sheaf
semantics, the ideal $F$ is finitely generated.

* Give a proof that $\ZZ$ is anonymously Noetherian which, unlike the proof
given in Example <ref>, uses the anonymous version of the least
number principle of Exercise <ref>.

[Free fields]

* A free field over a set $M$ would be
a field $K$ together with a map $M \to K$ such that any map $M \to L$ into a
field $L$ factors
over the given map $M \to K$ by a unique field homomorphism $K \to L$. Prove
that free fields exist for no set $M$.

* Let $k$ be a field. Devise a notion of
free $k$-fields (where a $k$-field is a field together with a
homomorphism from $k$) and show that the only set $M$ such that there is a
free $k$-field over $M$ is the empty set.

[Nontriviality of $\boldsymbol{A^\sim}$]
Let $A$ be a ring. In Proposition <ref>, we gave an
abstract proof that $A^\sim$ is (local and hence) nontrivial in the sense that $1
\neq 0$. This proof did not need to assume that $A$ itself is nontrivial. Give a new proof of this
fact, by verifying directly $1 \models \neg(1 =_{A^\sim} 0)$ using the
semantics given in Table <ref>.

[A generalization of the field property]

Let $A$ be a ring. We extend the sheaf semantics to infinitary first-order
formulas by adding the following clauses to
Table <ref>:

$f \models \bigwedge_{k \in K} \varphi_k$    iff
for all indices $k \in K$, $f \models \varphi_k$

$f \models \bigvee_{k \in K} \varphi_k$    iff
there exists a partition $f^n = fg_1 + \cdots + fg_m$ such that,

for each $i$, there is an index $k \in K$ such that $fg_i \models \varphi_k$

Theorem <ref>
also applies to this extension, and moreover, this extension in sound with
respect to infinitary intuitionistic logic.

* Prove that:

\[ 1 \models \forall f\?A^\sim\+ \forall x\?A^\sim\+
\bigl((\exists z\?A^\sim\+ fz = 1) \Rightarrow x = 0\bigr) \Longrightarrow \bigvee_{n \in \NN} (f^n x = 0). \]

* Deduce that $A^\sim$ is “almost a field” in the sense that any nonunit
is nilpotent.

* Show that $A$ is reduced iff $A^\sim$ is.

[A local–global principle]

Let $A$ be a ring. We introduce an operator $\nabla$ by

\[ \nabla\varphi \defeqv \bigl(\forall s\?A^\sim\+ ((\varphi \Rightarrow s = 0)
\Rightarrow s = 0\bigr).\]

* Verify that $\nabla$ is a local operator, that is that

\[ (\varphi \Rightarrow \nabla\varphi), \quad
(\nabla\nabla\varphi \Rightarrow \nabla\varphi) \quad\text{and}\quad
((\nabla\varphi \wedge \nabla\psi) \Leftrightarrow \nabla(\varphi \wedge \psi))
\]

hold under the sheaf semantics.

* Show that equality is $\nabla$-stable in that

\[ 1 \models \forall x\?A^\sim\+ \forall y\?A^\sim\+ \nabla(x = y) \Rightarrow x = y. \]

Note. If $A$ is reduced, then $\nabla$ coincides
with $\neg\neg$ and the claim reduces to statement (<ref>)
on page item:negneg-stable. In general, the operator $\nabla$ is
related to the notion of scheme-theoretic dense open
subsets <cit.>.

* Verify that an element of $A^\sim$ is regular iff it
is $\nabla$-invertible, that is:

\[ 1 \models \forall f\?A^\sim\+
\bigl(
(\forall s\?A^\sim\+ fs = 0 \Rightarrow s = 0) \Longleftrightarrow
\nabla(\exists g\?A^\sim\+ fg = 1)
\bigr)
\]

* Verify the analogous statement for finitely generated ideals:

\begin{multline*}1 \models \forall f_1\?A^\sim\+ \ldots \forall f_n\?A^\sim\+ \\
\bigl(
(\forall s\?A^\sim\+ (\textstyle\bigwedge_{i=1}^n f_is = 0) \Rightarrow s = 0) \Longleftrightarrow
\nabla(1 \in (f_1,\ldots,f_n))
\bigr) \end{multline*}

* Explain how the local–global principle “if $(f_1,\ldots,f_n)$ is a
regular ideal and if an ideal $(g_1,\ldots,g_m)$ is regular when considered
over each localization $A[f_i^{-1}]$, then $(g_1,\ldots,g_m)$ is regular
over $A$” can be viewed as an instance of modus ponens for local operators
($(\nabla\varphi \wedge (\varphi \Rightarrow \nabla\psi)) \Longrightarrow
\nabla\psi$).

* Fill in the details, unwind the following proof of McCoy's theorem
(page par:mccoy) and compare the result with the proof in
Ref. <cit.>.

Theorem. Let $M \in A^{n \times m}$ be an injective matrix.
Then $(\Lambda^m M)$, the ideal of $m$-minors of $M$, is regular.

Proof. We verify that, under $\nabla$, there exists an
invertible $m$-minor, that is we verify $\nabla(\bigvee_f (\exists g\?A^\sim\+
fg=1))$, where the disjunction is over the $m$-minors of $M$.

Since $M$ is injective, the ideal generated by the first column is regular,
hence under $\nabla$ the unit ideal. Since our goal is $\nabla$-stable, we may assume
that it actually is the unit ideal. Hence one of the entries in the first
column is invertible. Applying elementary row and column transformations, we
can put $M$ into the
form $\left(\begin{smallmatrix}1&0\\0&M'\end{smallmatrix}\right)$. Continuing
in this fashion, we obtain the
form $\left(\begin{smallmatrix}I\\0\end{smallmatrix}\right)$. This matrix
obviously has an invertible $m$-minor, and hence the original one has one as

[Bridging modules and their induced sheaves]

Let $M$ be a module over a ring $A$.

* Show that $M$ is finitely generated iff $M^\sim$ is.

*  Show that $M$ is finite locally free (that is, that there is a
partition $1 = f_1 + \cdots + f_n$ such that each module $M[f_i^{-1}]$ is
finite free over $A[f_i^{-1}]$) iff $M^\sim$ is finite free.

* Show that $M$ is finitely presented iff $M^\sim$ is.

[Local injectivity and surjectivity]
Let $M$ and $N$ be modules over a ring $A$. Let $f : M \to N$ be a linear map.

* Show that $f$ is injective iff $f^\sim : M^\sim \to N^\sim$ is injective.

* Show that $f$ is surjective iff $f^\sim : M^\sim \to N^\sim$ is surjective.

[Units of the sheaf model]
Let $A$ be a ring. Let $f \in A$. Let $x \in A[f^{-1}]$. Show using
Exercise <ref> that $f \models \exists y\?A^\sim\+ xy
= 1$ if and only if $x$ is invertible in $A[f^{-1}]$.

[Decidability of invertibility]
Show that it is not the case that any element of $\ZZ^\sim$ is invertible or
not invertible.

Note. Since $\ZZ^\sim$ is a (sheaf) model of the
theory of local rings, this observation shows that the theory of
local rings does not prove that invertibility is decidable. Using much the same
technique, this result has also been proven by Thierry
Coquand [103].

More generally, one can show: A ring $A$ is of Krull dimension $\leq n$
iff $A^\sim$ is; and a local ring (such as $A^\sim$) is of Krull
dimension $\leq 0$ iff any element is invertible or nilpotent. Hence
invertibility of elements of $A^\sim$ is decidable iff $A$ is of Krull
dimension $\leq 0$. In this case, up to a technical condition, the universe of
sheaves over $\Spec(A)$ is classical, hence any statement whatsoever is
decidable. The ring controls the logic: Assuming that the metatheory is
classical and assuming the technical condition, the universe of sheaves
over $\Spec(A)$ is governed by classical logic iff $A^\sim$ is of Krull
dimension $\leq 0$.

The for these purposes correct constructive notion of Krull dimension can be
found in Refs. coquand-ducos-lombardi-quitte:krull-integral,coquand-lombardi-roy:char-krull.
It has been used to give a short and constructive proof that $\dim
k[X_1,\ldots,X_n] = n$, where $k$ is a geometric
field [106]. Proofs of the stated
relation between the dimension of $A$ and the dimension of $A^\sim$ are recorded in
Ref. <cit.>.

[Triviality of the spectrum]
Let $A$ be a ring. Verify, without assuming , that $\Spec(A)$ is
isomorphic to the one-point locale iff any element of $A$ is either
invertible or nilpotent.

Hint. Use the description of the unique map $\OOO(\pt) \to
\OOO(\Spec(A)),\,\varphi \mapsto \bigvee\{\top\,|\,\varphi\}$ computed in
part (<ref>) of Exercise <ref>.

[Locality of the spectrum]
Let $A$ be a ring. Show that the spectrum of $A$ is local in the sense of
Exercise <ref> if and only if $A$ is local as a ring.

[Spatiality of the spectrum]
Let $A$ be a ring.

* Verify that $\Spec(A)$ is spatial if and only if for any element $x \in
A$ and any ideal $\aaa \subseteq A$,

\[ x \in \sqrt{\aaa} \quad\textnormal{if}\quad
\text{for all prime filters~$\fff \subseteq A$ with~$x \in \fff$, $\fff \between \aaa$}, \]

where the symbol “$\between$” denotes that the two sets have an element in common.

* Assuming the law of excluded middle, show that $\Spec(A)$ is spatial if
and only if for any ideal $\aaa \subseteq A$ the familiar identity

\[ \sqrt{\aaa} = \bigcap_{\ppp \supseteq \aaa} \ppp \]

* Conclude that the spectrum of any ring is spatial iff holds.

[Prüfer domains as valuation domains]
An integral domain is a ring such that $1 \neq 0$ and such that $xy = 0$
implies $x = 0$ or $y = 0$. A valuation domain is an integral domain
such that for any two elements, one divides the other. A Prüfer domain
is an integral domain such that any finitely generated ideal $\aaa$ is locally a
principal ideal (in the sense that there exists a partition $1 = f_1 + \cdots +
f_n$ such that, for each index $i$, the ideal $\aaa[f_i^{-1}]$ is a principal
ideal in $A[f_i^{-1}]$).

* Let $A$ be a ring. Show that $A^\sim$ is an integral domain if $A$ is.
Does the converse hold?

* Let $A$ be a valuation domain. Show that any matrix over $A$ can be put
into diagonal form by elementary row and column operations.

* Let $A$ be an integral domain. Show that $A$ is a Prüfer domain if and
only if $A^\sim$ is a valuation domain.

* Let $A$ be a Prüfer domain. Show that any matrix over $A$ can locally be
put into diagonal form by elementary row and column operations, by applying the
result of part (b) to $A^\sim$.

[A basic version of Kaplansky's theorem]

* Let $A$ be a local ring. Let $\aaa \subseteq A$ be a finitely generated
ideal such that $\aaa^2 = \aaa$. Show that $\aaa = (0)$ or $\aaa = (1)$.

Hint. Nakayama's lemma.

* Let $A$ be a local ring. Let $M \in A^{n \times n}$ be an idempotent
matrix. Verify that $M$ is similar to a diagonal matrix with entries zero and
one by applying part (a) to the ideals of $k$-minors of $M$. Deduce that the
cokernel of $M$ is finite free.

* Let $A$ be an arbitrary ring. Let $M \in A^{n \times n}$ be an idempotent
matrix. Show that the cokernel of $M$ is finite locally free, by applying the
result of part (b) to $A^\sim$.

* Verify, without using the law of excluded middle or that $A$ is
Noetherian, that an $A$-module $M$ is finitely generated and projective if and
only if it is finite locally free.

Note. A self-contained solution is given in
Ref. blechschmidt:kaplansky.

§ ACKNOWLEDGMENTS

We are grateful to Peter Arndt, Andrej Bauer,
Martin Brandenburg, Thierry Coquand, Martín Escardó, Simon Henry, Matthias
Hutzler, Milly Maietti, Marc Nieper-Wißkirchen, Alexander Oldenziel, Anja
Petković, Peter Schuster, Helmut Schwichtenberg, Steve Vickers and Daniel
Wessel for invaluable discussions shaping this work. We are also grateful to
the anonymous referee, whose comments suggested several improvements to the

We thank the
organizers Klaus Mainzer, Peter Schuster and Helmut Schwichtenberg of
Proof and Computation 2019, where this work was presented, for their
kind invitation and for creating a beautiful and stimulating meeting. We also
express our thanks to the local coordinator Chuangjie Xu and to all
participants of that meeting.

[1]
M. Maietti, Modular correspondence between dependent type theories and
categories including pretopoi and topoi, Math. Structures Comp. Sci.
150 (6), 0 1089–1149  (2005).

[2]
L. Crosilla.
Set theory: constructive and intuitionistic ZF.
In ed. E. Zalta, The Stanford Encyclopedia of Philosophy.
Metaphysics Research Lab, Stanford University  (2015).

[3]
P. T. Johnstone.
The art of pointless thinking: a student's guide to the category of
In Category theory at work (Bremen, 1990), number 18 in Res.
Exp. Math., pp. 85–107, Heldermann  (1991).

[4]
P. T. Johnstone, The point of pointless topology, Bull. Amer. Math. Soc.
80 (1), 0 41–53  (1983).

[5]
S. Vickers, Continuity and geometric logic, J. Appl. Log. 120 (1), 0 14–27  (2014).
URL <https://www.cs.bham.ac.uk/ sjv/GeoAspects.pdf>.

[6]
S. Vickers, Locales and Toposes as Spaces, In eds. M. Aiello,
I. Pratt-Hartmann, and J. van Benthem, Handbook of Spatial Logics, pp.
Springer  (2007).
URL <https://www.cs.bham.ac.uk/ sjv/LocTopSpaces.pdf>.

[7]
M. Bélanger and J.-P. Marquis, Menger and nöbeling on pointless topology,
Logic Log. Philos. 220 (2)  (2013).

[8]
J. Picado and A. Pultr, Frames and Locales. Topology without points.
Front. Math., Birkhäuser  (2012).

[9]
D. Scott, Prime ideal theorems for rings, lattices, and boolean algebras,
Bull. Amer. Math. Soc. 600 (4), 0 390  (1954).

[10]
B. Banaschewski and R. Harting, Lattice aspects of radical ideals and choice
principles, Proc. Lond. Math. Soc. s3-50, 0 385–404

[11]
W. Savin.
Minimal prime ideals and the axiom of choice (answer on
URL <https://mathoverflow.net/a/98734>  (2012).

[12]
P. T. Johnstone, Sketches of an Elephant: A Topos Theory Compendium.
Oxford University Press  (2002).

[13]
F. Richman, Nontrivial uses of trivial rings, Proc. Amer. Math. Soc.
103, 0 1012–1014  (1988).

[14]
H. Lombardi and C. Quitté, Commutative Algebra: Constructive Methods.
Springer  (2015).

[15]
T. Leinster, An informal introduction to topos theory, Publications of
the nLab. 10 (1)  (2011).

[16]
S. Mac Lane and I. Moerdijk, Sheaves in Geometry and Logic: a First
Introduction to Topos Theory. Universitext, Springer  (1992).

[17]
G. Sambin, Some points in formal topology, Theoret. Comput. Sci. 305, 0 347–408  (2003).

[18]
G. Sambin.
Intuitionistic formal spaces – a first communication.
In ed. D. Skordev, Mathematical Logic and its Applications,
Proc. Adv. Internat. Summer School Conf., Druzhba, Bulgaria, 1986, pp.
187–204. Plenum  (1987).

[19]
P. Schuster, Formal Zariski topology: positivity and points, Ann. Pure
Appl. Logic. 1370 (1), 0 317–359  (2006).

[20]
T. Coquand, H. Lombardi, and P. Schuster, Spectral schemes as ringed lattices,
Ann. Math. Artif. Intell. 56, 0 339–360  (2009).

[21]
T. Coquand, H. Lombardi, and P. Schuster, The projective spectrum as a
distributive lattice, Cah. Topol. Géom. Différ. Catég. 480 (3), 0 220–228  (2007).

[22]
M. Shulman.
Stack semantics and the comparison of material and structural set
URL <https://arxiv.org/abs/1004.3802>  (2010).

[23]
A. Kock, Synthetic Differential Geometry, 2 edn. Number 333 in London
Math Soc. Lecture Note Ser., Cambridge University Press  (2006).

[24]
J. M. E. Hyland.
First steps in synthetic domain theory.
In eds. A. Carbonia, M. Pedicchio, and G. Rosolini, Proc. of
the International Conference held in Como, Italy, 1990, vol. 1488,
Lecture Notes in Math., pp. 131–156, Springer  (1991).

[25]
A. Bauer.
First steps in synthetic computability theory.
In eds. M. Escardó, A. Jung, and M. Mislove, Proc. of the 21st
Annual Conference on Mathematical Foundations of Programming Semantics, vol.
155, Electron. Notes Theor. Comput. Sci., pp. 5–31, Elsevier B.V.

[26]
R. Mines, F. Richman, and W. Ruitenburg, A Course in Constructive
Algebra. Universitext, Springer  (1988).

[27]
I. Yengui, Constructive Commutative Algebra. Projective Modules Over
Polynomial Rings and Dynamical Gröbner Bases. Lecture Notes in Math.,
Springer  (2015).

[28]
M. Coste, H. Lombardi, and M.-F. Roy, Dynamical method in algebra: effective
Nullstellensätze, Ann. Pure Appl. Logic. 1110 (3),
0 203–256  (2001).

[29]
T. Coquand and H. Lombardi, A logical approach to abstract algebra, Math.
Structures Comput. Sci. 160 (5), 0 885–900  (2006).

[30]
D. Rinaldi, P. Schuster, and D. Wessel, Eliminating disjunctions by disjunction
elimination, Indag. Math. (N.S.). 290 (1), 0
226–259  (2018).
Virtual Special Issue – L.E.J. Brouwer, fifty years later.

[31]
J. Cederquist and T. Coquand.
Entailment relations and distributive lattices.
In eds. S. Buss, P. Hájek, and P. Pudlák, Logic Colloquium
'98. Proceedings of the Annual European Summer Meeting of the Association for
Symbolic Logic, Prague, Czech Republic, August 9–15, 1998, vol. 13,
Lect. Notes Log., pp. 127–139. A. K. Peters  (2000).

[32]
T. Coquand.
A completeness proof for geometrical logic.
In eds. P. Hájek, L. Valdés-Villanueva, and D. Westerståhl,
Logic, Methodology and Philosophy of Science. Proceedings of the
Twelfth International Congress, pp. 79–90, King's College Publications

[33]
P. Aczel, The Russell–Prawitz modality, Math. Structures Comput. Sci.
110 (4), 0 541–554  (2001).

[34]
M. Maietti, Joyal's arithmetic universes as list-arithmetic pretoposes,
Theory Appl. Categ. 230 (3), 0 39–83  (2010).

[35]
S. Vickers.
Sketches for arithmetic universes.
URL <https://arxiv.org/abs/1608.01559>  (2016).

[36]
I. Blechschmidt and M. Hutzler.
A constructive Knaster–Tarski proof of the uncountability of the
URL <https://arxiv.org/abs/1902.07366>  (2019).

[37]
A. Joyal and M. Tierney, An Extension of the Galois Theory of
Grothendieck. vol. 309, Mem. Amer. Math. Soc., American Mathematical
Society  (1984).

[38]
A. Simpson, Measure, randomness and sublocales, Ann. Pure Appl. Logic.
1630 (11), 0 1642–1659  (2012).

[39]
A. Bauer.
König's lemma and the Kleene tree.

[40]
J. Cederquist and S. Negri.
A constructive proof of the Heine–Borel covering theorem for formal
In eds. S. Berardi and M. Coppo, Types for Proofs and
Programs, pp. 62–75, Springer  (1996).

[41]
S. Vickers, Some constructive roads to Tychonoff, In eds. L. Crosilla
and P. Schuster, From Sets and Types to Analysis and Topology: Towards
Practicable Foundations for Constructive Mathematics, pp. 223–238.
Oxford Univ. Press  (2005).

[42]
G. Wraith, Localic groups, Cah. Topol. Géom. Différ. Catég. 22,
0 61–66  (1981).

[43]
G. Wraith, Galois theory in a topos, J. Pure Appl. Algebra. 19,
0 401–410  (1980).

[44]
B. Banaschewski and C. Mulvey, A globalisation of the Gelfand duality
theorem, Ann. Pure Appl. Logic. 137, 0 62–103  (2006).

[45]
T. Coquand and B. Spitters, Constructive Gelfand duality for
$C^\star$-algebras, Math. Proc. Cambridge Philos. Soc. 147

[46]
S. Henry.
Constructive Gelfand duality for non-unital commutative
URL <https://arxiv.org/abs/1412.2009>  (2014).

[47]
J. Butterfield, J. Hamilton, and C. Isham, A topos perspective on the
kochen–specker theorem, i. quantum states as generalized valuations,
Internat. J. Theoret. Phys. 370 (11), 0
2669–2733  (1998).

[48]
C. Heunen, N. Landsman, and B. Spitters, A topos for algebraic quantum theory,
Comm. Math. Phys. 2910 (1), 0 63–110  (2009).

[49]
S. Henry.
A geometric bohr topos.
URL <https://arxiv.org/abs/1502.01896>  (2015).

[50]
M. Fourman and D. Scott.
Sheaves and logic.
In eds. M. Fourman, C. Mulvey, and D. Scott, Applications of
sheaves, vol. 753, Lecture Notes in Math., pp. 302–401, Springer

[51]
J. Picado and A. Pultr, Locales mostly treated in a covariant way.
vol. 41, Textos Mat. Sér. B, Universidade de Coimbra, Departamento de
Matemática  (2008).

[52]
M. Rathjen.
Remarks on Barr's theorem: proofs in geometric theories.
In eds. D. Probst and P. Schuster, Concepts of Proof in
Mathematics, Philosophy, and Computer Science, vol. 6, Ontos Math.
Log., pp. 347–374. De Gruyter  (2016).

[53]
F. Lawvere, Quantifiers and sheaves, Actes Congrès Intern. Math. 1, 0 329–334  (1970).

[54]
M. Tierney.
On the spectrum of a ringed topos.
In eds. A. Heller and M. Tierney, Algebra, Topology, and
Category Theory. A Collection of Papers in Honor of Samuel Eilenberg, pp.
189–210. Academic Press  (1976).

[55]
G. Wraith.
Intuitionistic algebra: some recent developments in topos theory.
In Proceedings of the International Congress of Mathematicians
(1978, Helsinki), pp. 331–337, Acad. Sci. Fennica, Helsinki  (1980).

[56]
P. T. Johnstone, Topos Theory. vol. 10, L.M.S. Monographs,
Academic Press  (1977).

[57]
S. Henry.
Barr's theorem and constructivity? (question on MathOverflow).
URL <https://mathoverflow.net/questions/142217/>  (2013).

[58]
R. Goldblatt, Topoi: The Categorical Analysis of Logic. vol. 98,
Stud. Logic Found. Math., Elsevier  (1984).

[59]
O. Caramello, Theories, Sites, Toposes: Relating and studying
mathematical theories through topos-theoretic `bridges'. Oxford University
Press  (2018).

[60]
R. Dyckhoff and S. Negri, Geometrisation of first-order logic, Bull.
Symbolic Logic. 210 (2), 0 123–163  (2015).

[61]
M. Rathjen and M. Toppel.
On relating theories: Proof-theoretical reduction.
In eds. S. Centrone, S. Negri, D. Sarikaya, and P. Schuster,
Mathesis Universalis, Computability and Proof, vol. 412,
Synthese Library, pp. 311–331. Springer  (2019).

[62]
A. Tarizadeh.
The flat topology and its duality aspects.
URL <https://arxiv.org/abs/1503.04299v9>  (2015).

[63]
P. T. Johnstone, Rings, fields, and spectra, J. Algebra. 490 (1), 0 238–260  (1977).

[64]
I. Blechschmidt.
Exploring mathematical objects from custom-tailored mathematical
In eds. G. Oliveri, S. Boscolo, and C. Ternullo, Philosophy of
mathematics. Objects, Structures, and Logics (forthcoming). Springer

[65]
C. Mulvey.
Intuitionistic algebra and representations of rings.
In eds. K. H. Hofmann and J. R. Liukkonen, Recent Advances in
the Representation Theory of Rings and $C^*$-algebras by Continuous
Sections, vol. 148, Mem. Amer. Math. Soc., pp. 3–57, American
Mathematical Society  (1974).

[66]
O. Caramello.
Topos-theoretic background.

[67]
T. Streicher.
Introduction to category theory and categorical logic.
URL <https://www.mathematik.tu-darmstadt.de/ streicher/CTCL.pdf>

[68]
F. Borceux, Handbook of Categorical Algebra: Volume 3, Sheaf Theory.
Encyclopedia Math. Appl., Cambridge University Press  (1994).

[69]
M. Shulman.
Categorical logic from a categorical point of view (draft for AARMS
Summer School 2016).
URL <http://mikeshulman.github.io/catlog/catlog.pdf>  (2016).

[70]
M. Hyland.
The effective topos.
In eds. A. S. Troelstra and D. van Dalen, The L. E. J. Brouwer
Centenary Symposium, pp. 165–216, North-Holland  (1982).

[71]
W. Phoa.
An introduction to fibrations, topos theory, the effective topos
and modest sets.
Technical report, University of Edinburgh  (1992).
URL <http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/>.

[72]
A. Bauer.
Realizability as the connection between computable and constructive
URL <http://math.andrej.com/asset/data/c2c.pdf>  (2005).

[73]
A. Ščedrov, Forcing and Classifying Topoi. vol. 295, Mem. Amer.
Math. Soc., American Mathematical Society  (1984).

[74]
J. Hamkins and A. Lewis, Infinite time turing machines, J. Symbolic
Logic. 650 (2), 0 567–604  (2000).

[75]
A. Bauer, An injection from the baire space to natural numbers, Math.
Structures Comput. Sci. 250 (7), 0 1484–1489  (2015).

[76]
D. Normann and S. Sanders, On the mathematical and foundational significance of
the uncountable, J. Math. Log. 180 (2)  (2018).

[77]
F. Richman, The fundamental theorem of algebra: a constructive development
without choice, Pac. J. Math. 1960 (1), 0
213–230  (2000).

[78]
W. Ruitenburg.
Constructing roots of polynomials over the complex numbers.
In ed. A. Cohen, Computational Aspects of Lie Group
Representations and Related Topics, Proc. of the 1990 Computer Algebra
Seminar held in Amsterdam, vol. 84, CWI Tract, pp. 107–128, Centrum
voor Wiskunde en Informatica, Amsterdam  (1991).

[79]
D. Bridges, F. Richman, and P. Schuster, A weak countable choice principle,
Proc. Amer. Math. Soc. 1280 (9)  (2000).

[80]
I. Blechschmidt.
Using the internal language of toposes in algebraic geometry.
PhD thesis, University of Augsburg  (2017).

[81]
F. Richman, The ascending tree condition: constructive algebra without choice,
Comm. Algebra. 310 (4), 0 1993–2002  (2003).

[82]
H. Perdry, Strongly noetherian rings and constructive ideal theory, J.
Symbolic Comput. 370 (4), 0 511–535  (2004).

[83]
H. Perdry, Lazy bases: a minimalist constructive theory of Noetherian rings,
MLQ Math. Log. Q. 540 (1), 0 70–82  (2008).

[84]
H. Perdry and P. Schuster, Noetherian orders, Math. Structures in Comput.
Sci. 210 (1), 0 111–124  (2011).

[85]
J. Tennenbaum.
A constructive version of Hilbert's basis theorem.
PhD thesis, University of California  (1973).

[86]
N. Kraus, M. Escardó, T. Coquand, and T. Altenkirch, Notions of anonymous
existence in Martin–Löf type theory, Log. Methods Comput. Sci. 130 (1)  (2017).

[87]
M. Atiyah and I. Macdonald, Introduction to Commutative Algebra.
Addison–Wesley  (1969).

[88]
E. Palmgren and S. Vickers, Partial horn logic and cartesian categories,
Ann. Pure Appl. Logic. 1450 (3), 0 314–353

[89]
M. Coste.
Localisation, spectra and sheaf representation.
In eds. M. Fourman, C. Mulvey, and D. Scott, Applications of
sheaves, vol. 753, Lecture Notes in Math., pp. 212–238, Springer

[90]
J. Cole, The bicategory of topoi and spectra, Repr. Theory Appl. Categ.
25, 0 1–16  (2016).

[91]
L. Crosilla, Exploring predicativity, In eds. K. Mainzer, P. Schuster,
and H. Schwichtenberg, Proof and Computation, pp. 83–108.
World Scientific  (2018).

[92]
P. Aczel and M. Rathjen.
Constructive set theory (book draft).
URL <https://www1.maths.leeds.ac.uk/ rathjen/book.pdf>  (2010).

[93]
J. Dieudonné and A. Grothendieck, Éléments de géométrie algébrique: IV.
Étude locale des schémas et des morphismes de schémas, Seconde partie,
Publ. Math. Inst. Hautes Études Sci. 24  (1965).

[94]
H. Matsumura, Commutative Ring Theory. vol. 8, Cambridge Stud.
Adv. Math., Cambridge University Press  (1987).

[95]
D. Eisenbud, Commutative Algebra with a View Toward Algebraic Geometry.
vol. 150, Grad. Texts in Math., Springer  (1995).

[96]
C. Staats.
Elementary proof of generic freeness.
<https://math.uchicago.edu/ cstaats/Charles_Staats_III/Notes_and_papers_files/generic_freeness.pdf>

[97]
The Stacks Project Authors.
Stacks Project.
URL <https://stacks.math.columbia.edu/> .

[98]
I. Blechschmidt.
An elementary and constructive proof of Grothendieck's generic
freeness lemma.
URL <https://arxiv.org/abs/1807.01231>  (2018).

[99]
Z. Błocki, An elementary proof of the McCoy theorem, Univ. Iagel. Acta
Math. 30, 0 215–218  (1993).

[100]
T. Lam, Exercises in Modules and Rings. Problem Books in Math., Springer

[101]
N. Bourbaki, Algebra I, Chapters 1–3. Addison-Wesley  (1973).

[102]
T. Coquand and C. Quitté, Constructive finite free resolutions,
Manuscripta Math. 137, 0 331–345  (2012).

[103]
T. Coquand.
A remark about the theory of local rings.
URL <http://www.cse.chalmers.se/ coquand/local.pdf>  (2008).

[104]
T. Coquand, L. Ducos, H. Lombardi, and C. Quitté, Constructive Krull
dimension I: integral extensions, J. Algebra Appl. 80
(1), 0 129–138  (2009).

[105]
T. Coquand, H. Lombardi, and M.-F. Roy, An elementary characterisation of
Krull dimension, In From Sets and Types to Analysis and Topology:
Towards Practicable Foundations for Constructive Mathematics, pp. 239–244.
Oxford Univ. Press  (2005).

[106]
T. Coquand and H. Lombardi, A short proof for the Krull dimension of a
polynomial ring, Amer. Math. Monthly. 1120 (9),
0 826–829  (2005).

[107]
I. Blechschmidt.
Vector bundles on affine schemes (short note).
URL <https://www.ingo-blechschmidt.eu/kaplansky-en.pdf>  (2015).

FUTURE: Why the name "geometric"?
FUTURE: Forcing
FUTURE: Grothendieck quote

FUTURE: Cite Duval and Joyal.

FUTURE: Relate algebraic quantum mechanics to topos theoryto construct new kind
of quantum spaces.?? A spectral invariant for non-commutative algebras ??