Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: composing universal property morphisms

David Egolf (Dec 05 2023 at 20:51):

I'm currently contemplating this rather impressive diagram (from "Categorical logic from a categorical point of view" by Michael Shulman):
diagram

In this diagram, many of the morphism pictured are induced by using the universal property of products. To try and show that different polygons in this diagram commute I think involves calculating the composite of these "universal property morphisms". For example, we'd like to be able to show that $(i \times 1 \times 1) \circ (\Delta \times 1) \circ (1,j) = (i,1,j)$.

I think I've figured out an approach that works, but I would like to try and formalize it a bit so that I can use it more easily. I drew this rough diagram to illustrate the approach:
rough diagram

David Egolf (Dec 05 2023 at 20:53):

In this diagram $A$, $B$ and $B'$ are objects, while $D$ and $D'$ are diagrams. The fancy wider arrows are supposed to indicate that there are potentially multiple parallel morphisms present. Since we want to use the universal property of a limit, the idea is that $B$ and $B'$ (together with their projecting morphisms) are limits over the diagrams $D$ and $D'$, respectively.

David Egolf (Dec 05 2023 at 20:53):

For each object $d$ in $D$, there is exactly one morphism in $f$ from $A$ to $d$. In addition, the morphisms $g$ from $D$ to $D'$ are such that when composed with the morphisms $\pi$ from $B$ to $D$, there is exactly one morphism in the composite to each object of $D'$ from $B$.

David Egolf (Dec 05 2023 at 20:53):

The dashed arrows indicate morphisms induced by the universal property of the limits involved. The dashed arrow $u_f$ indicates the morphism induced by by the morphisms $f$, and $u_g$ is the morphism induced by the morphisms $g \circ \pi$.

Since each path in the left triangle commutes (we might say $\pi \circ u_f = f$) and each path in the right rectangle commutes (we might say $g \circ \pi = \pi' \circ u_g$) I think each path in the larger "outside" diagram commutes (so $g \circ f = \pi' \circ u_g \circ u_f$). I think this implies that $u_g \circ u_f$ is the universal property morphism $u_{g \circ f}$ induced by $g \circ f$.

David Egolf (Dec 05 2023 at 20:54):

So, to form the composite of two morphisms $u_f$ and $u_g$ induced by universal properties, I think one takes the universal property morphism induced by the "composite" of their inducing sets of morphisms $f$ and $g$. (Although, note that $\pi$ was involved in induced $u_g$, not just the morphisms $g$.)

Does this seem like it should work? I'd also be interested in learning how to formalize this cleanly. I'm not used to thinking about "composing" collections of parallel morphisms!

David Egolf (Dec 05 2023 at 21:19):

I guess one limitation of this approach is that it assumes the inducing morphisms for the second universal morphism (from $B$ to $B'$) all "factor through" the diagram $D$. I don't think is necessarily always the case.

To handle a more general situation, probably a relevant diagram would look more like this:
more general diagram

In this diagram we don't assume that the morphisms inducing the second universal morphism factor through $D$.

In this more general case we'd have $\pi' \circ u_g \circ u_f = g \circ u_f$. I guess that in this case $u_g \circ u_f$ is the universal property morphism induced by $g \circ u_f$.