Here’s one potential way of thinking about the condition symmetric monoidal
preorders place on their
ordering relation (p41, def 2.2, condition (a)). We use the context of enriched
categories. Let
V be a symmetric monoidal
preorder and let
C be a
V-enriched
category. Now consider the
diagram in
C:
For any two
objects x,
y, let
xy denote
C(x,y). Then by the second axiom of enriched
categories (p57, def 2.46) we have that
AB⊗BC≤ACand likewise that
CD⊗DE≤CE
We can motivate this by thinkin’ of
xy as giving some measure, perhaps, of “ease of traversing ‘from’
x ‘to’
y". Then the above make sense because the ease of going from
x to
y can never be more than the ease of a specific path
x→d→y.
By the same axiom we also have
AC⊗CE≤AE
We might naturally expect, additionally, for
AB⊗BC⊗CD⊗DE≤AC⊗CE
to hold. And indeed it does,
given that we adopt the symmetric monoidal
preorder condition
a≤a′∧b≤b′⟹a⊗b≤a′⊗b′(a)
Perhaps this example motivates this condition.
As an aside, this example can also be used to refute a tempting condition to place on symmetric monoidal
preorders. If we think of the arrows in the above
diagram as
representing, say, roads, then we expect all measures of ease to be negative (it always requires some work to move around in the world.)
Guided by this mental
model we would expect not just that
AB⊗BC⊗CD⊗DE≤AC⊗CE
hold but perhaps, stronger, that
AB⊗BC≤AC⊗CE(⋆)
We know that going
A→B→C is at
least as difficult as going
A→C, so should it not also be at
least as difficult as going
A→C→E?
The trouble is that in a generic symmetric monoidal
preorder not all values will be same-signed; ie, there may be inverses. So in the example above we might find, for instance, that in fact
CE>0; that is, traversing
C→E in fact does not require any work and in fact gives you
back energy!
This is the reason, I think, that the coherence condition for
≤ on symmetric monoidal
preorders is as weak as it is.
(If your symmetric
monoid does not have inverses then it’s my bet that in fact you get as a theorem that
a≤a⊗b, which entails the above condition
(⋆))