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.
Josselin Poiret (Jul 13 2023 at 12:57):I've been thinking a bit about straightening/unstraightening, and although I can't pretend I've read the proof for ∞,1-categories (I ought to at some point), am I right in my intuition that the complicated part of straightening/unstraightening isn't doing the Grothendieck construction part, but rather actually straightening the data of an ∞,2-functor into a bona-fide ∞-functor that ought to be equivalent with it?
If so, then am I right in expecting a 1-categorical analogue of straightening/unstraightening along the lines of: the 1-category of Grothendieck fibrations over up to equivalence is equivalent to the category of 1-functors
Joe Moeller (Jul 13 2023 at 15:21):The Grothendieck construction gives an equivalence between fibrations over and pseudofunctors .
Josselin Poiret (Jul 13 2023 at 15:58):Joe Moeller said:
The Grothendieck construction gives an equivalence between fibrations over and pseudofunctors .
yes, but that's not what I'm asking here, I'm asking for a strictification of this result, and first whether this strictification underlies the straightening/unstraightening for (∞,1)-categories
Kevin Arlin (Jul 13 2023 at 16:01):To get a split fibration (i.e. a strict functor into Cat) equivalent to an arbitrary Grothendieck fibration, I believe you generally have to change the base to an equivalent category.
Joe Moeller (Jul 13 2023 at 16:13):Sorry, I misunderstood the question. I see now why the question seemed odd to me.
Joe Moeller (Jul 13 2023 at 16:23):Kevin Arlin said:
To get a split fibration (i.e. a strict functor into Cat) equivalent to an arbitrary Grothendieck fibration, I believe you generally have to change the base to an equivalent category.
Could you explain how this would work with like short exact sequences of groups? Split sequences correspond to split fibrations. What can you change in a non-split sequence to get an equivalent split one?
Kevin Arlin (Jul 13 2023 at 16:27):I'll think about it more if I get a chance but in particular I'm pretty sure you won't end up with a functor into groups.
Mike Shulman (Jul 13 2023 at 16:27):No, you don't have to change the base. It's true in general that to replace a pseudofunctor between arbitrary 2-categories by a strict one, you have to change the domain. But in the special case when the codomain is , you don't.
Kevin Arlin (Jul 13 2023 at 16:28):Oh oops, thanks Mike.
Mike Shulman (Jul 13 2023 at 16:29):A highfalutin' way to explain it is that there's a 2-monad (and also a 2-comonad) whose strict (co)algebras are strict 2-functor and whose pseudoalgebras are pseudofunctors, and it satisfies the general strictification theorem, so any pseudoalgebra can be replaced by a strict one.
Mike Shulman (Jul 13 2023 at 16:33):There are also more explicit constructions. For instance, given a pseudofunctor , you can define an object of to be an object of together with isomorphic "choices" of its image under all maps (this is the comonad version). Or, you can define an object of to be a morphism together with an object of (this is the monad version). In both cases you define the morphisms to be induced from those of .
Kevin Arlin (Jul 13 2023 at 16:38):Is giving the explicit construction the usual way you'd suggest showing these co/monads satisfy strictification? I don't really know how to check in concrete cases in general using the condition that there's a splitting of the counit of the pseudomorphism classifier or whatever.
Josselin Poiret (Jul 13 2023 at 16:42):Right, but can you strictify the whole equivalence you get from the Grothendieck construction?
Mike Shulman (Jul 13 2023 at 16:55):There's a general theorem of Power ("A general coherence theorem"), generalized further by Lack ("Codescent objects and coherence"), which is usually my first resort when asking whether a 2-monad satisfies strictification. You observe that the base 2-category has a certain sort of factorization system and that the monad preserves the left class of it.
Mike Shulman (Jul 13 2023 at 16:59):Josselin Poiret said:
Right, but can you strictify the whole equivalence you get from the Grothendieck construction?
Oh argh, this is the thing I always get wrong. Let's see, I think the 1-category of fibrations and morphisms of fibrations is equivalent to the 1-category of pseudofunctors and pseudonatural transformations. But the 1-category of pseudofunctors is not equivalent to the 1-category of 2-functors, for two reasons: every pseudofunctor is equivalent to a 2-functor, but not isomorphic to it, and even between 2-functors not every pseudonatural transformation is isomorphic to a strict natural transformation.
Josselin Poiret (Jul 13 2023 at 17:28):What if you quotient by equivalences of fibrations on the left, and strictify to the 1-category of functors and pseudonatural transformations on the right side? I'm trying to mirror the straightening/unstraightening for ∞,1-categories
Kevin Arlin (Jul 13 2023 at 17:54):A theorem that seems to be in the direction you're looking for is on page 12-13 of Streicher's notes on fibered categories, and states that the forgetful functor from the 2-category of split fibrations and split cartesian functors to the 2-category of fibrations and cartesian functors is the 2-functor freely inverting the split cartesian functors which are equivalences on every fiber, but it's not an equivalence. So this says that if you quotient split fibrations by a weak notion of equivalence of fibration, one which isn't visible in the underlying 1-category, then the result is the same as the 2-category of fibrations.
The fact that this isn't an equivalence illustrates Mike's point that not every pseudonatural transformation comes from a 2-natural transformation.
Kevin Arlin (Jul 13 2023 at 17:55):This localizing forgetful functor also has both left and right adjoints, which may be relevant to the straightening and unstraightening argument you're trying to follow.
Mike Shulman (Jul 13 2023 at 18:40):Quotienting is very rarely what you want to do. Taking pseudonatural transformations between 1-functors (which accidentally form a 1-category) solves one problem but not the other.
Mike Shulman (Jul 13 2023 at 18:40):You also don't have an equivalence of 1-categories in the world, so I'm not sure what you're hoping to mirror.
Josselin Poiret (Jul 13 2023 at 18:48):Isn't there a Quillen equivalence between sSet-enriched presheaves and the slice category of simplical sets? But yeah I guess what you're alluding to is that while you can lower ∞,2 to ∞,1 you can't really get rid of all the 2-morphisms here.
Mike Shulman (Jul 13 2023 at 18:54):A Quillen equivalence is an -equivalence, which is much weaker than a 1-equivalence. There's nothing to be done in "lowering" an -equivalence to an -equivalence: since the is still the same, the former isn't any weaker than the latter, it just contains more data that you can easily forget.
Mike Shulman (Jul 13 2023 at 18:55):In other words: the weakness of the equivalence lies in the invertible morphisms, which are the same in the and the world. The analogue in lower dimensions would be a -equivalence, which is likewise easy to get from a 2-equivalence by forgetting the noninvertible 2-cells.
Josselin Poiret (Jul 13 2023 at 18:59):ah, yes, it's much clearer now, I don't know why I didn't think of that... thanks!
Notification Bot (Jul 13 2023 at 18:59):Josselin Poiret has marked this topic as resolved.
Josselin Poiret (Jul 13 2023 at 19:01):(FTR, I was looking for universe construction similar to eg. regular functions X → Sets, but for 1-categories, but I guess the picture is much more complicated since you can't just take functors B → Cat to faithfully represent all opfibrations over B)