= Solution
Use one ring sort with $0,1,+,-,\cdot$ and the usual unital <commutative ring> equations. Write $\operatorname{Inv}(x)$ for the <coherent formula> $\exists y\,(xy=1)$. Add the <coherent sequents>
$$
0=1\vdash\bot,\qquad\top\vdash_x\operatorname{Inv}(x)\vee\operatorname{Inv}(1-x).
$$
This presents the <coherent theory of local rings>. For an ordinary nonzero ring satisfying these axioms, the nonunits form an ideal: a multiple of a nonunit cannot be a unit; and if nonunits $a,b$ had unit sum, multiplying by $(a+b)^{-1}$ would make two nonunits sum to $1$, contradicting the second axiom. They are also closed under additive inverses. This proper ideal contains every proper ideal, since a proper ideal contains no unit, and its quotient is a field; it is the unique <maximal ideal>. Conversely in a <local ring>, $x$ and $1-x$ cannot both belong to the unique <maximal ideal>, so one is a unit. The first sequent excludes the zero ring. In a <topos>, the disjunction asserts that these unit alternatives hold locally.
Let $\mathcal C$ be a small skeleton of the opposite of the category of finitely presented unital <commutative rings>; write $C_A$ for the object corresponding to $A$. The <Zariski coverage on finitely presented rings> is generated by
$$
\{C_{A[f_i^{-1}]}\longrightarrow C_A\}_{i=1}^n,\qquad(f_1,\ldots,f_n)=A,
$$
and the empty cover of $C_0$. Localization is finitely presented, and its compatibility with base change proves the covering axioms.
Here is the classifying argument. For an internal commutative ring $M$ and a presentation $A=\mathbb Z[x_1,\ldots,x_n]/(p_1,\ldots,p_r)$, define $F_M(C_A)$ as the <subobject> of $M^n$ satisfying the polynomial equations $p_i=0$. Ring maps induce maps of these solution objects in the site direction. This is independent of presentation, and it preserves <finite limits>: finite colimits of finitely presented rings correspond to joining finite generators and equations, whose solution objects are <finite limits>. Conversely a left-exact <functor> $F:\mathcal C\to\mathcal E$ reconstructs a commutative ring $F(C_{\mathbb Z[t]})$ using the polynomial maps for addition, multiplication, constants and additive inverse. Presentations by generators and equations then show $F\cong F_M$. Thus flat <functors> on $\mathcal C$ correspond to internal <commutative rings>.
Under $F_M$, the localization arrow above identifies its domain with the locus where $f_i$ evaluates to a unit; the inverse witness is unique. The family is jointly epimorphic exactly when these unit loci cover the solution object for $A$. The locality axiom implies this for every unit-ideal family: from a finite sum $\sum f_i g_i=1$, repeatedly apply the two-summand unit alternative, rescaling a unit partial sum when necessary; some $f_i g_i$, hence some $f_i$, is a unit locally. Conversely the cover of $\mathbb Z[t]$ by its localizations at $t$ and $1-t$ gives precisely the locality axiom, while the empty cover of the zero ring gives $0=1\vdash\bot$. Therefore continuous flat <functors> are exactly models of the displayed <coherent theory>. The <Diaconescu equivalence for geometric morphisms> now identifies
$$
\operatorname{Geom}(\mathcal E,\operatorname{Sh}(\mathcal C,Z))\simeq\operatorname{Mod}_{\mathrm{local\ rings}}(\mathcal E),
$$
naturally in $\mathcal E$. This proves the asserted <classifying topos> identification.
Since the site is <subcanonical>, the <generic local ring> is the representable sheaf
$$
R=yC_{\mathbb Z[t]},\qquad R(C_A)=\operatorname{Hom}_{\mathrm{Ring}}(\mathbb Z[t],A)=A.
$$
Its ring operations are induced by polynomial substitution. Its infinitesimal <subobject> is likewise representable:
$$
D=yC_{\mathbb Z[\varepsilon]/(\varepsilon^2)},\qquad D(C_A)=\{a\in A:a^2=0\}.
$$
Products of representables correspond to tensor products of their rings. For every finitely presented $A$, exponential adjunction and the <Yoneda lemma> give
$$
\begin{aligned}
(R^D)(C_A)&\cong\operatorname{Hom}(yC_A\times D,R)\\
&\cong\operatorname{Hom}(yC_{A[\varepsilon]/(\varepsilon^2)},yC_{\mathbb Z[t]})\\
&\cong A[\varepsilon]/(\varepsilon^2).
\end{aligned}
$$
Every element of this ring has a unique expression $a+b\varepsilon$, because $1,\varepsilon$ form an $A$-basis. This holds even when $A$ has nilpotents or zero divisors. The expression is natural under every <ring homomorphism> $A\to B$, which sends its two coefficients to their images. The canonical morphism $R\times R\to R^D$, transposed from $(a,b,d)\mapsto a+bd$, is consequently a bijection at every stage $C_A$, with a natural inverse extracting the coefficients. Therefore
$$
\boxed{R\times R\xrightarrow{\sim}R^D,\qquad(a,b)\longmapsto(d\mapsto a+bd).}
$$
This proves the <Kock-Lawvere axiom for the generic local ring>. The uniqueness is an internal sheaf assertion tested at all finitely presented rings, including the ring with its generic square-zero element; restricting the test to fields would lose that element and would not prove uniqueness.
Back to article page
