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: Proarrow equipments

Jana Nickel (May 10 2025 at 07:54):

I am trying to understand this wonderful blog post about proarrow equipments written by Mike Shulman. However, when constructing the companion B(1,f) of f, I do not see why the horizontal composite square.jpg coincides with the identity square of B(1,f). If I understood it correctly, the horizontal identity morphisms are not necessarily strict, so why should the horizontal composite B(1,f) U_A from A to B be equal to B(1,f)?

Jana Nickel (May 10 2025 at 07:55):

I would be very grateful for any hint. Many thanks in advance!

Bryce Clarke (May 10 2025 at 08:13):

I’m general, these horizontal morphisms won’t be equal

Bryce Clarke (May 10 2025 at 08:14):

In the diagram you attached, one should really paste with the unitors on the top and bottom, and ask that the resulting cell is an identity instead

Bryce Clarke (May 10 2025 at 08:16):

In many double categories, one can choose the horizontal identity morphisms so that they behave strictly, so many authors make this assumption implicitly.

Bryce Clarke (May 10 2025 at 08:17):

It also happens that people just omit the unions and associators when drawing these diagrams, mainly to avoid clutter, knowing that the reader can substitute them in where necessary.

Jana Nickel (May 10 2025 at 08:24):

Thank you!

Mike Shulman (May 10 2025 at 15:23):

Bryce Clarke said:

In many double categories, one can choose the horizontal identity morphisms so that they behave strictly, so many authors make this assumption implicitly.

A fun fact is that it's actually always possible to redefine the composition so that the units are strict. Define the new composite $M\odot' N$ to be $N$ if $M$ is an identity, and $M$ if $N$ is an identity, and the original $M\odot N$ otherwise. The first two cases agree when they overlap, and the result is isomorphic to the original $M\odot N$ by the original unitors, so you can transport the associators across those isomorphisms. (This works for bicategories too, and monoidal categories, etc.)

And, of course, by changing the morphisms you can replace the whole double category by a strict one.

Jana Nickel (May 10 2025 at 21:26):

Mike Shulman schrieb:

Bryce Clarke said:

In many double categories, one can choose the horizontal identity morphisms so that they behave strictly, so many authors make this assumption implicitly.

A fun fact is that it's actually always possible to redefine the composition so that the units are strict. Define the new composite $M\odot' N$ to be $N$ if $M$ is an identity, and $M$ if $N$ is an identity, and the original $M\odot N$ otherwise. The first two cases agree when they overlap, and the result is isomorphic to the original $M\odot N$ by the original unitors, so you can transport the associators across those isomorphisms. (This works for bicategories too, and monoidal categories, etc.)

And, of course, by changing the morphisms you can replace the whole double category by a strict one.

Many thanks!

Is there any context where it would be useful to work with the weak definition, meaning a pseudo double category?

Mike Shulman (May 10 2025 at 22:40):

We often work with pseudo double categories, since many double categories that arise in practice are pseudo, such as the prototypical proarrow equipment Prof.

James Deikun (May 10 2025 at 22:44):

Strictification makes metatheory of a class of structures easier but it can make actual computations with particular structures harder.