# Order-regular categories

For background on order enriched category theory see [here](https://hackmd.io/@alexhkurz/BywmMN9G8).

The following definition is taken from [Kurz-Velebil](https://alexhkurz.github.io/papers/Ordered-algebras.pdf) Def 3.18, but see also Remark 3.4.

**Definition:** A category is *order-regular* if

- the category has finite limits (in the $Pos$-enriched sense),
- P-regular epis and P-monos form a factorisation system,
- P-regular epis are stable under pullback.

**Remark:** If the category in quesiton has a P-faithful (ie order-reflecting on homsets) functor to $Pos$, then the 2-dimensional property of item 3 comes for free.

**Example:** $Pos$ is order-regular but not regular (since regular epis, as opposed to P-regular epis, are not stable under pullbacks in $Pos$).

**Remark:** Stability under pullbacks is needed in various places. For example, to show that composition of relations is associative (Borceux Vol.?,??).

The above definition of an order-regular category does not tell us how to prove that regular P-epis and P-monos form a factorisation system. For this reason, the definition of regular category is usually formulated differently. But before we state this as a proposition, we collect in a remark some properties needed in the proof that the two definitions are equivalent.

**Remark:** The following is entirely analogous to the ordinary case. (CHECK again)
1. If a coinserter has a P-kernel, then the coinserter is the coinserter of its P-kernel. (Compare with Borceux Vol.1, 2.5.7.)
2. If a P-kernel has a coinserter, then the P-kernel is the P-kernel of that P-regular epi. (Compare with Borceux Vol.1, 2.5.8.)
3. In an order-regular category, every P-kernel has a coinserter.
4. The composition of two P-regular epis is a P-epi. (Compare with Borceux Vol.1, 1.8.2.)
5. If $f:A\to B$ is a P-regular epi and $g:B\to C$, then the canonical arrow from the P-kernel of $g\circ f$ to the P-kernel of $g$ is epi, provided that P-regular epis are stable under pullbacks. (Compare with Borceux Vol.2, 2.1.2.)

**Proposition:** (CHECK AGAIN) A $Pos$-category is order-regular iff
- it is finitely complete (in the $Pos$-enriched sense),
- every P-kernel has a coinserter,
- regular P-epis are stable under pullbacks.

*Proof:* The proof should follow the one in the ordinary case, see the previous remark.
- First, we show that if we factor $f$ as $m\circ e$ where $e$ is the coinserter of the P-kernel pair of $f$, then $m$ is $P$-mono.

- Second, we show that if we factor $f$ as $m\circ e$ with $e$ a P-regular epi, then $e$ is the coinserter of the P-kernel pair of $f$.

Consequently, P-regular epi and P-mono factorisations are unique up to unique isomorphism. It follows (see Adamek-Herrlich-Strecker, 14.7) that P-regular epi and P-monos constitute a factorisation system. QED.