Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: The generic commutative ring is a field!?

John Baez (Jun 08 2026 at 08:55):

@Ingo Blechschmidt wrote a very interesting 3-part post on on Mastodon. Here's the first part, though I recommend reading all of them if you know even a little topos theory:

I love it when formalizing mathematics tells me something new about the mathematics. Today this happened again, with the geometric Nullstellensatz.

First, a quick introduction.

"Recall" that for any geometric theory 𝕋, there is the "generic 𝕋-model", living not in the category of sets but in the rather special, syntactically constructed "classifying topos of 𝕋".

For instance, there is the generic group, the generic ring, the generic ideal of a given ring 𝐴 and so on.

These generic models have exactly those properties which are shared by all models everywhere (i.e. in every Grothendieck topos, in particular in Set). For instance, the generic group does not have the property to be commutative as else all groups would be commutative.

But! This only refers to those properties which can be formulated as geometric sequents. There can very well be first-order formulas which are satisfied by the generic model but not by all models in Set. It is then amazing that geometric-sequent-consequences of these first-order formulas pass down from the generic model to all models. (Definition of "geometric sequent": https://mathstodon.xyz/@iblech/116699667876012150)

For instance, every commutative ring 𝑅 secretly wants to be a field in that all geometric-sequent-consequences of the field axiom ∀x:𝑅. ¬(x = 0) ⇒ (∃y:𝑅. xy = 1) hold. This is because the generic ring has this field property. (This result is due to Mulvey, about which Tierney remarked in 1976 that "its precise significance is still somewhat obscure".) By "¬", I mean Lombardi/Quittè-style "implication to 1 = 0".

I had a bunch of very vague questions about Mulvey's result:

@iblech wrote:

"For instance, every commutative ring 𝑅 secretly wants to be a field in that all geometric-sequent-consequences of the field axiom ∀x:𝑅. ¬(x = 0) ⇒ (∃y:𝑅. xy = 1) hold. This is because the generic ring has this field property."

Wow, this is crazy. Very exciting. Does this have some consequences for algebraic geometry? I can't help but think it explains something about the importance of fields in algebraic geometry. I'd gotten the impression from Mac Lane and Moerdijk's book that fields are taboo in topos-theoretic algebraic geometry and that we should work with local rings instead. Is the definition of local ring the "most important" geometric-sequent consequence of the field axiom, in some sense or other? (For example maybe all other geometric-sequence consequences of being a field follow, in geometric logic, from being a local ring. This may be overoptimistic.)

Graham Manuell (Jun 08 2026 at 10:12):

Despite being a field in a weak sense, the generic ring is not a local ring. There cannot be any geometric consequences of this field condition that don't follow from the ring axioms. That's the whole point of these non-geometric sequents: you can assume them without loss of generality to prove geometric results and it won't change what you'll be able to prove (though maybe the proofs will be easier).

Being a local ring does follow from other stronger definitions of fields, but is unlikely to be the only geometric consequence.

David Corfield (Jun 08 2026 at 14:35):

An interesting discussion of topics in this area is in @David Jaz Myers's Liberating synthetic quasi-coherence from forcing. (David Jaz is using quasi-coherent definability for Ingo's general nullstellensatz.)

Morgan Rogers (he/him) (Jun 08 2026 at 19:24):

Statements like this always seem exciting but inaccessibly mysterious to the unversed in topos theory, so let's make it concrete! What is the generic ring? Because rings form an algebraic theory, the classifying topos is the category of Set-valued functors on the category of finitely presentable rings. The underlying object of the ring is the forgetful functor sending each such ring to its collection of elements.
An equation like x=0 in the language of rings with a single free variable gets interpreted as a subfunctor of this one, namely the (singleton) subset of elements of each finitely presented ring which are equal to 0.
Now here is where one must be careful. If he had written $\neg x=0$ without further qualification, the usual interpretation would be the largest subfunctor disjoint from the one described above, which would be the initial/empty subfunctor because no subfunctor containing an element can avoid becoming 0=1 in the terminal ring. However, Ingo mentions that what he means by $\neg x=0$ is actually another formula, namely $(x=0) \implies (1=0)$ which gets interpreted in the Heyting algebra of subfunctors as the largest subfunctor whose intersection with the subfunctor $x=0$ above is the unique element of the trivial ring.
The claim is that this subfunctor is contained in (and thus consists exactly of) the invertible elements of the finitely presentable rings plus the unique element of the trivial ring (although this happens to be invertible too).
Indeed, if an element of a ring is not invertible, we can quotient by the ideal it generates and obtain a non-degenerate ring in which that element is mapped to 0, so the element can't belong to the subfunctor interpreting $(x=0) \implies (1=0)$. Conversely, if an element is invertible then any homomorphism mapping it to 0 must also map 1 to 0. Tada!
You'll notice that I used the law of excluded middle here. Indeed, when I talked about the category of finitely presentable rings earlier, these are rings in the usual category of classical Sets, which is why this reasoning is meaningful (I.e. that's why I can say that any element of one of these rings is either invertible or non-invertible).

Josselin Poiret (Jun 09 2026 at 13:08):

You don't need LEM for this result: write $P$ for the interpretation of $(x = 0) ⇒ (1 = 0)$, seen as a subobject of the generic ring $R$. Let $x ∈ P(A)$ for an arbitrary fp ring $A$, then we know that its image in $P(A/(x))$ is zero, thus by the definition of $P$, $A/(x)$ is the trivial ring.
It is constructively valid that $A/(x) = 0$ implies $x$ invertible, as this just requires effectivity of quotients. indeed, you then have $1 = 0$ in the quotient ring so necessarily $1 = x * a$ for some $a$.

Morgan Rogers (he/him) (Jun 10 2026 at 10:19):

Josselin Poiret said:

It is constructively valid that $A/(x) = 0$ implies $x$ invertible, as this just requires effectivity of quotients.

I don't know how to unpack this sentence, but the rest was convincing enough to me :) I should have just used a more constructive argument!

Damiano Mazza (Jun 10 2026 at 12:21):

I don't know what "effectivity of quotients" means but isn't this just the fact that the implication $A/I=0 \Rightarrow 1\in I$ for any ideal $I$ is constructively valid? (This is certainly the case because $A/I=0$ means that the congruence generated by $I$ identifies everything, in particular $1$ and $0$, so $1-0\in I$).

Josselin Poiret (Jun 10 2026 at 12:25):

Damiano Mazza said:

I don't know what "effectivity of quotients" means but isn't this just the fact that the implication $A/I=0 \Rightarrow 1\in I$ for any ideal $I$ is constructively valid? (This is certainly the case because $A/I=0$ means that the congruence generated by $I$ identifies everything, in particular $1$ and $0$, so $1-0\in I$).

yes, that's the same idea. Effectivity of quotients means that in a quotient type $p : A → A/R$, two elements $p(a)$ and $p(b)$ are equal iff. $R\:a\:b$. One direction is true for anything that claims to be a quotient type by the universal property of quotients, the other is not necessarily true and depends on your meta theory.

Damiano Mazza (Jun 10 2026 at 12:44):

Ah but wait, then my statement "$A/I=0$ means that the congruence generated by $I$ identifies everything" might be non-constructive? Because we are using precisely the non-trivial direction here.

Josselin Poiret (Jun 10 2026 at 12:51):

whether effective quotients are considered constructive depends on who you talk to, but I guess the most commonly held opinion is that it is still a constructively acceptable principle

Damiano Mazza (Jun 10 2026 at 12:52):

Oh wow, ok. I had no idea that this could be such a tricky issue! :smile:

Josselin Poiret (Jun 10 2026 at 13:07):

To be a bit more precise: quotients in a theory like Cubical Type Theory are effective, and CTT is considered constructive, as it should have the witness property by the proofs of normalization we have. For a more “standard” type theory such as MLTT+effective quotients, I don't know of any proof of a witness property, but maybe someone can correct me.

Jon Sterling (Jun 16 2026 at 06:49):

From the point of view of philosophical constructivists, MLTT is not aimed to be a theory of sets (which should have quotients) but rather as the computational substrate on which a theory of sets is built — via setoids. And, naturally, the setoid construction yields effective quotients. Perhaps one can think of cubical type theory as a more thorough realisation of this vision — though, to be sure, it has some substantial differences (e.g. setoids magically make countable choice true, which won't happen in cubical type theory).

Jon Sterling (Jun 16 2026 at 07:00):

It's also true that people haven't investigated the canonicity property for MLTT + effective quotients, as @Josselin Poiret points out. I have to think a bit about this question, but I have a feeling that it is very subtle.

In any case, I think that the question of whether something "is constructive" can have different kinds of answers. A very strong kind of constructivity for X is that the syntactic category of MLTT+X has the canonicity property for numerals (and that this can be proved in some suitably weak metatheory).

But usually when people in the type theory world speak of the philosophical justification of some concept as being "constructive" what they mean is that there is a model of that concept that can be built in some philosophically acceptable way (again, allowing for differences in what people consider 'acceptable'), where the model has some kind of philosophically evident computational content. Or, a little stronger, one might ask for a model that can take the form of a syntactic translation.

So as far as the question of the constructivity of effective quotients is concerned, I think that the setoid and groupoid and cubical models establish that these are constructive in a pretty strong philosophical sense. It is true that we can also come up with countermodels (e.g. assemblies or type theories that mirror their structure, like CiC), but the goal of a philosophical explanation of type theory is to explain "how something _can_ be justified" not "how something _must_ be justified".