Monotone Map

definition example theorem proof

A monotone map between preorders $(A,{\le }_A)$ and $(B,{\le }_B)$ is a Function $f:A\to B$ such that for all $x,y\in A$, if $x{\le }_{A}y$ then $f(x){\le }_{B}f(y)$. Kittenlab calls these order-preserving maps. Monotone maps are the structure-preserving maps for preorders: 7 Sketches thinks of them as observations of one system by another.

Sources: 7 Sketches Definition 1.59, Examples 1.60–1.64, 1.68, Propositions 1.70, 1.78, Exercises 1.67, 1.71, 1.77; Kittenlab Lecture 5, 7; DaoFP §20.1; CTfS Definition 3.4.3.1, Example 3.4.3.2, Application 3.4.3.3, Exercises 3.4.3.4, 3.4.4.11, 4.1.1.8

Examples

• $\mathbb{B}\to \mathbb{N}$, $\mathsf{false}\mapsto 17$, $\mathsf{true}\mapsto 24$ (Example 1.60).
• The Tree of Life map from classifications to taxonomic ranks (Example 1.61).
• Cardinality $|\cdot |:\mathcal{P}(X)\to \mathbb{N}$ (Example 1.62).
• The inclusion $\mathcal{U}(P)\to \mathcal{P}(P)$ of upper sets into the Power Set (Example 1.64).
• Pullback of partitions $f^{\ast }:\mathrm{Prt}(Y)\to \mathrm{Prt}(X)$ along a surjection $f:X\twoheadrightarrow Y$, $s\mapsto f;s$ (Example 1.68); see Pushforward and Pullback of Partitions.
• Every function out of a Discrete Preorder is monotone (7S Exercise 1.67).
• Monotone maps $P\to \mathbb{B}$ are the same as upper sets (Upper Sets Classified by Maps to Bool).
• The connectivity observation $\Phi :\mathrm{Prt}(\{\bullet ,\circ ,\ast \})\to \mathbb{B}$ (7S Exercise 1.77) — monotone but with a Generative Effect.

Scientific hypotheses as monotone maps (CTfS Application 3.4.3.3). “A team is only as strong as its weakest member” — is a material only as strong as its weakest constituent? Order materials by constituency ($m{\le }_C{m}^{\prime }$ if $m$ is an ingredient of $m^{\prime }$) and by strength ($m{\le }_S{m}^{\prime }$ if $m^{\prime }$ is stronger). The hypothesis is precisely that the identity is a monotone map $(M,{\le }_C)\to (M,{\le }_S^{\mathrm{op}})$. Other CTfS examples: taking images $\mathcal{P}(X)\to \mathcal{P}(Y)$ and preimages $\mathcal{P}(Y)\to \mathcal{P}(X)$ along a function (CTfS Example 3.4.3.2, Exercise 3.4.3.4); assigning to each region of the earth its range of recorded temperatures (Join). Counting: there are $\left(\genfrac{}{}{0ex}{}{m+n+1}{m+1}\right)$ monotone maps $[m]\to [n]$ between the linear orders $\{0<\cdots <m\}$ and $\{0<\cdots <n\}$ — e.g. 4 maps $[0]\to [3]$, one map $[3]\to [0]$ and 20 maps $[2]\to [3]$ (CTfS Exercise 4.1.1.8, Simplex Category).

Monotone maps are functors (Kittenlab Lecture 5)

Proposition. A Functor between preorders $X$ and $Y$ viewed as categories is exactly a function $F:X\to Y$ with $x\le x^{\prime }$ implying $F(x)\le F(x^{\prime })$.

Proof. A morphism $x\to y$ must be sent to a morphism $F(x)\to F(y)$, and since there is at most one morphism between any two objects, $F$ automatically preserves composites and identities. $■$

Proposition 1.70. The Identity Function is monotone, and the composite $f;g$ of monotone maps is monotone (7S Exercise 1.71). Hence preorders and monotone maps form a category $\mathbf{Preord}$ (Kittenlab: $\mathsf{Preorder}$), a full Subcategory of $\mathbf{Cat}$; see Category of Preorders.

Some functors involving $\mathbf{Preord}$ (Kittenlab):

1. $\mathbf{Preord}\to \mathbf{Cat}$, view a preorder as a category;
2. $\mathbf{Cat}\to \mathbf{Preord}$, the Preorder Reflection: $x\le y$ iff $\mathrm{Hom}(x,y)\ne \varnothing$;
3. $\mathbf{Preord}\to \mathbf{Set}$, the underlying set;
4. $\mathbf{Set}\to \mathbf{Preord}$, the Discrete Preorder;
5. $\mathbf{Set}\to \mathbf{Preord}$, the Codiscrete Preorder.

Between monotone maps $f,g:P\to Q$ there is at most one Natural Transformation, existing iff $f(x)\le g(x)$ for all $x$ (Lecture 7).

Preservation

A monotone map may or may not preserve meets and joins (Preservation of Meets and Joins); failing to preserve joins is a Generative Effect. Monotone maps that preserve all meets are exactly right adjoints of Galois connections (Adjoint Functor Theorem for Preorders). Between monoidal preorders the right notion is a Monoidal Monotone Map; between metric spaces, monotone maps become $\mathbf{Cost}$-functors, i.e. distance-non-increasing maps.

JuliaLeanHaskell

Docs: Vignette: preorders — Kittenlab Lecture 5

Builds on: Bool (Monoidal Preorder) (BoolPre), Natural Numbers (UsualOrder) — run those notes’ Julia code first.

# check monotonicity on finite preorders (Kittenlab-style `leq`)
is_monotone(pA, pB, f, xs) = all(!leq(pA, x, y) || leq(pB, f(x), f(y)) for x in xs, y in xs)
 
# Example 1.60: Bool → ℕ
f(b) = b ? 24 : 17
is_monotone(BoolPre(), UsualOrder(), f, [false, true])   # true

#check @Monotone     -- ∀ ⦃a b⦄, a ≤ b → f a ≤ f b
example : Monotone (fun n : ℕ => n + 5) := fun _ _ h => Nat.add_le_add_right h 5
-- monotone maps compose; bundled as `OrderHom` (notation α →o β)
#check @Monotone.comp
#check (OrderHom ℕ ℕ)
-- monotone maps are functors between the thin categories
example {α β : Type} [Preorder α] [Preorder β] (f : α →o β) :
    CategoryTheory.Functor α β := f.monotone.functor

-- a monotone map is a function with a promise (unenforced): leq x y ==> leq (f x) (f y)
newtype Monotone a b = Monotone (a -> b)
 
isMonotoneOn :: (Preorder a, Preorder b) => [a] -> (a -> b) -> Bool
isMonotoneOn xs f = and [ not (leq x y) || leq (f x) (f y) | x <- xs, y <- xs ]
 
-- Example 1.60
ex160 :: Bool -> Int
ex160 False = 17
ex160 True  = 24