22
$\begingroup$

Consider the language of rigs (also called semirings): it has constants $0$ and $1$ and binary operations $+$ and $\times$. The theory of commutative rigs is generated by the usual axioms: $+$ is associative, commutative, and has unit $0$; $\times$ is associative, commutative, and has unit $1$; $\times$ distributes over $+$; and $0$ is absorbing for $\times$.

Every commutative ring is a commutative rig (of course), and every distributive lattice as well (interpreting $\bot$ as $0$, $\top$ as $1$, $\vee$ as $+$, and $\wedge$ as $\times$). In fact, the category of commutative rings is a full reflective subcategory of the category of commutative rigs, as is the category of distributive lattices. The intersection of the two is trivial, in the sense that only the trivial algebra is both a ring and a lattice. (In a lattice, $\top \vee \top = \top$; but in a ring $1 + 1 = 1$ implies $0 = 1$.) What I am wondering is how close do these two subcategories come to capturing "all" the possible behaviour of commutative rigs. More precisely:

Question 1. Is there a Horn clause in the language of rigs that is true in every commutative ring and every distributive lattice but false in some commutative rig?

Since commutative rings are not axiomatisable in the language of rigs using only Horn clauses, I would also be interested to hear about, say, cartesian sequents instead of Horn clauses. This can be phrased category theoretically:

Question 2. Is there a full reflective subcategory $\mathcal{C}$ of the category of commutative rigs that is closed under filtered colimits and contains the subcategories of commutative rings and distributive lattices but is not the whole category? (Furthermore, can we choose such a $\mathcal{C}$ so that the reflection of $\mathbb{N} [x]$ (= the free commutative rig on one generator) represents a monadic functor $\mathcal{C} \to \textbf{Set}$?)

I don't want to be too permissive, however – since commutative rings and distributive lattices can both be axiomatised by a single first order sentence in the language of rigs, taking their disjunction yields a sentence that is true in only commutative rings and distributive lattices but false in general commutative rigs.

Here is an example of a first-order axiom that is true in commutative rings and distributive lattices that is false in some commutative rig:

For all $a$ and $b$, there exist $c$ and $d$ such that $(c + d) a + d b = b$.

This axiom amounts to saying that every ideal is subtractive (which is a second-order axiom prima facie); it is the case that every ideal in a commutative ring or distributive lattice is subtractive. The way I prefer to think about it is that in a commutative ring, ideals are automatically subtractive because $-1$ exists, and in a distributive lattice, ideals are automatically subtractive because they are downward closed. As it turns out, this can be expressed as a first-order sentence, albeit not a cartesian sequent.

$\endgroup$
  • 9
    $\begingroup$ How about $x+z=y+z, x\times z = y \times z \vdash x = y$? There should be a rig where that doesn't hold, but it is true in every commutative ring and every distributive lattice. $\endgroup$ – François G. Dorais Sep 10 at 9:14
  • 4
    $\begingroup$ Very nice! That axiom says that for a ring or a distributive lattice $(-) + z$ and $(-) \times z$ are jointly injective, which seems to be worth thinking about. It fails in $\mathbb{N} \cup \{ +\infty \}$ (which is a semiring if we define $0 \times {+ \infty} = 0$). I will accept that as answer. $\endgroup$ – Zhen Lin Sep 10 at 9:44
24
$\begingroup$

Following François's suggestion, I ran alg to find a unital commutative semiring which fails to satisfy $$ \forall x\, y\, z,\; x + z = y + z \land x \times z = y \times z \Rightarrow x = y. \tag{1} $$ The smallest one has size 3. Here is the output of the program, cut off after the first example.

    Theory unital_commutative_semiring.
    
    Constant 0 1.
    Binary + *.
    
    Axiom: 0 + x = x.
    Axiom: x + 0 = x.
    Axiom: x + (y + z) = (x + y) + z.
    Axiom: x + y = y + x.
    
    Axiom: 1 * x = x.
    Axiom: x * 1 = x.
    Axiom: x * (y * z) = (x * y) * z.
    Axiom: x * y = y * x.
    
    Axiom: (x + y) * z = x * z + y * z.
    Axiom: x * (y + z) = x * y + x * z.
    
    Axiom: 0 * x = 0.
    Axiom: x * 0 = 0.
    
    # Extra command-line axioms
    Axiom: not forall x y z, x + z = y + z /\ x * z = y * z => x = y.

# Size 3

### unital_commutative_semiring_with_extras_3_1


    + |  0  1  a
    --+---------
    0 |  0  1  a
    1 |  1  1  1
    a |  a  1  a


    * |  0  1  a
    --+---------
    0 |  0  0  0
    1 |  0  1  a
    a |  0  a  0

We can also count the structures. For commutative unital semirings the counts are

    size | count
    -----|------
       2 | 2
       3 | 6
       4 | 36
       5 | 228
       6 | 2075

The counts for commutative unital semirings that also satisfy (1):

    size | count
    -----|------
       2 | 2
       3 | 3
       4 | 9
       5 | 12
       6 | 23

So clearly there will be some, but it looks like not too many for small sizes.

It is a bit weird that $2, 6, 36, 228, 2075$ is not in OEIS.

| cite | improve this answer | |
$\endgroup$
  • 2
    $\begingroup$ The example you give is even an affine quantale! Interesting... $\endgroup$ – Zhen Lin Sep 10 at 11:43
  • 9
    $\begingroup$ The example could perhaps be concisely described as “the three-element semiring {0,1,infinitesimal}”. $\endgroup$ – Peter LeFanu Lumsdaine Sep 10 at 12:43
  • 2
    $\begingroup$ A square-nilpotent infinitesimal no less. $\endgroup$ – Andrej Bauer Sep 10 at 13:15
  • 3
    $\begingroup$ Andrej, thank you for alg! It's a really wonderful tool, I wish I had remembered it when I made my suggestion in the comments since I did look at it a while ago but I forgot about it... Thank you for working it out for us! $\endgroup$ – François G. Dorais Sep 11 at 2:57
  • $\begingroup$ There's an easy way to remedy the absence from OEIS... $\endgroup$ – Timothy Chow Sep 11 at 12:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.