Michael wrote:
> I am having a hard time understanding strong monoidal monotone functions. This seems to be a paradox for me (like this water is both hot and cold). Does anyone have an example of one that can clarify how this can happen?
I'm guessing what seemed "paradoxical" was having
\[ f(x) \otimes f(x) \le f(x \otimes x') \textrm{ and } I \le f(I) \]
and also
\[ f(x) \otimes f(x) \ge f(x \otimes x') \textrm{ and } I \ge f(I) \]
yet still not having
\[ f(x) \otimes f(x) = f(x \otimes x') \textrm{ and } I = f(I). \]
Presumably this was because you're used to _posets_, where \\(x \le y \\) and \\(y \le x\\) imply \\(x = y\\). But in a _preorder_ this needn't be true.
So, you need to understand preorders that aren't posets. Here is the easiest example: take a set \\(X\\) and decree that _everything_ in this set is less than or equal to _everything else_. Then the laws of a preorder hold: check them in your mind, and if you don't instantly remember what these laws are, go to jail and stay there until you do! But the law that makes a preorder a poset:
\[ \textrm{ if } x \le y \textrm{ and } y \le x \textrm{ then } x = y \]
obviously does _not_ hold.
So, this kind of preorder, very far from being a poset, is good to keep in mind.
Let's use this kind to get a monotone map that's strong monoidal but not strict monoidal.
**Answer to Puzzle 82.** Let \\(X\\) and \\(Y\\) be monoids and let \\(f : X \to Y\\) be a function that's _not_ a homomorphism: for example,
\[ f(x \otimes x') \ne f(x) \otimes f(x') \]
for some \\(x,x' \in X\\). Examples of this are a dime a dozen: just take your favorite two monoids with lots of elements and take some random idiotic function between them: it probably won't make \\(f(x \otimes x') = f(x) \otimes f(x')\\) for all \\(x,x' \in X\\).
Now, make \\(X\\) into a preorder in the silly way I just described: decree that _everything_ is less than or equal to _everything_. Do the same for \\(Y\\).
Then it's easy to see that \\(X\\) and \\(Y\\) are monoidal preorders. For example \\(X\\) obeys
\[ x_1 \le x_1' \textrm{ and } x_2 \le x_2' \textrm{ imply } x_1 \otimes x_2 \le x_1' \otimes x_2' \]
because _everything in \\(X\\) is less than or equal to everything else!_
Similarly, it's easy to see that \\(f: X \to Y\\) is lax monoidal. We have
\[ f(x) \otimes f(x) \le f(x \otimes x') \textrm{ and } I \le f(I), \]
because _everything in \\(Y\\) is less than or equal to everything else!_
We also know that \\(f\\) is oplax monoidal:
\[ f(x) \otimes f(x) \ge f(x \otimes x') \textrm{ and } I \ge f(I) \]
because _everything in \\(Y\\) is greater than or equal to everything else!_
So \\(f\\) is strong monoidal for very silly reasons. But it's not _strict_ monoidal, because we've set things up to ensure
\[ f(x \otimes x') \ne f(x) \otimes f(x') . \]
Get it?
The moral is that _sometimes_ in a preorder saying that one thing is less than or equal to another is saying _absolutely nothing_, because _everybody_ is less than or equal to _everybody_ else. So in a typical preorder, you should _never_ expect to reason from inequalities to equations. For that, you want a poset.
> I am having a hard time understanding strong monoidal monotone functions. This seems to be a paradox for me (like this water is both hot and cold). Does anyone have an example of one that can clarify how this can happen?
I'm guessing what seemed "paradoxical" was having
\[ f(x) \otimes f(x) \le f(x \otimes x') \textrm{ and } I \le f(I) \]
and also
\[ f(x) \otimes f(x) \ge f(x \otimes x') \textrm{ and } I \ge f(I) \]
yet still not having
\[ f(x) \otimes f(x) = f(x \otimes x') \textrm{ and } I = f(I). \]
Presumably this was because you're used to _posets_, where \\(x \le y \\) and \\(y \le x\\) imply \\(x = y\\). But in a _preorder_ this needn't be true.
So, you need to understand preorders that aren't posets. Here is the easiest example: take a set \\(X\\) and decree that _everything_ in this set is less than or equal to _everything else_. Then the laws of a preorder hold: check them in your mind, and if you don't instantly remember what these laws are, go to jail and stay there until you do! But the law that makes a preorder a poset:
\[ \textrm{ if } x \le y \textrm{ and } y \le x \textrm{ then } x = y \]
obviously does _not_ hold.
So, this kind of preorder, very far from being a poset, is good to keep in mind.
Let's use this kind to get a monotone map that's strong monoidal but not strict monoidal.
**Answer to Puzzle 82.** Let \\(X\\) and \\(Y\\) be monoids and let \\(f : X \to Y\\) be a function that's _not_ a homomorphism: for example,
\[ f(x \otimes x') \ne f(x) \otimes f(x') \]
for some \\(x,x' \in X\\). Examples of this are a dime a dozen: just take your favorite two monoids with lots of elements and take some random idiotic function between them: it probably won't make \\(f(x \otimes x') = f(x) \otimes f(x')\\) for all \\(x,x' \in X\\).
Now, make \\(X\\) into a preorder in the silly way I just described: decree that _everything_ is less than or equal to _everything_. Do the same for \\(Y\\).
Then it's easy to see that \\(X\\) and \\(Y\\) are monoidal preorders. For example \\(X\\) obeys
\[ x_1 \le x_1' \textrm{ and } x_2 \le x_2' \textrm{ imply } x_1 \otimes x_2 \le x_1' \otimes x_2' \]
because _everything in \\(X\\) is less than or equal to everything else!_
Similarly, it's easy to see that \\(f: X \to Y\\) is lax monoidal. We have
\[ f(x) \otimes f(x) \le f(x \otimes x') \textrm{ and } I \le f(I), \]
because _everything in \\(Y\\) is less than or equal to everything else!_
We also know that \\(f\\) is oplax monoidal:
\[ f(x) \otimes f(x) \ge f(x \otimes x') \textrm{ and } I \ge f(I) \]
because _everything in \\(Y\\) is greater than or equal to everything else!_
So \\(f\\) is strong monoidal for very silly reasons. But it's not _strict_ monoidal, because we've set things up to ensure
\[ f(x \otimes x') \ne f(x) \otimes f(x') . \]
Get it?
The moral is that _sometimes_ in a preorder saying that one thing is less than or equal to another is saying _absolutely nothing_, because _everybody_ is less than or equal to _everybody_ else. So in a typical preorder, you should _never_ expect to reason from inequalities to equations. For that, you want a poset.
Version 2.1.8p2
