Timeline for Filtered 2-colimits commute with finite 2-limits
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 27, 2021 at 22:36 | comment | added | Tim Campion | @ZhenLin That seems valid. I think the simplest patch is to appeal to Prop 4.2.4.4 (which was used earlier in the proof in a similar way) to see that any functor of $\infty$-categories $\square \times A \to Spaces$ may be represented by a functor of 1-categories $\square \times A \to Kan$, where $\square = [1] \times [1]$ is the walking commutative square and $Kan$ is the category of Kan complexes (and $A$ is the directed poset as in the proof). | |
| Apr 27, 2021 at 16:27 | vote | accept | Mike Shulman | ||
| Apr 27, 2021 at 10:59 | history | became hot network question | |||
| Apr 27, 2021 at 10:52 | comment | added | Zhen Lin | The classical result is for strictly commutative diagrams, however, so somewhere one is using the fact that diagrams can be strictified… | |
| Apr 27, 2021 at 10:48 | answer | added | varkor | timeline score: 8 | |
| Apr 27, 2021 at 10:42 | comment | added | Tim Campion | It may not be a proof which is easily converted into a direct bicategorical proof, but I wouldn't call it "sketchy". | |
| Apr 27, 2021 at 10:41 | comment | added | Tim Campion | @MikeShulman Lurie reduces to the assertion that homotopy cartesian squares of Kan complexes are stable under colimits indexed by directed partially ordered sets, which he refers to as a "classical fact". It's true that such facts about simplicial homotopy theory are regularly used without citation in HTT, but I think they really are classical. For instance here, you just have to observe that since you've got all the maps you need, you can detect homotopy cartesianness by looking at homotopy groups, and that homotopy groups of Kan complexes commute with filtered colimits. | |
| Apr 27, 2021 at 2:05 | comment | added | Mike Shulman | @varkor Thanks, that's terrific! And the citation to Dupont's Interchange of filtered 2-colimits and finite 2-limits might be even better. I expect reflectivity isn't even needed if the filtered domains are 1-categories, since groupoids are closed in Cat under all limits and under colimits over 1-categories. If you post your comment as an answer I would probably accept it. | |
| Apr 27, 2021 at 1:59 | comment | added | Mike Shulman | @TimCampion Well, I'm looking at HTT 5.3.3.3, which spends quite a while carefully saying things about projective model structures, but then for the actual meat of the proof just says it "reduces to a classical assertion" without a citation. | |
| Apr 27, 2021 at 0:00 | comment | added | varkor | In case it's useful, Theorem 7.24 of Canevali's thesis 2-filtered bicolimits and finite weighted bilimits commute in Cat proves the result for categories rather than groupoids. Perhaps the reflectivity of Grpd in Cat is enough to transfer this to groupoids? | |
| Apr 26, 2021 at 23:40 | comment | added | Tim Campion | I agree there exist sketchy $\infty$-categorical proofs in the literature, but I can't think of anything I might try to deduce something like this from which I'd classify as "sketchy"... | |
| Apr 26, 2021 at 23:33 | history | asked | Mike Shulman | CC BY-SA 4.0 |