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.
Asad Saeeduddin (Feb 24 2022 at 22:37):Given a category C with all finite products, is there a "dependent pair" category whose objects are dependent pairs of objects (o : C, f : C/o), (o' : C, f' : C/o') (where C/o is the slice category induced by o) and whose morphisms are dependent pairs (m : C(o, o'), m' : C/o'(m* f, f')) (where m* : C/o -> C/o' is the base change functor induced by m)?
Reid Barton (Feb 24 2022 at 22:39):Yes, but it's just called the arrow category of C.
Reid Barton (Feb 24 2022 at 22:39):Unless I overlooked some subtlety in your definition.
Asad Saeeduddin (Feb 24 2022 at 22:41):oh, interesting. i'll have to chew on that for a bit, thanks!
Asad Saeeduddin (Feb 24 2022 at 22:48):@Reid Barton is there an equally easy name for the category given by taking the _opposites_ of the slice categories?
Asad Saeeduddin (Feb 24 2022 at 22:48):I'm still trying to work through the correspondence between what I described and the arrow category btw, if you know of some resources I could consult that would be much appreciated
Mike Shulman (Feb 24 2022 at 22:51): Asad Saeeduddin (Feb 24 2022 at 23:26):Ok, someone linked me to this, which clarifies a bunch of this: https://arxiv.org/pdf/1908.02202.pdf
Asad Saeeduddin (Feb 25 2022 at 00:41):Ok, so one mistake I was making in the original question is that I was applying the change of base functor on the wrong side: f : X -> Y induces f* : C/Y -> C/X, and not the other way around. I can see now (from the linked paper) how the twisted arrow category can arise from a correction of this process. Is there some variation that also gives rise to the (non-twisted) arrow category?
Bruno Gavranović (Feb 25 2022 at 01:03):I believe this is the codomain fibration which you get with a covariant functor, and a different variant of the Grothendieck construction than the one Spivak uses in that paper (not pointwise opposite)
Spencer Breiner (Feb 25 2022 at 13:35):In the bidirectional case there are two different versions.
The twisted arrow category makes sense for any underlying category, and has arrows like this:
The dependent lens category requires pullbacks, and has arrows like this:
You can play the same game in the forward direction, but these are equivalent via the universal property of the pullback:
This last one is a presheaf category, so it is well-understood by general methods.
Reid Barton (Feb 25 2022 at 14:05):(It's a presheaf category if C is Set or more generally a presheaf category, and it's always a category of diagrams valued in C.)
Spencer Breiner (Feb 25 2022 at 15:28):Whoops! Good point