# What is the theory of local rings and local ring homomorphisms?

It is well-known that the category of local rings and ring homomorphisms admits an axiomatisation in coherent logic. Explicitly, it is the coherent theory over the signature $0, 1, -, +, \times$ with the usual axioms for rings, plus the axioms $$0 = 1 \vdash \bot$$ $$\top \vdash (\exists b . \; a \times b = 1) \lor (\exists b . \; (1 - a) \times b = 1)$$ See, for example, [Sheaves in Geometry and Logic, Ch. VIII, §6]. Unfortunately, because homomorphisms are only required to commute with the various things in the signature, the homomorphisms here are just ring homomorphisms and need not be local. It appears to me that the neatest way to fix this is to introduce a unary relation symbol $(\quad) \in \mathfrak{m}$, with the intention that $\mathfrak{m}$ is interpreted as the unique maximal ideal of the local ring. Then, by the usual rules for homomorphisms of models, a homomorphism $R \to R'$ must map elements of $\mathfrak{m}$ to elements of $\mathfrak{m}'$. But is there a way to axiomatise the theory so that

1. we get a coherent, or at least geometric theory, and

2. the category of models in $\textbf{Set}$ is indeed the category of local rings and local ring homomorphisms, and

3. the structure sheaf homomorphism $f^\ast \mathscr{O}_{Y} \to \mathscr{O}_{X}$ of morphism of locally ringed spaces $X \to Y$ is a homomorphism in the category of models for this theory?

Ideally, we'd like to define $\mathfrak{m}$ to be the subsheaf of nowhere invertible sections defined by $$\{ s \in \mathscr{O} : \nexists t . \; s \times t = 1 \}$$ but unfortunately $\nexists t . \; s \times t = 1$ is not a geometric formula. (The formula $\forall t . \; s \times t \ne 1$ is equivalent to the previous one but has the same defect.) We can salvage one half of the biimplication as the geometric sequent $$(a \in \mathfrak{m}) \land (\exists b . \; a \times b = 1) \vdash \bot$$ which merely expresses the requirement that "$a$ is not in $\mathfrak{m}$ if $a$ is invertible", but we also need to express the requirement that "$a$ is in $\mathfrak{m}$ if $a$ is not invertible". One possibility is the following: $$\top \vdash (\exists b . \; a \times b = 1) \lor (a \in \mathfrak{m})$$ These two axioms appear to give the correct characterisation of $\mathfrak{m}$ in intuitionistic first order logic: it is easy to derive from these axioms that $$a \in \mathfrak{m} \dashv \vdash \nexists b . \; a \times b = 1$$ so the interpretation of $\mathfrak{m}$ is completely determined by the axioms, at least in a topos.

But does every local ring object (in the sense of the first paragraph) admit an $\mathfrak{m}$ satisfying these axioms? The answer appears to be no, for the reason that these axioms assert that a every section of a sheaf of a local ring admits an open cover of the space by open sets on which the restriction is either invertible or nowhere invertible – and this is certainly not true in the contexts of interest. Can this idea be rescued with a more clever approach?

-
Isn't this question equivalent to asking whether the category of local rings and local ring homomorphisms is coherent, as in ncatlab.org/nlab/show/coherent+category? –  Andrej Bauer Feb 28 '12 at 21:57
Is it? I can't say I know enough about categorical algebra to see why this is plausible/implausible. –  Zhen Lin Feb 29 '12 at 0:17
Because a category is equivalent to the category of models of a coherent theory iff the category is coherent? I might be getting duped by terminology, but I don't think I am. –  Andrej Bauer Mar 2 '12 at 6:14
@Andrej: No, that doesn't seem to be the case. The theory of abelian groups is algebraic, hence coherent, but the category of abelian groups is not coherent (since coherent categories have a strict initial object, while $\textbf{Ab}$ has a zero object). –  Zhen Lin Mar 2 '12 at 7:46
You may want to read about the concept of a "geometry" introduced in Lurie's DAG V. It was invented precisely to get around this problem. –  David Carchedi May 18 '13 at 1:16

If you know the objects of a geometric theory then you also know its morphisms because $\mathbb{T}(\mathbf 2,\mathcal E)\simeq [\mathbf 2,\mathbb{T}(\mathcal E)]$. This is Lemma 4.2.3 in Chapter B of Sketches of an Elephant. Hence, it is impossible for the two theories to have the same objects, but different morphisms as you request.
More explicitly, the local ring corresponding to $\operatorname{Spec} A$ for a discrete valuation ring $A$ corresponds to the ring homomorphism $A \to \operatorname{Frac} A$, which is not a local ring homomorphism. Hence not every local ring in $[\mathbb{2}, \mathbf{Set}]$ comes from a local ring homomorphism in $\mathbf{Set}$. –  Zhen Lin Jun 11 '13 at 17:19
You can define $\mathfrak{m}_R := \{x ~|~ \forall y : 1 - xy \in R^*\}$. Then a homomorphism $R \to S$ of local rings is a map which is compatible with the ring structure and maps $\mathfrak{m}_R$ maps into $\mathfrak{m}_S$. However, this is not equivalent to the usual condition that images of non-units are non-units: In general it is not true that $R = R^* \cup \mathfrak{m}_R$. This is proven by Thierry Coquand in a remark about the theory of local rings. The counterexample is as follows: Consider the Zariski topos $C$ over $\mathbb{Z}$ and the structure sheaf $\mathcal{O}$ of $\mathrm{Spec}(\mathbb{Z})$. Then $\mathcal{O}$ is a local ring in $C$, one verifies that $\mathfrak{m}=\{0\}$ on global sections, so that in particular $2 \in \mathcal{O}^* \vee 2 \in \mathfrak{m}$ is not satisfied.
You are right. I just wanted to mention that with this axiomatization, 1+2 are fulfilled, but 3 is not. Zhen already asked specifically about the equation $R = R^* \cup \mathfrak{m}_R$ (in logical language), therefore I've added this not just as a comment. I hope it's ok ... –  Martin Brandenburg Feb 28 '12 at 10:36
I'm not sure your definition of $\mathfrak{m}$ is geometric/coherent. Certainly, $\exists z . \; z - x y z = 1$ is a coherent formula, but the problem is that what we want is $(\forall y. \; \exists z . \; z - x y z = 1) \vdash x \in \mathfrak{m}$, and this is not a coherent sequent. –  Zhen Lin Feb 28 '12 at 23:25