Ring orderings - structure or predicate?

Stream: maths

[Artie Khovanov]

Let $R$ be a (commutative) ring. A preordering on $R$ is a subsemiring of $R$ containing all squares but not containing $-1$. The support $\text{supp}(P)$ of a preordering $P$ on $R$ is the set $P\cap-P$. An ordering on $R$ is a preordering $P$ such that $P\cup-P=R$ and $\text{supp}(P)$ is a prime ideal.

Orderings on $R$ correspond to linearly ordered ring structures on quotient domains of $R$. It turns out that any preordering is contained in an ordering, which proves that a field can be linearly ordered if and only if $-1$ is not a sum of squares. Orderings are therefore a fundamental prerequisite for the formalisation of real algebra.

Reference: https://doi.org/10.1216/RMJ-1984-14-4-767

Orderings were formalised in Mathlib by me here. I defined preorderings as a type docs#RingPreordering of structures extending docs#Subsemiring, and ring orderings as a predicate docs#RingPreordering.IsOrdering on docs#RingPreordering.

PR #32077, which defines the standard operations on preorderings, has raised an issue. Preorderings don't have a total supremum, map, or closure operation, since the subsemiring closure might contain $-1.$ Preorderings are, however, closed under directed unions and nontrivial intersections, and preserved under surjective maps whose kernel is contained in the support. This means these operations are not naturally backed by API, and are annoying to define totally. However, I need the directed union and map operations to prove the results mentioned above, which justify defining orderings in the first place!

@Yaël Dillies has suggested unbundling docs#RingPreordering into a predicate IsRingPreordering on docs#Subsemiring to avoid this issue of partial operations. I feel well out of my depth. Does anybody have thoughts on how to proceed?

[Kevin Buzzard]

docs#RingPreordering

[Kevin Buzzard]

So right now you have a structure extending Subsemiring for the preorders, which could have been a predicate on Subsemiring, and a (class) predicate docs#RingPreordering.IsOrdering on this struture . Subsemirings are a nice lattice with sup, map, closure etc but preorders aren't so lucky. You say "preorderings are closed under directed unions and nontrivial intersections" etc etc -- by this I guess you mean "if I perform these operations in Subsemiring then they preserve preorders" so it sounds like it would be much easier to state all of these results if you had IsRingPreorder (P : Subsemiring R) : Prop i.e. "do what you did for orders, but do it for preorders too".

[Artie Khovanov]

Yep agree with everything you said

[Artie Khovanov]

I suppose my concern is - why is docs#Subsemiring not itself a predicate? When do we care about the type of all subsemirings of a (semi)ring? In other words, if I refactor docs#RingPreordering into a predicate, will I lose something important? What questions should I be asking in making this decision?

[Kevin Buzzard]

Subsemirings are a good choice for a structure precisely because they are super-well-behaved under closure, map etc etc, there will be adjoint functors and Galois connections everywhere, they will form a complete lattice etc etc.

[Kevin Buzzard]

You say "a predicate" -- but what exactly do you mean? A predicate on what? Subsemirings are in some sense the simplest sensible substructure of a semiring, it's not so clear what you want to put a predicate on.

[Artie Khovanov]

Right, I see. The best I could do for preorderings was docs#CompletePartialOrder, which did allow me directed unions - but doesn't resolve the issue with intersections or map/pushforward. I think that, since the operations I want are just the same as the underlying subsemiring operations (not true for e.g. subsemiring on top of additive submonoid, or subring on top of subsemiring), preorderings should be formalised as a predicate on subsemirings.

[Kevin Buzzard]

I guess you could try IsSubSemiring : Set R -> Prop (and also IsSubgroup, IsSubmonoid etc) but IIRC we had this a long time ago and it didn't work as well; I have forgotten the details (I just remember deprecating them in Yorkshire when England men were losing the Euros football final to Italy, funny what your brain retains).

[Artie Khovanov]

Oh and I suppose that answers your second question (for preorderings). The type of IsPreordering should be Subsemiring R → Prop precisely because the operations I want are the subsemiring operations. Obviously for directed union or nonempty intersection it makes no difference, but I'll give a more advanced example.

We want to prove that every preordering is contained in an ordering. It's straightforward to show that a maximal preordering must be an ordering and that preorderings are closed under arbitrary directed unions. So by Zorn's lemma we just need the successor step. Indeed, it turns out that, given a preordering $P$ and some $x\in R$, either $-1\notin\text{cl}(P\cup\{x\})$ or $-1\notin\text{cl}(P\cup\{-x\})$, where $\text{cl}$ is the semiring-closure. So we're done.

Therefore I argue that it is precisely the subsemiring operations we wish to make use of here.

[Aaron Liu]

Artie Khovanov said:

Preorderings don't have a total supremum, map, or closure operation, since the subsemiring closure might contain $-1.$

Why do you boot want to contain -1? Is it analogous to requiring filters be proper, or requiring affine subspaces be nonempty? It sounds like if you let the whole ring be a preordering then preorderings become a complete lattice whose coatoms are the orderings.

[Artie Khovanov]

Without the condition that preorderings do not contain $-1$, we are just looking at the type of subsemirings that are greater than docs#Subsemiring.sumSq. This does form a lattice, albeit an uninteresting one.

However, the condition that the subsemiring does not contain $-1$ is not merely a nontriviality condition. It excludes many more semirings than just the top element. In particular, coatomic subsemirings almost always might still contain $-1.$ Indeed, the whole interesting question is when you can construct bigger subsemirings that do not contain $-1$ from smaller subsemirings that do not contain $-1$!

I suppose you could define a type RingPreordering R whose terms are preorderings (in the informal sense) along with a formal top element $⊤$. I guess this is a general construction for turning meet-semilattices into complete lattices. However, I do not see the benefit of such an abstraction over unbundling the notation into a predicate on subsemirings.

[Artie Khovanov]

OK, well, I took some time to do the refactor. It seems to work fine? I probably need to update one more file before I'm sure the design doesn't have any big issues - this is the file that proves the correspondence of orderings and linear orders.

[Artie Khovanov]

Just realised something. @Aaron Liu I was wrong. The situation is close to analogous to what you said. Precisely:

1. Every maximal ordering is indeed a coatom in the lattice of subsemirings. This is because the subring generated by an ordering is always $R$.
2. The converse holds if $2$ is invertible in $R$. Indeed, if a subring $S$ contains all squares, then $x=((1+x)/2)^2-((1-x)/2)^2\in S$ for any $x\in R$. In other words, every coatomic subsemiring that contains all squares is an ordering.
3. However this converse does not hold in general. A counterexample is obtained (by Zorn) precisely when the subring generated by the squares is proper. For instance, the subring generated by the squares in $\mathbb{Z}[X]$ misses $X,X^3,X^5,\dots$ since the odd-degree coefficients of any $f^2$ are all even. So this ring will have coatomic subsemirings containing all squares that are not orderings.

So we can often do what you say in practice, but it's not true in general.

[Artie Khovanov]

I wonder if the class of rings whose squares generate the whole ring (as a ring) is known in the literature?