Post History

To further emphasize the "fake difficulty", we can show that most of this proof is completely "formal", in that it holds for very general reasons that have little to do with real numbers. See the bottom for a detailed, elementary proof that explicitly illustrates that the proof is almost entirely a manipulation of definitions and basic logic.

----

Let $\mathcal C$, $\mathcal D$, and $\mathcal E$ be arbitrary categories and $\odot : \mathcal D \times \mathcal E \to \mathcal C$ be a bifunctor. Write $\int^{I : \mathbb I} D(I)$ for the colimit of the diagram $D$ which is just a functor from some small category $\mathbb I$ to another category. If $\odot$ is cocontinuous in both arguments, then $$\left(\int^{I:\mathbb I}D_1(I)\right) \odot \left(\int^{J:\mathbb J}D_2(J)\right) \cong \int^{(I, J) : \mathbb I \times \mathbb J} D_1(I)\odot D_2(J)$$

All left adjoints are cocontinuous, so it would suffice to show that both $({-})\odot E$ and $D \odot ({-})$ are left adjoints for all $E \in \mathrm{Ob}(\mathcal E)$ and $D \in \mathrm{Ob}(\mathcal D)$.

All these facts are easily provable facts of basic category theory and coend calculus.

Now, let's instantiate it. Given any partially ordered set, $S$, we can make a category whose objects are the elements of $S$ and whose hom-sets have at most one arrow with $\mathrm{Hom}(s, s')$ being non-empty exactly when $s \leq s'$. A functor between such categories is exactly a monotonic function. The supremum of $A \subseteq S$ is the colimit of the diagram $\mathsf D A \to S$ where $\mathsf D$ turns a set into a discrete category, and we're identifying the partially ordered set with its corresponding category.

We'll choose $S = \mathbb R^{+}$, the set of positive reals with the usual ordering. We'll define $\odot : \mathbb R^+ \times \mathbb R^+ \to \mathbb R^+$ to be $x \odot y = xy$. To be a (bi)functor, it must be monotonic in each argument which is a basic fact of real number multiplication (for *positive* numbers). $\odot$ is obviously commutative, so we can complete our proof if we show that $x \odot ({-})$ is a left adjoint which it is via the right adjoint $({-})/x$. The adjunction condition is simply $$xy \leq z \iff y \leq z/x$$ for all $x$, $y$, and $z$ in $\mathbb R^+$ which is, again, a basic fact of (positive) real numbers.

Obviously it would be silly to go through these general results that have to track a bunch of detail that is degenerate in this example. My point is 1) the core pieces of the proof generalize massively if appropriately formulated, and 2) taking this abstract perspective and having a good handle on categorical intuitions can feed back into elegant proofs and a start to teaching categorical intuitions. In fact, a lot of the useful *logical* relations can be motivated by categorical intuitions. For example, below we'll use $(\exists x.P(x)) \to Q \iff \forall x. P(x) \to Q$ which is just continuity of right adjoints, and indiscernability of identicals is a special case of the Yoneda lemma.

Here's the proof I'd actually present in an undergrad class. (Well, I'd probably not present it in such detail.)

----

First, I'd define the supremum (in general) via the following, for $A \subseteq S$ for a partially ordered set, $S$, $\sup A$ is the unique element of $S$ satisfying $$\sup A \leq z \iff \forall a \in A. a \leq z$$ for all $z \in S$ which is a natural definition (and secretly is also the representability formulation of coproducts/colimits).

As lemmas, we'd have $ab \leq z \iff a \leq z/b$ (exercise; this is the only vaguely $\mathbb R^+$-specific result here) and

$$\begin{flalign}
\sup (A\cdot B) \leq z
& \iff \forall x \in (A \cdot B). x \leq z \tag{definition of $\sup$} \\
& \iff \forall x. (x \in (A \cdot B)) \to x \leq z \tag{expand shorthand} \\
& \iff \forall x. (\exists a \in A. \exists b \in B. x = ab) \to x \leq z \tag{definition of $A \cdot B$} \\
& \iff \forall x. \forall a \in A. \forall b \in B. (x = ab) \to x \leq z \tag{$(\exists x.P(x)\to Q \iff \forall x. P(x) \to Q$} \\
& \iff \forall a \in A. \forall b \in B. \forall x. (x = ab) \to x \leq z \tag{commutativity of $\forall$}\\
& \iff \forall a \in A. \forall b \in B. ab \leq z \tag{indiscernibility of identicals}
\end{flalign}$$

The proof is then:

$$\begin{flalign}
(\sup A)(\sup B) \leq z
& \iff \sup A \leq z/(\sup B) \tag{lemma} \\
& \iff \forall a \in A. a \leq z/(\sup B) \tag{definition of $\sup$}\\
& \iff \forall a \in A. a(\sup B) \leq z \tag{lemma} \\
& \iff \forall a \in A. (\sup B) \leq z/a \tag{commutativity, lemma} \\
& \iff \forall a \in A. \forall b \in B. b\leq z/a \tag{definition of $\sup$} \\
& \iff \forall a \in A. \forall b \in B. ab \leq z \tag{commutativity, lemma} \\
& \iff \sup (A\cdot B) \leq z \tag{other lemma}
\end{flalign}$$

To get $(\sup A)(\sup B) = \sup A\cdot B$ simply choose $z$ to be $(\sup A)(\sup B)$ and $\sup A\cdot B$.