Monoidal Monotone Map

definition example

Let $\mathcal{P}=(P,{\le }_P,I_P,{\otimes }_P)$ and $\mathcal{Q}=(Q,{\le }_Q,I_Q,{\otimes }_Q)$ be monoidal preorders. A monoidal monotone from $\mathcal{P}$ to $\mathcal{Q}$ is a Monotone Map $f:(P,{\le }_P)\to (Q,{\le }_Q)$ such that

(a) $I_Q{\le }_{Q}f(I_P)$, and (b) $f(p_1){\otimes }_{Q}f(p_2){\le }_{Q}f(p_1{\otimes }_P{p}_2)$ for all $p_1,p_2\in P$.

It is strong if (a′) $I_Q\cong f(I_P)$ and (b′) $f(p_1){\otimes }_{Q}f(p_2)\cong f(p_1{\otimes }_P{p}_2)$, and strict if these hold with $=$. Monoidal monotones are the preorder case of (lax) monoidal functors (7 Sketches Definition 6.68, DaoFP §14.9); reversing the inequalities gives oplax monoidal monotones.

Sources: 7 Sketches Definition 2.41, Example 2.42, 2.65, Exercises 2.43–2.45, 2.68; Construction 2.64.

Examples

• $i:(\mathbb{N},\le ,0,+)\to (\mathbb{R},\le ,0,+)$, $n\mapsto n$: strict.
• $\lfloor -\rfloor :(\mathbb{R},\le ,0,+)\to (\mathbb{N},\le ,0,+)$: monoidal monotone since $\lfloor x\rfloor +\lfloor y\rfloor \le \lfloor x+y\rfloor$, but not strong: $\lfloor 0.5\rfloor +\lfloor 0.5\rfloor \ne \lfloor 1\rfloor$.
• $g:\mathbf{Bool}\to \mathbf{Cost}$, $\mathsf{false}\mapsto \infty$, $\mathsf{true}\mapsto 0$: strict (7S Exercise 2.43).
• $d,u:\mathbf{Cost}\to \mathbf{Bool}$, $d(x)=[x=0]$ and $u(x)=[x<\infty ]$: both strict (7S Exercise 2.44); via Change of Base they turn Lawvere metric spaces into preorders in two different ways (7S Exercise 2.68).
• The constant map $n\mapsto 1$ is the unique monoidal monotone $(\mathbb{N},\le ,0,+)\to (\mathbb{N},\le ,1,\ast )$ (7S Exercise 2.45).

Use

A monoidal monotone $f:\mathcal{V}\to \mathcal{W}$ converts $\mathcal{V}$-categories into $\mathcal{W}$-categories (Change of Base): condition (a) makes identities work, (b) makes composition work. Monoidal preorders and monoidal monotones form a category; strong monoidal monotones that are isomorphisms of preorders are isomorphisms of monoidal preorders.

JuliaLeanHaskell

Docs: Vignette: monoidal preorders & SMCs

Builds on: Bool (Monoidal Preorder) (BoolPre), Cost (CostPre), Monotone Map (is_monotone) — run those notes’ Julia code first.

# check the lax monoidal conditions on finite samples
function is_monoidal_monotone(P, Q, f, ps)
  cond_a = leq(Q, munit(Q), f(munit(P)))
  cond_b = all(leq(Q, otimes(Q, f(p1), f(p2)), f(otimes(P, p1, p2))) for p1 in ps, p2 in ps)
  is_monotone(P, Q, f, ps) && cond_a && cond_b
end
g(b::Bool) = b ? 0.0 : Inf           # Bool → Cost
is_monoidal_monotone(BoolPre(), CostPre(), g, [false, true])   # true

-- Mathlib: a monotone monoid hom between ordered monoids is a strict monoidal monotone
#check OrderMonoidHom          -- α →*o β : monoid hom that is also monotone
-- lax version, by hand:
structure LaxMonoidalMonotone (P Q : Type) [OrderedCommMonoid P] [OrderedCommMonoid Q] where
  toFun : P → Q
  mono : Monotone toFun
  unit : 1 ≤ toFun 1
  mul : ∀ p₁ p₂, toFun p₁ * toFun p₂ ≤ toFun (p₁ * p₂)

-- a (lax) monoidal monotone: monotone, with mempty <= f mempty and f p <> f q <= f (p <> q)
newtype MonoidalMonotone p q = MonoidalMonotone (p -> q)
 
boolToCost :: All -> Cost
boolToCost (All True)  = Fin 0
boolToCost (All False) = Inf