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

Question

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?

Answer 1

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.

Answer 2

The following should give some insight to this question, which was more or less the inspiring example of Diers' work on locally multipresentable categories. This involves the "multi" versions of usual universal constructions involved in Gabriel-Ulmer duality.

Locally (finitely) multipresentable categories are (finitely) accessible categories with multi-colimits - or equivalently, (finitely) accessible categories with connected limits commuting with (finitely) filtered colimits.

It is known that any locally finitely multipresentable category can be axiomatized by a small finite-limit/coproduct sketch, equivalently by a disjunctive geometric theory - which often happens to be finitely disjunctive, as in the example below.

In particular, Diers proposed in his thesis a process to construct locally finitely multipresentable categories as follows. If you start with a locally (finitely) multipresentable category $\mathcal{A}$ - hence in particular with a locally (finitely) presentable category - and a choice of a small family $ \Gamma $ of cones of finitely presented maps, then you can take the category $\mathcal{A}_\Gamma$ of objects that are injective relatively to cones in $\Gamma$, and morphisms that are right orthogonal to each arrows involved in the cones of $\Gamma$ (in general arrows in the cones of $\Gamma$ are chosen in a left class in an orthogonal factorization system, so the morphisms in $\mathcal{A}_\Gamma$ are in particular in the corresponding right class).

Then $\mathcal{A}_\Gamma$ can be shown to be locally multipresentable itself, and we have a (finitely) accessible functor $ \mathcal{A}_\Gamma \hookrightarrow \mathcal{A}$ which is a right multi-adjoint and only has to be relatively full and faithful, but not necessarily full. Multireflexiveness involves a kind of small object argument returning a factorization of morphisms with local codomain.

In the example of local rings, take as $\Gamma$ as consisting of the single cone made of the following two finitely presented localizations of the free ring on one generator as in Zariski topology

$ \mathbb{Z}[X] \twoheadrightarrow \mathbb{Z}[X,Y]/(XY-1)$ and $\mathbb{Z}[X] \twoheadrightarrow \mathbb{Z}[X,Y]/((X-1)Y-1)$

Then as expected the objects of $CRing_\Gamma$ are the local rings, but moreover conservativity of a ring homomorphisms just has to be tested relatively to either one of those localizations. Hence $CRing_\Gamma$ is the category with the good choice of morphisms. In this case relative fullness comes from the fact that conservative morphisms are a right class in the (localization, conservative) factorization system in $CRing$ and hence have right cancellability. And the result above says that $CRing_\Gamma = LocRing^{Cons} $ is a locally finitely multipresentable category. Hence there must be a small finite-limit/coproduct sketch axiomatizing it, and hence a disjunctive theory in some convenient signature (though I must admit I don't know which one).

However I don't think that the finite limit part of this sketch is the same as the finite limit sketch of commutative rings, because there is a result by Adamek-Rosicky suggesting that the category of models of a finite limit-coproduct sketch should be a full multireflective subcategory of the category of models of the underlying finite limit sketch.

There is also an interesting paper from Johnstone about disjunctive theories and their link with Diers multipresentability that may be of interest relatively to this question.

Answer 3

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.