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.
Nathaniel Virgo (Jul 08 2024 at 03:08):There are lots of ways to think about double categories, but for the purpose of this post I'm interested in viewing a (strict) double category as "a category with two types of morphism", where we think of a square as asserting that its frame commutes. ("Frame" means the four objects and four morphisms that define a square's type.)
As an example, imagine sets equipped with two different structures. Let horizontal morphisms preserve one structure and vertical morphisms preserve the other, and let squares assert that the underlying maps in commute.
To interpret a general double category in this sort of way, the double category should at least be "thin", meaning there is at most one square that fills each frame. But for it to really feel like the squares are "asserting equality", it feels like we need a bit more than that. For example, if we have squares
then it seems like we should be able to conclude that . The idea being that and can both be thought of as a kind of composite of and (despite their not being the same type), and so the two composites should be equal.
So I'm wondering if there's a structure like this that's been studied - a double category with additional axioms such that it makes sense to think of the squares as asserting that the frame commutes.
Matteo Capucci (he/him) (Jul 08 2024 at 06:45):I believe you can characterize the situation by asking the dbl category to be (a) fibrant (aka framed bicat aka proarrow equipment) (b) transpositive (ie it's a strict double category) and (c) for the transpose to be fibrant again
Matteo Capucci (he/him) (Jul 08 2024 at 06:46):Practically it means you have extensions and restrictions along both tight and loose maps. So in the example you make, h=g because they are both restrictions of F along (1_X,a)
Matteo Capucci (he/him) (Jul 08 2024 at 06:47):I wonder if one can prove that every 'transpositively fibrant' double category is equivalent to a double category of arrows
Nathaniel Virgo (Jul 08 2024 at 06:49):That makes a lot of sense, but I think it might be too strong, because if we change to some other morphism, we shouldn't be able to draw the same conclusion. At least, we can't draw that conclusion if we're looking at the double category of squares in some category.
Matteo Capucci (he/him) (Jul 08 2024 at 07:01):Uhm that's very true
Matteo Capucci (he/him) (Jul 08 2024 at 07:02):A category of squares though is transpositively fibrant :thinking: because it is fibrant & invariant under transposition! What am I missing?
Bryce Clarke (Jul 08 2024 at 07:03):As an example, imagine sets equipped with two different structures. Let horizontal morphisms preserve one structure and vertical morphisms preserve the other, and let squares assert that the underlying maps in Set commute.
It's worth warning that such double categories are typically ill-behaved. In the paper "Limits in double categories", Grandis and Paré describe a double category of topological groups in this way, but later note that isomorphisms in one direction do not transpose to isomorphisms in the other direction.
Matteo Capucci (he/him) (Jul 08 2024 at 07:04):Ah, no, it isn't fibrant unless the base category is finitely complete 🤦🏻♂️
Bryce Clarke (Jul 08 2024 at 07:04):Matteo Capucci (he/him) said:
A category of squares though is transpositively fibrant :thinking: because it is fibrant & invariant under transposition! What am I missing?
The double category of squares does not have conjoints.
Matteo Capucci (he/him) (Jul 08 2024 at 07:04):Indeed!
Matteo Capucci (he/him) (Jul 08 2024 at 07:05):Perhaps companions both ways are enough
Bryce Clarke (Jul 08 2024 at 07:08):@Nathaniel Virgo perhaps the notion you are looking for is [[right-connected double category]]. I have some talk slides on the notion here.