Opposite Preorder

definition

Given a Preorder $(P,\le )$, the opposite preorder $(P,{\le }^{\mathrm{op}})$ has the same elements, with $p{\le }^{\mathrm{op}}q$ iff $q\le p$.

Sources: 7 Sketches Example 1.58, 1.72, Exercise 1.66; DaoFP §8.1 (opposite categories), §5.2 (duality).

• The identity is monotone $P\to P^{\mathrm{op}}$ iff $P$ is a Dagger Preorder (Example 1.72).
• The principal-upper-set map $\uparrow :P^{\mathrm{op}}\to \mathcal{U}(P)$ is monotone (7S Exercise 1.66) — a preorder Yoneda Embedding.
• Reversing the order swaps meets and joins, and swaps left and right adjoints in a Galois Connection. This is the preorder instance of the Opposite Category and of duality (“reversing the arrows”, DaoFP §3, §5.2): every statement about preorders has a dual obtained by replacing $\le$ with $\ge$.
• The reverse ordering on $\mathbb{N}$ (“like golf”) is ${\mathbb{N}}^{\mathrm{op}}$; the base $\mathbf{Cost}=([0,\infty ],\ge )$ of Lawvere metric spaces is $[0,\infty {]}^{\mathrm{op}}$.

JuliaLeanHaskell

Docs: Vignette: preorders

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

struct OppositePreorder{T,P<:Preorder{T}} <: Preorder{T}
  p::P
end
leq(op::OppositePreorder, x, y) = leq(op.p, y, x)

-- Mathlib: `OrderDual α` (notation αᵒᵈ) reverses the order
example {α : Type} [Preorder α] (a b : α) : OrderDual.toDual a ≤ OrderDual.toDual b ↔ b ≤ a :=
  OrderDual.toDual_le_toDual

newtype Op a = Op a
instance Preorder a => Preorder (Op a) where
  leq (Op x) (Op y) = leq y x
-- cf. Data.Ord.Down for Ord