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: Arrow category as a ??? category

Jacques Carette (Apr 16 2021 at 21:51):

An arrow category "mixes" two things: objects and morphisms (as objects), and then again "mixes" morphisms and commutative squares (as morphisms). [This is easiest to see in the Setoid-enriched case, where there are 3 sizes involved, being pushed down to 2].

It seems to me that such a thing would prefer to live in 2 dimensions instead. It's not naturally a 2-category or a bicategory. Sure, we can have the objects and morphisms stay as is, but 2-morphisms want to be between things that mention only 2 objects, not 4. But maybe I'm not being creative enough? Let me try: to get $\mathsf{Arr}(C)$, take objects as pairs of objects of $C$, morphisms would be pairs of morphisms of $C$, and then 2-morphisms could again be a pair of morphisms $C$ that arrange into a commutative square. Does this work? The other direction of thinking is via double categories, but I can't work out the details.

My basic issue is that the Arrow Category is trying to squish too many things down to one level below where they really want to live (IMHO). But I'm having a hard time assembling things correctly.

This seems such an obvious thing to try, I'm surprised I have not been able to find such an alternate view. [This is part of me re-thinking all categorical constructions that seem to want to squish things down unnecessarily, and see instead where a roomier environment would be for them. Doing things in a theorem prover that forces you to pay very close attention to size issues pushes this kind of (re)thinking on me.]

John Baez (Apr 16 2021 at 22:04):

It sounds like you're wanting to think about the double category where the objects are objects of $C$, the horizontal and vertical arrows are arrows of $C$, and the squares (or 2-cells) are commuting squares in $C$.

Jacques Carette (Apr 16 2021 at 22:05):

I think so too, but when I try to work out the details, it doesn't quite work. So I was hoping that someone had already done it, and I could just read the right paper.

Nathanael Arkor (Apr 16 2021 at 22:55):

Is the double category of commutative squares the sort of structure you're thinking about? The objects are those of $\mathbf C$, with vertical and horizontal 1-cells the morphisms of $\mathbf C$, and 2-cells exhibiting commutative squares. See Example 3.8 in Fiore's Pseudo Algebras and Pseudo Double Categories, for instance.

John Baez (Apr 17 2021 at 02:07):

@Jacques Carette - Nathanael gave you a reference, but if you're stuck getting this to work I doubt that reference will help you much. But as the reference points out, this double category of commutative squares goes back to Ehresmann, the guy who invented double categories. So it's one of those things "everyone knows", and there are probably a bunch of references.

Ehresmann called it the "quintet construction". Why? Since he built such a double category from any 2-category, and then a 2-cell is a square that commutes up to a 2-morphism - so it consists of four morphisms and a 2-morphism.

In the special case where your 2-category is the discrete 2-category on a category (i.e., only having identity 2-morphisms) then the square must commute and we get what you're wanting.

Nathanael Arkor (Apr 17 2021 at 02:14):

(For some reason I entirely missed that you had also described this double category, John!)

John Baez (Apr 17 2021 at 04:12):

No problem. I usually reply to a comment and then read on and discover that other people already have....

Reid Barton (Apr 17 2021 at 16:53):

The arrow category is also just a special case of a functor category/category of diagrams, so maybe it would help to work at that level of generality.

Jacques Carette (Apr 17 2021 at 19:06):

The "problem" with a functor category is that it has the same issue as what got me here to begin with: squishing down big things into small spaces. I want a recipient that has as many size parameters as what I'm trying to fit. A "functor category" has 6 while a category has 3. Though it is true that for the Arrow category, 3 of the levels are 0. Nevertheless, it still takes things at two different levels (objects and arrows) to the same, thus the squishing.

I do realize this is somewhat quixotic. The reason I'm pulling on this thread is that it seems to really clarify size issues, and lets me be quite a bit more 'size polymorphic'. My instincts tell me this is a good thing.

Reid Barton (Apr 18 2021 at 15:03):

I guess most constructions in category theory "mix" the levels in a similar way. For example, an algebra for a monad consists of (1) an object $X$, (2) a map $\alpha : TX \to X$, (3) [such that] certain equations [hold].
Maybe the moral is that the levels are not that separate in the first place.

Reid Barton (Apr 18 2021 at 15:13):

Set theory seems to fit better here, since you don't have to have a universe in mind prior to introducing a set. You can ask after the fact whether set $X$ belongs to universe $\mathcal{U}$, and if it does that's great, and if not, just pick a bigger universe $\mathcal{V}$.

David Kern (Apr 18 2021 at 17:05):

This kind of mixing of levels has been given some attention by Crans in his study of the Gray tensor product, as laid out from the very end of page 13 (a.k.a. 2) and on, where he explains how he takes this dimension-raising idea (which he refers to as "topological" in contrast to the more "set-theoretical" lack of mixing seen in the cartesian product) as a central tenet for the construction of the tensor product of Gray-categories. It is also in this paper that he quantified this shift in categorical levels by coining the notion of $k$-transfor (for which see also this follow-up by the author and this generalisation to the $\infty$-categorical world), which sends an $n$-cell in a higher category to an $(n+k)$-cell.
In fact, in a functor (higher) category, the $0$-cells are $0$-transfors, the $1$-cells are $1$-transfors, and so on. Now I don't know whether this really helps things make more, or less, sense, but what it seems to suggest to me is that the current view of things is not too unreasonable.