# WR: Internal Orders

See Carboni and Street, [Order ideals in categories](https://msp.org/pjm/1986/124-2/pjm-v124-n2-p02-p.pdf), 1986. One starts with a regular category $\cal E$ and forms the category $Ord(\cal E)$ of internal preorders. (Internally) monotone relations are called ideals. The paper starts with the minimal assumption on $\mathcal E$ of being regular and proceeds to the case where $\mathcal E$ is a topos.

There is a follow-up on [internal metric spaces](https://hackmd.io/@alexhkurz/r1UYWxBeD) under construction.

## Notational Preliminaries

(feel free to skip at first ... this section keeps getting longer)

- In a regular category $\cal E$, a relation $R:A\to B$ is a mono-span $\,A\stackrel{\ dR}{\longleftarrow} R \stackrel{cR\ }{\longrightarrow}B\,$.
- Relations form an order-enriched **category of relations** $$Rel(\cal E)$$

Arrows in $\cal E$ are called *maps*. For maps $a:E\to A$ and $b:E\to B$, write $a\,R\,b$ if there is a map $h:E\to R$ such that $a=dR\circ h$ and $b=cR\circ h$. Maps are embedded into relations via $f_\ast = (1,f)$ and $f^\ast=(f,1)$. We have $f_\ast \dashv f^\ast$ and $\ a\,R\,b \ \Longleftrightarrow \ a^\ast\cdot b_\ast \le (dR)^\ast\cdot (cR)_\ast$. [^a-ast]

- A relation in $Rel(\cal E)$ comes from a map iff it is left adjoint. An **internal order** in $\mathcal E$ is an object $A$ with a relation that is reflexive and transitive. $$Ord(\cal E)$$

is the category of internal orders with monotone maps. Since $\le$ is a relation, we already said what we mean by $f\le f'$ and $Ord(\cal E)$ is an order-enriched category.
- A **monotone relation** $R:(A_o,\le_A)\to(B_o,\le_B)$ is a relation $A_o\to B_o$ such that ${\le_A}\cdot R\cdot {\le_B}=R$. Monotone relations form an order-enriched category
$$Rel(Ord(\cal E))$$

A monotone map $f:A\to B$ is embedded to relations via $f_\diamond = f_\ast\cdot {\le_B}$ and $f^\diamond = {\le_B}\cdot f^\ast$. [^diamond-ast] We have $f_\diamond \dashv f^\diamond$.

See also the notes on the [calculus of relations](https://hackmd.io/@alexhkurz/S1QpkXNJD).

## Questions

Is the category $Rel(Ord(\cal E))$ always well-behaved? What are the precise conditions under which $Ord(\cal E)$ is order regular? Which order-regular categories arise in this way?

How do the two embeddings $\mathcal E\to Rel(\mathcal E)$ and $Ord(\mathcal E)\to Rel(Ord(\mathcal E))$ interact? [^embeddings] [^proposition]

There is some work on domain theory in nominal sets. Would it be interesting to look at monotone relations in that setting?

In the case of $\mathcal E$ being a topos, one can also develop a theory of internal metric spaces, see eg Reichman, [Semicontinuous Real Numbers in a Topos](https://core.ac.uk/reader/82582022). Are there weaker assumptions under which one can develop internal metric spaces?

## Technical Preliminaries

Carboni and Street define $e$ to be a **strong epi** if $ae\,R
\,be \Rightarrow a\,R\,b$ for maps $a,b$.

**Remark:**
- If we put for $R$ the order relation on an object, we see that a strong epi in $\cal E$ is a P-epi in $Ord(\mathcal E)$ because of $ae\le a'e \Rightarrow a\le a'$.
- The strong epis in $\mathcal E$ are exactly the left adjoints in $Rel(\mathcal E)$ with $e^\ast\cdot e_\ast = 1$.

They use this notion of strong epi to define *regular category*. In such regular categories all these strong epis are regular.[^strong-epi] It follows that their notion of regular category is equivalent to the usual one (the one of Barr).

**Lemma:** $a\,RS\,c$ if and only if there is a strong epi $e$ and a map $b$ such that $ae\,R\,b\,S\,ce$.

More precisely, for all relations $R:A\to B$ and $S:B\to C$, for all $a:E\to A$ and $c:E\to C$ we have $a\,RS\,c$ iff there is $e:D\to E$ and $b:D\to B$ such that $ae\,R\,b\,S\,ce$.

*Proof of the lemma*: "If": If $ae\,R\,b\,S\,ce$ then $ae\,RS\,ce$, hence $a\,RS\,c$.
"Only If": Let $R=(dR,cR), S=(dS,cS), T=RS=(dT,cT)$. The composition $T$ arises from factoring the pullback $(p,q)$ of $(cR,dS)$ via a strong epi $f:(p,q)\to (dT,cT)$. Now $a(RS)c$ means that there is $y$ such that $a=dT\circ y$ and $c=cT\circ y$. Let $(x,e)$ be the pullback of $(f,y)$. We already defined $e$ and finish the construction by putting $b=cR\circ p\circ y'=dS\circ q \circ y$.

**Remark:** If we had spans instead of relations, it would not be necessary to stick the $e$ into $ae\,R\,b\,S\,ce$. In Rel(Set) we get away without the $e$ because all epis split in Set.

If we apply the lemma to the definition of an adjunction in $Ord(\cal E)$, we can remove the $e$ from the counit because $e$ is strong and therefore $be\le b'e \ \Rightarrow \ b\le b'$:

**Corollary:** $L\dashv R$ if and only if
\begin{gather}
a\le a' \ \Longrightarrow \ \exists e,b \,.\, ae\, L\, b\, R\, a'e \\[1ex]
\exists a \,.\, b\, R\, a\, L\, b' \ \Longrightarrow \ b\le b'
\end{gather}

## Lawvere-Cauchy Completeness

As opposed to in poests or in preorders, in a general $Ord(\cal E)$ left adjoints do not need to be principal (=induced by a map). One only has:

The following proposition falls in between $Rel(\mathcal E)$ and $Rel(Ord(\mathcal E))$ in a curious fashion. Recall that the relation $L:A\to B$ is principal if there is a map $f$ such that $L\cong f_\ast\cdot{\le_B}$.

**Proposition:** The monotone relation $L:A\to B$ has a right adjoint iff there is a strong epimorphic map $e:D_o\to A_o$ such that $e_\ast\cdot L$ is principal.

*Proof:* "If": $e_\ast\cdot L$ is principal, that is, there is $h$ such that $h_\diamond = e_\ast\cdot L$. We define the right adjoint as $R=h^\diamond\cdot e_\ast$. We need to show

\begin{gather}
h^\diamond\cdot e_\ast\cdot L \le 1\\[1ex]
1 \le L\cdot h^\diamond \cdot e_\ast
\end{gather}

We know (a) $h_\diamond \dashv h^\diamond$, that is $h^\diamond\cdot h_\diamond\le 1$ and $1\le h_\diamond\cdot h^\diamond$, and (b) $e$ strong epi, that is, $e^\ast\cdot e_\ast=1$.

For the counit, we calculate $h^\diamond\cdot e_\ast\cdot L = h^\diamond\cdot h_\diamond \le 1$. For the unit, we calculate $1=e^\ast\cdot e_\ast
\le e^\ast\cdot h_\diamond\cdot h^\diamond \cdot e_\ast
= e^\ast\cdot e_\ast\cdot L\cdot h^\diamond \cdot e_\ast
\le L\cdot h^\diamond \cdot e_\ast$.

"Only If": Suppose $L\dashv R$. With $a=a'=1$ in the unit of the corollary above we get $e$ and $b$ such that
$$e\, L\, b\, R\, e$$

The $b$ is uniquely determined by this property because the counit gives us
$$b\,R\,e\, L\, b' \ \Longrightarrow \ b \le b'$$

To finish the proof we need to show $e_\ast\cdot L = b_\diamond$. From $e\,L\,b$ we [know](https://hackmd.io/@alexhkurz/S1QpkXNJD) $b_\ast\le e_\ast\cdot L$, hence $b_\diamond\le e_\ast\cdot L$ (because $L$ is closed under $\le_B$). Similarly, $b\,R\,e$ means $e_\ast \le b_\ast\cdot R$, which gives us $e_\ast\cdot L \le b_\ast\cdot R\cdot L\le b_\ast\le b_\diamond$ because $R\cdot L \le 1$. QED

**Remark:** The "If" direction can be generalised to any 2-category. Indeed, we only used (a) and (b), that is, we only used that (a) $h_\diamond=e_\diamond\cdot L$ has a right-adjoint and not that it is principal and that (b) $e^\diamond\cdot e_\diamond=1$ and not that $e_\diamond$ is principal

An object $B$ in $Ord(\cal E)$ is **Lawvere-Cauchy complete** if all left-adjoints $L:A\to B$ are principal. As a corollary to the proposition we obtain the following.

**Corollary:** An object $B$ in $Ord(\cal E)$ is Lawvere-Cauchy complete if all left-adjoints $L:A\to B$ with $A$ discrete are principal.

**Corollary:** The strong epis in $\mathcal E$ split iff all objects in $Ord(\cal E)$ are Lawvere-Cauchy complete iff all equivalences in $Ord(\cal E)$ are principal.

**Example:** What would be a nice regular category where strong epis do not split? What about nominal sets? How does relational semantics work in nominal sets? What about $Ord(Nom)$?

...

There is more interesting stuff in this paper but I leave it here for now ...

[^a-ast]: $\ a\,R\,b \ \Longleftrightarrow \ a^\ast\cdot b_\ast \le (dR)^\ast\cdot (cR)_\ast$. From left to right follows from the [laws of the embeddings](https://hackmd.io/8NWUvz8gSPueOLTeVh4q2A?both#Laws-of-the-Embeddings). The other direction is immediate from the definition of the order on relations.

[^diamond-ast]: It follows from $f$ monotone that, moreover, $f_\diamond = {\le_A}\cdot f_\ast\cdot {\le_B}$ and $f^\diamond = {\le_B}\cdot f^\ast\cdot {\le_A}$.

[^embeddings]: - For example, starting with a monotone function $f:A\to B$, the two functors $f\mapsto f_o \mapsto (f_o)_\ast$ and $f\mapsto f_\diamond \mapsto (f_\diamond)_o$ do not commute since the latter does remember the order of $A$ and $B$. On the other hand, the corresponding diagram involving the discrete functor instead of the forgetful functor $(-)_o$ does commute.
- To highlight the difference between the $\ast$- and $\diamond$-embedding:
- Let $A=(A_o,\le)$ be an internal order. Then $(1,1)$ tabulates $\le_A$ in the sense that $1^\diamond\cdot 1_\diamond = {\le_A}$, but $1^\ast\cdot 1_\ast$ is the equality relation on $A_o$.
- Let $(p,q)$ tabulate the monotone relation $R$. ...

[^proposition]: See the proposition below for an example of a subtle interaction between reasoning in $Rel(\mathcal E)$ and $Rel(Ord(\mathcal E))$

[^strong-epi]: In the other direction, if a category has products, then strong epi in the usual sense implies strong epi in the sense of Carboni and Street. I don't know whether the converse holds in non-regular categories.

To prove "strong implies regular", we assume $e$ is a strong epi and $p,q$ its kernel pair (hence $p^\ast\cdot q_\ast=e_\ast\cdot e^\ast$) and $hp=hq$. We define the unique map from $e$ to $h$ as $e^\ast\cdot h_\ast$. Uniqueness follows from $e$ epi. It remains to show that $e^\ast\cdot h_\ast$ is map. Being in $Rel(\mathcal E)$ it suffices to show that $e^\ast\cdot h_\ast \dashv h^\ast\cdot e_\ast$, which is a straightforward calculation.