Regarding the following…

If $f: X \to Y$ is a function between finite sets, then $\left| X \times_{f} X \right| \geq \left| X \right|^{2} / \left| Y \right|$.

…perhaps it may be helpful to try to write down in a reasonably direct way *any* monomorphism $X^{2} \rightarrow Y \times \left( X \times_{f} X \right)$, whether or not it is immediately category theoretic. To this end, I wonder if the following works.

As a preliminary step, for any pair $(y, y') \in Y \times Y$ such that $\left| f^{-1}(y) \right| \leq \left| f^{-1}(y') \right|$, choose any monomorphism $f^{-1}(y) \rightarrow f^{-1}(y')$, and denote it by $i_{y,y'}$.

Take $(x_1, x_2) \in X^{2}$. Suppose that $\left| f^{-1} \left( f(x_1) \right) \right| \lt \left| f^{-1} \left( f(x_2) \right) \right|$. In this case, send $(x_1, x_2)$ to $\left( f(x_1), \left( i_{f(x_1), f(x_2)}(x_1), x_2 \right) \right)$. Otherwise, namely if $\left| f^{-1} \left( f(x_1) \right) \right| \geq \left| f^{-1} \left( f(x_2) \right) \right|$, send $(x_1, x_2)$ to $\left( f(x_1), \left( x_1, i_{f(x_2), f(x_1)}(x_2) \right) \right)$.

I think that this defines a monomorphism. To see this, take $(x_1, x_2)$ and $(x_1', x_2')$ in $X^{2}$ which map to the same thing in $Y \times \left( X \times_{f} X \right)$. Observe first that it is impossible that $\left| f^{-1} \left( f(x_1) \right) \right| \lt \left| f^{-1} \left( f(x_2) \right) \right|$ but that $\left| f^{-1} \left( f(x_1') \right) \right| \geq \left| f^{-1} \left( f(x_2') \right) \right|$. Indeed, we would then have that $f(x_1) = f(x_1')$, and also that $i_{f(x_1), f(x_2)}(x_1) = x_1'$. But $i_{f(x_1), f(x_2)}(x_1)$ is in $f^{-1}\left(f(x_2) \right)$ whereas $x_1'$ is in $f^{-1}\left( f(x_1') \right) = f^{-1}\left( f(x_1) \right)$, so we would then have that $f(x_2) = f(x_1)$, which contradicts our assumption that $\left| f^{-1} \left( f(x_1) \right) \right| \lt \left| f^{-1} \left( f(x_2) \right) \right|$.

An entirely analogous argument demonstrates that it is impossible that $\left| f^{-1} \left( f(x_1) \right) \right| \geq \left| f^{-1} \left( f(x_2) \right) \right|$ but that $\left| f^{-1} \left( f(x_1') \right) \right| \lt \left| f^{-1} \left( f(x_2') \right) \right|$. Indeed, we would then have that $f(x_1) = f(x_1')$, and also that $i_{f(x_1'), f(x_2')}(x_1') = x_1$, from which, as above, we would be able to deduce that $f(x_2') = f(x_1')$, contradicting our assumption that $\left| f^{-1} \left( f(x_1') \right) \right| \lt \left| f^{-1} \left( f(x_2') \right) \right|$.

Suppose now that $\left| f^{-1} \left( f(x_1) \right) \right| \lt \left| f^{-1} \left( f(x_2) \right) \right|$ and that $\left| f^{-1} \left( f(x_1') \right) \right| \lt \left| f^{-1} \left( f(x_2') \right)\right|$. Then $x_2 = x_2'$, and moreover $f(x_1) = f(x_1')$ and $i_{f(x_1), f(x_2)}(x_1) = i_{f(x_1'), f(x_2')}(x_1')$. Putting all of these facts together, we obtain that $i_{f(x_1), f(x_2)}(x_1) = i_{f(x_1), f(x_2)}(x_1')$, which, since $i_{f(x_1), f(x_2)}$ is a monomorphism, implies that $x_1 = x_1'$. Hence $(x_1, x_2) = (x_1', x_2')$, as required.

An entirely analogous argument demonstrates that $(x_1, x_2) = (x_1', x_2')$ also holds if $\left| f^{-1} \left( f(x_1) \right) \right| \gt \left| f^{-1} \left( f(x_2) \right) \right|$ and $\left| f^{-1} \left( f(x_1') \right) \right| \gt \left| f^{-1} \left( f(x_2') \right) \right|$.

Finally, if $\left| f^{-1} \left( f(x_1) \right) \right| = \left| f^{-1} \left( f(x_2) \right) \right|$ and $\left| f^{-1} \left( f(x_1') \right) \right| = \left| f^{-1} \left( f(x_2') \right) \right|$, then it is immediate that $(x_1, x_2) = (x_1', x_2')$, as required.

How ‘category theoretic’ is this monomorphism? Actually I think it *is* constructible category theoretically. We have (purely category theoretically) that $X^{2}$ is isomorphic to $\bigsqcup_{y \in Y} \bigsqcup_{y' \in Y} f^{-1}(y) \times f^{-1}(y')$. Thus it suffices to construct a map $f^{-1}(y) \times f^{-1}(y') \rightarrow Y \times \left( X \times_{f} X \right)$ for every $(y,y') \in Y^{2}$. To do this in the way I did above, the only thing one really needs is that one of $\left| f^{-1}(y) \right| \lt \left| f^{-1}(y') \right|$, $\left| f^{-1}(y) \right| \gt \left| f^{-1}(y') \right|$, or $\left| f^{-1}(y) \right| = \left| f^{-1}(y') \right|$ must hold. If one defines all of the ingredients in the last sentence in a category theoretic way (e.g. defining a finite set to be one isomorphic to $\bigsqcup_{n} 1$ for some $n \in \mathbb{N}$, where $1$ is a one element set), this will reduce to the fact that, for any pair of natural numbers $n$ and $n'$, one of $n \leq n'$, $n \geq n'$, or $n = n'$ must hold, which will be perfectly true when working category theoretically as well. Once one has this, everything else in my definition of the map is straightforwardly expressible ‘category theoretically’ (in terms of arrows between sets), as is the proof that we have a monomorphism.

I think it would be naïve to imagine that one can construct a monomorphism by only some immediate application of some ‘doctrinal’ properties of the category of sets. The formulation of the problem only really makes sense because of the fact that one can express a finite set as a coproduct of $1$’s, so I think one has to expect a non-trivial result to dig down to that level. This does not preclude of course that it might be possible to formulate some useful greater level of generality in which one can carry out the same kind of argument.

This is all off the cuff, so I hope I have not made some egregious error(s); apologies in advance if so! I have not thought about how this argument relates to usual proofs of the Cauchy-Schwartz inequality, I just came up with it directly.

## Re: The Two Cultures Challenge Revisited

Maybe we can categorify the argument by replacing the inequality $|X\times Y|+|Y\times X|\leq|X\times X|+|Y\times Y|$ by the set of injections $Inj(X\times Y + Y\times X,X\times X + Y\times Y)$?

The overall form of the “proof” would be a map (what kind?)

$In