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 morphisms between Day convolutions

Ralph Sarkis (Dec 10 2024 at 17:18):

I am trying to unroll a definition involving Day convolution, and I don't understand this operation enough to do what seem to me should be simple computations. It can be summarized in the following picture.
image.png

We work in the category $[\mathbf{C},\mathbf{Set}]$, where $\mathbf{C}$ is a symmetric strict monoidal category whose tensor is denoted $\otimes$, and $\star$ denotes the [[Day convolution]]. By universal properties, I know that the blue $\phi$ corresponds to a natural transformation $\phi^t$, and similarly, the green $\psi_1 \star \psi_2$ corresponds to a pair of natural transformations $\psi_1^t$ and $\psi_2^t$. The isomorphism denoted $\cong$ is built out of the associator and symmetries in the functor category, which are themselves inherited from the associators and symmetries in $\mathbf{C}$ and $\mathbf{Set}$. I would like to know if it is easy to describe the natural transformation that corresponds to the composite $\phi \circ (\psi_1 \star \psi_2) \circ {\cong}$, i.e. the orange arrow, in terms of the other natural transformations ($\phi^t$, $\psi_1^t$, and $\psi_2^t$).

From the context, I infer that it should be sending $(f_1,f_2,f_3,f_4)$ to $H(\cong)(\phi^t(\psi_1^t(f_1,f_3),\psi_2^t(f_2,f_4))$, where $\cong$ abusively denotes the isomorphism in $\mathbf{C}$ that associates and swaps like the functors (we omit the components of the natural transformations). I am trying to rigorously verify that.

I tried to abstract away from my context to make the question more approachable, but I can try to decompose it in two subquestions if you this one is still too complex.

Morgan Rogers (he/him) (Dec 11 2024 at 08:46):

There aren't a lot of things that will typecheck and use all of the data at hand, so it seems like you're on the right track? To be honest it's not quite clear where you're stuck.

Ralph Sarkis (Dec 11 2024 at 12:35):

I am missing the step from pre-rigorous to rigorous. I got on the right track simply by typechecking, but I don't know why the thing I obtained works. For example, in the following simpler diagram, how do I prove the equation with the question mark I wrote ? The symmetry $\sigma_{G_1,G_2}$ is defined by an isomorphism of coends, and I don't see how to prove that the thing that typechecks is the natural transformation corresponding to the composition with that isomorphism.
image.png