Skip to main content
6 of 8
deleted 30 characters in body

Here's a nice (imo) universal property. Let $P$ be a poset and $\iota : |P| \to P$ the inclusion of its underlying set (considered as a discrete poset). This induces a functor $\iota^* : \mathsf{Pos}/P \to \mathsf{Pos}/|P|$. We argue that $\iota^*$ has a right adjoint $\iota_*$ and that this adjoint is the lexicographic order construction, in a sense explained below. We first generalize a little. Usually the lexicographic order is defined on non-dependent pairs $P \times Q$, as in your question. But if $P$ is a poset and we have a family $\{Q_x\}_{x\in P}$ of posets indexed by $P$ then the definition of the lexicographic order makes sense for the set of dependent pairs $\sum_{x\in P} Q_x$ too: $(x, y) \leq^\ell (x', y')$ iff $x\leq x$ in $P$ and ($x = x'$ implies $y \leq y$ in $Q_x = Q_{x'}$). It's this lexicographic order we'll talk about, but the non-dependent version can be recovered by looking at constant families.

Now observe that the category of $P$-indexed posets $\mathsf{Pos}^{|P|}$ is equivalent to $\mathsf{Pos}/|P|$, via the functor $E : \mathsf{Pos}^{|P|} \to \mathsf{Pos}/|P|$ sending a family $\{Q_x\}_{x \in P}$ to the coproduct of posets $\coprod_{x\in P} Q_x$ with the obvious map $\pi^E : \coprod_{x\in P} Q_x \to \coprod_{x\in P} 1 \cong |P|$; explicitly we order $\coprod_{x\in P} Q_x$ by keeping the order on each $Q_x$ and making different $Q_{\bullet}$'s mutually incomparable. As usual the inverse of $E$ takes some $\pi : Q \to |P|$ to the family of fibers $\{\pi^{-1}(x)\}_{x\in P}$ (ordered as subsets of $Q$). The only subtlety that comes up when verifying that the standard adjoint equivalence $\mathsf{Set}/|P| \simeq \mathsf{Set}^{|P|}$ lifts is that we need to know for any $\pi : Q \to |P|$ the natural map $\coprod_{x\in P} \pi^{-1}(x) \to Q$ is an order-isomorphism, or more explicitly that distinct fibers $\pi^{-1}(x), \pi^{-1}(y)$ are incomparable. This holds by monotonicity of $\pi$, as $x\leq y$ in $Q$ implies $\pi(x) \leq \pi(y)$ in $|P|$ and by discreteness $\pi(x) = \pi(y)$.

It'll be a little nicer to work with the category $$\mathcal{C} = \mathsf{Pos}^{|P|} \times_{\mathsf{Pos}/|P|} \mathsf{Pos}/P$$ (we mean the strict pullback, but this is equivalent to the weak one because the forgetful functor $\iota_{!} : \mathsf{Pos}/|P| \to \mathsf{Pos}/P$ is an isofibration by general nonsense). The base change of $E$ gives an equivalence $E' : \mathcal{C} \to \mathsf{Pos}/P$ and the base change $F : \mathcal{C} \to \mathsf{Pos}^{|P|}$ of $\iota^*$ satisfies $\iota^* \cong E \circ F \circ (E')^{-1}$. Neglecting some redundant data (or replacing $\mathcal{C}$ by an isomorphic category) the objects of $\mathcal{C}$ are pairs $(\{Q_x\}_{x \in P}, \leq)$ where $\{Q_x\}_{x \in P}$ is a family of posets and $\leq$ is a partial order on $\sum_{x \in P} Q_x$ which (i) restricts to the given order on each cross section $\{x\} \times Q_x \cong Q_x$ and (ii) makes the set-theoretic projection $\sum_{x\in P} Q_x \to P$ monotone. We can restate (ii) as saying whenever $(x, y) \leq (x', y')$ also $x\leq x'$. Morphisms in $\mathcal{C}$ are the obvious thing: morphisms of families as in $\mathsf{Pos}^{|P|}$ such that the induced morphism on $\Sigma$'s is monotone with respect to the chosen orders.

Now for any family $\{Q_x\}_{x \in P}$ observe that the partial order $\leq^{\ell}$ defined previously satisfies conditions (i), (ii). We can then define $L : \mathsf{Pos}^{|P|} \to \mathcal{C}$ by $L(\{Q_x\}_{x \in P}) = (\{Q_x\}_{x \in P}, \leq^\ell)$ on objects and $L(f) = f$ on morphisms. Clearly this is a section of $F$, so we have a natural transformation (the identity) $\varepsilon : F \circ L \to \mathsf{Id}_{\mathsf{Pos}^{|P|}}$. Finally we show that $\varepsilon$ is the counit of an adjunction $F \dashv L$. Hopefully passing back and forth between families and slices hasn't obscured the point too much; we can unravel all of this to calculate a right adjoint $\iota_*$ to $\iota^*$ which on objects sends $\pi : Q \to |P|$ to the same set-function $\pi$ but with the order on $Q$ modified to be $x \leq^{\mathsf{new}} y$ iff $\pi(x) \leq \pi(y)$ and ($\pi(x) = \pi(y)$ implies $x \leq^{\mathsf{old}} y$), and this captures the essence of the lexicographic order.

For an object $Q = (\{Q_x\}_{x \in P}, \leq)$ of $\mathcal{C}$ define $\eta_Q : Q \to L(F(Q))$ to be the family of identity maps $Q_x \to Q_x$. For this to be a well defined morphism in $\mathcal{C}$ we need the induced map $\Sigma_{x \in P} Q_x \to \Sigma_{x \in P} Q_x$, again the identity, to be monotone with respect to $\leq$ on the domain and $\leq^{\ell}$ on the codomain. This is immediate from conditions (i), (ii) and the definition of $\leq^{\ell}$. Finally the triangle identities are trivial to check because $F, L$ don't change the underlying families of set-functions at all and the underlying families of $\eta, \varepsilon$ are the identities.

Here are some other thoughts: the fact that $\iota^*$ is a left adjoint actually doesn't require us to construct $\iota_*$, it follows from the fact that $\iota$ is a Conduché fibration (this is a condition about lifting factorizations in $P$ to factorizations in $|P|$, and in this case it's the fact that $x \leq y \leq z$ and $x = z$ implies $x = y$ and $y = z$). We can very explicitly check that the left adjoint $\iota_! \dashv \iota^*$ is fully faithful (it's immediate from injectivity of $\iota$) and since we have an adjoint triple $\iota_! \dashv \iota^* \dashv \iota_*$ this implies $\iota_*$ is fully faithful as well. And then $\iota_! \circ \iota^*$, $\iota_* \circ \iota^*$ are the coreflection and reflection of $\mathsf{Pos}/P$ at the class $W$ of morphisms which restrict to bijections on fibers. So given a poset $Q$ over $P$ the coproduct of the fibers of $Q$, i.e. $\iota_!(\iota^*(Q))$, is characterized by being $W$-colocal and mapping into $Q$ via an element of $W$ while the lexicographic order on $Q$, i.e. $\iota_*(\iota^*(Q))$, is characterized by being $W$-local and mapping into $Q$ via an element of $W$. A decategorification of this is that if we fix a family $\{Q_x\}_{x \in P}$ of posets then the coproduct order on $\sum_{x \in P} Q_x$ is the minimum order satisfying (i) and (ii) while the lexicographic order on $\sum_{x \in P} Q_x$ is the maximum order satisfying (i) and (ii). I'm sure you could rephrase what I did above in terms of this. This description in terms of slices also sort of clarifies why the lexicographic order isn't a grothendieck construction. In a topos or locally cartesian closed category the left adjoint to pullback is dependent sum, which the grothendieck construction is like a higher dimensional version of, while the right adjoint is dependent product. But this is still strange: why does the lexicographic order on the dependent sum arise as a sort of dependent product? Maybe the answer lies in the semantics of directed type theory (which I know nothing about). I also wonder if there's any cohesion stuff happening here since it's all about slices and discreteness (although again this isn't something I understand). The fact that we get a "dependent product" maybe suggests that the lexicographic order is a lax limit, but I didn't work that part out.