Product Preorder

definition example

Given preorders $(P,\le )$ and $(Q,\le )$, the product preorder on the product set $P\times Q$ has $(p,q)\le (p^{\prime },q^{\prime })$ iff $p\le p^{\prime }$ and $q\le q^{\prime }$. This is a basic example of the product of categories.

Sources: 7 Sketches Example 1.56, Exercise 1.57; §2.4.3 (product $\mathcal{V}$-categories); CTfS Example 4.5.1.2, Exercises 4.5.1.3–4.5.1.4

Example (7S Exercise 1.57): the product of $b\ge a\le c$ with $1\le 2$ has six elements $(a,1)\le (a,2),(b,1),(c,1)\le (b,2),(c,2)$.

The product preorder is the Product of $P$ and $Q$ in the category $\mathbf{Preord}$ (Kittenlab-style: the projections are monotone and a monotone map into $P\times Q$ is a pair of monotone maps). Meets and joins in $P\times Q$ are computed componentwise. For monoidal preorders, the product of two $\mathcal{V}$-categories uses $\otimes$ on hom-objects (7 Sketches §2.4.3).

JuliaLeanHaskell

Docs: Vignette: preorders

Builds on: Preorder (Preorder) — run that note’s Julia code first.

struct ProductPreorder{S,T,P<:Preorder{S},Q<:Preorder{T}} <: Preorder{Tuple{S,T}}
  p::P; q::Q
end
leq(pq::ProductPreorder, x, y) = leq(pq.p, x[1], y[1]) && leq(pq.q, x[2], y[2])

-- Mathlib: `Prod.instPreorder` is exactly the componentwise order
example {α β : Type} [Preorder α] [Preorder β] (a a' : α) (b b' : β) :
    (a, b) ≤ (a', b') ↔ a ≤ a' ∧ b ≤ b' := Prod.le_def

instance (Preorder a, Preorder b) => Preorder (a, b) where
  leq (p, q) (p', q') = leq p p' && leq q q'