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: learning: questions

Topic: the generic inhabited linear order

James Deikun (Sep 09 2021 at 19:56):

At https://ncatlab.org/nlab/show/classifying+topos#ForLinearOrders I learned that $Set^{\Delta}$ is the classifying category of inhabited linear orders. Now I know that in general arbitrarily much of the classifying topos may be required to represent an instance of the geometric theory it classifies, but from the axioms of this one it seems like it should be reducible to finitely many finitely presented objects. However I am not very familiar with the process of doing this when a theory has relations in its signature. Does anyone know which small diagram of cosimplicial sets represents the 'generic linearly ordered set' and its order relation in a nice way?

Morgan Rogers (he/him) (Sep 10 2021 at 07:51):

The universal model of inhabited linear orders is the representable on the (dual of) the one-element ordinal, and the ordering on it is given by the two morphisms from the (dual of) the two-element ordinal.

Morgan Rogers (he/him) (Sep 10 2021 at 08:06):

You're probably wondering how I worked this out!

For the topos of presheaves over $\mathcal{C}$, we can identify theories classified by this topos as those theories whose finitely presentable models form a category equivalent to $\mathcal{C}^{\mathrm{op}}$. This is much harder for non-algebraic theories, because there may be no free models on a generic finite set. This is the case here: there is no "free linear order on two elements", for instance, since there is no canonical way to put them in an order.

However, we see that every presentation consisting of a finite number of generating elements and enough axioms to guarantee they can be put into a linear order determines a finitely presented total order, namely the one obtained by closing under the axioms of the theory. So $\{x,y : x < y\}$ is a formula/presentation of the two element linear order, but so does $\{x,y,z : (x = y) \wedge (y < z)\}$. These formulas-in-context can be identified with objects of the syntactic category for the theory, and this is the identification we need to make in order to arrive at the conclusion above.

Now we use the following observations:

• $\{x : \top \}$ is a presentation of the one-element linear order (the only free linear order). But in the syntactic category, this formula is a presentation of the basic sort of the theory, the carrier set.
• $\{x,y : x<y\}$ is a presentation of the two-element linear order, as we saw above, but in the syntactic category this formula represents the order relation.
• By definition of our theory, these (along with the morphisms between them, which is to say the projection morphisms) entirely determine any model of the theory, in particular representing the universal model.

Morgan Rogers (he/him) (Sep 10 2021 at 08:09):

This seems complicated, and for good reason: identifying theories classified by a given topos is hard, and one always has to work to extract a non-trivial theory, where by this I mean anything better than the "canonical" theory obtained by using a maximal site of presentation, such as the entire category $\Delta$ in this instance.

Zhen Lin Low (Sep 10 2021 at 08:13):

Morgan Rogers (he/him) said:

For the topos of presheaves over $\mathcal{C}$, we can identify theories classified by this topos as those theories whose finitely presentable models form a category equivalent to $\mathcal{C}^{\mathrm{op}}$.

** when $\mathcal{C}$ is Cauchy complete

Morgan Rogers (he/him) (Sep 10 2021 at 08:15):

Indeed, thanks Zhen Lin Low

James Deikun (Sep 10 2021 at 19:58):

Thanks very much for this answer; in particular I learned a lot about how finitely presentable models for relational theories behave! Let me try to figure a few things out:

The generic linear order's carrier and relation embed in a certain simplicial object in cosimplicial sets, namely, the standard cosimplicial cosimplices. This object is given by the Yoneda embedding $y$.

The three-element linear order (cotriangle) represents, with its face maps, the transitivity of the order relation. So far so good. Here are some things I am still confused about though:

• What does the degeneracy from the copoint to the cosegment represent? I would think reflexivity but that doesn't hold for a linear order.
• Is there something that represents the asymmetry, comparison or connectedness axioms?
• Every augmented cosimplicial object becomes a cosimplicial object by restriction. This would seem to mean that a linear order is a kind of inhabited linear order, rather than the other way around like one would think?

Morgan Rogers (he/him) (Sep 11 2021 at 14:24):

I thought about this for some time, until eventually I followed up the reference to Moerdijk's book on the nLab page and realised that IT IS AN ERROR. What Moerdijk calls a "linear order" is just a total order; in particular, it is equipped with the reflexive version of the relation. After all, there is no function from the two-element "linear order" to the one-element linear order which preserves antisymmetry of the relation, so the category of models of linear orders in Set is not equivalent to the dual of the simplex category.

Morgan Rogers (he/him) (Sep 11 2021 at 14:26):

So... $\mathrm{Set}^{\Delta}$ classifies the theory of total orders without endpoints. Meanwhile, it is the topos $\mathrm{Set}^{\Delta_{mon}}$ of cosimplicial sets but only the monomorphisms between these which classifies the theory of decidable linear orders; cf Sketches of an Elephant, Example D3.4.11.

Morgan Rogers (he/him) (Sep 11 2021 at 14:26):

Everything I said is true, but for the latter topos rather than the former. Replace < with ${\leq}$ to apply it to $\mathrm{Set}^{\Delta}$.

Morgan Rogers (he/him) (Sep 11 2021 at 14:48):

Now, to answer your other questions in $\mathrm{Set}^{\Delta_{mon}}$, to represent the asymmetry axiom we need to extend to a fragment of logic containing $\bot$ and intersections of relations. In this case it's enough to extend the embedded representables (corresponding to the n-fold order relation, as you've spotted), with the initial object of the topos, which represents $\{\vec{x} : \bot\}$ for any context $\vec{x}$; the fact that this is the intersection of $<$ and $>$ corresponds to antisymmetry.
For comparison we need unions of relations, but that's okay too, we can extend to the coherent syntactic category (which embeds into the topos too!), and then the comparison axiom is the observation that a certain subobject of the form $y[1] \times y[2] \hookrightarrow y[1]^3$ is contained in the union of two others of the same form (I'll let you figure out the details of that one ;) )

For your final question, I don't follow the reasoning; it should indeed be the case that any inhabited linear order is a special case of a linear order and not the other way around!

Morgan Rogers (he/him) (Sep 11 2021 at 15:01):

Morgan Rogers (he/him) said:

I thought about this for some time, until eventually I followed up the reference to Moerdijk's book on the nLab page and realised that IT IS AN ERROR.

I mentioned this on the nforum; I've added it to my "nLab edit to-do list" alongside the monad page I promised to improve months ago...