Timeline for Weak colimits in locally cartesian closed categories
Current License: CC BY-SA 4.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 5, 2018 at 11:47 | history | edited | Valery Isaev | CC BY-SA 4.0 |
added 268 characters in body
|
| May 5, 2018 at 11:44 | answer | added | Valery Isaev | timeline score: 1 | |
| May 4, 2018 at 19:32 | comment | added | Mike Shulman | Hahaha, that's an awesome and hilarious proof. So it is actually easier to show that the weakly initial object is inital than to construct an (apparently different) initial object from it. Note that the second part of your argument can be rephrased as the standard proof that the typal $\eta$-rule for the empty type is provable from its induction principle; the first part is a clever trick to derive the induction principle from the recursion principle. | |
| May 4, 2018 at 10:30 | comment | added | Valery Isaev | I was trying to construct the initial object in an $\infty$-lccc using indexed $\infty$-categories, but it is easier to do this directly. First, note that we have a map $W \to \mathrm{isContr}(W)$. This implies that $W$ is a proposition. Now, if we have a pair of maps $f,g : W \to X$, then we have a map $r : W \to \Sigma_{x : W} f(x) = g(x)$. Since $W$ is a proposition, $\pi_1 \circ r = \mathrm{id}_W$. This implies that $f = g$. I need to think about the indexed case and then I'll write up this as an answer. | |
| May 4, 2018 at 8:29 | comment | added | Mike Shulman | I realized after writing it that it might not work either: adding extra data to $Z$ might let you show that $h$ is coherently idempotent "on the original data", but then you'd also have to show it's coherently idempotent on the new data, and that would probably require more data, ad infinitum. | |
| May 3, 2018 at 23:03 | comment | added | Valery Isaev | @MikeShulman I tried to add another level of coherence to $Z$, but this does not really work. It's too technical to try to explain the problem in the comment. And I need to think about your comment about completeness of an indexed $\infty$-category. Maybe you are right. | |
| May 3, 2018 at 22:54 | comment | added | Mike Shulman | A small diagram in an indexed $\infty$-category should be indexed by an internal $\infty$-category in the base. But the latter is externally infinitary (e.g. a complete Segal object), so I don't see any way to construct its limit from only fiberwise finite limits and indexed products; it seems we would need either fiberwise countable products or else some way of expressing an internal $\infty$-category in the base "finitarily". This is closely related to the "problem of infinite objects" in HoTT. | |
| May 3, 2018 at 22:51 | comment | added | Mike Shulman | Perhaps also worth noting that if an lccc has an initial object, then any weakly initial object is in fact itself initial, since initial objects in an lccc are strict. Not that this helps (at least, not in any obvious way) with constructing an initial object. | |
| May 3, 2018 at 22:51 | comment | added | Mike Shulman | Note that in order to make an idempotent fully coherent it suffices to have one extra coherence cell; the latter may not be itself fully coherent but it can always be nudged to become fully coherent. This is Lemma 7.3.5.14 of Higher Algebra, and the internal-logic version is in arxiv.org/abs/1507.03634. So maybe it would suffice to add one extra level of coherence to $Z$? | |
| May 3, 2018 at 22:39 | comment | added | Valery Isaev | If the $\infty$-lccc is idempotent complete, then I can almost construct the initial object. We have a map $r : W \to Z$, where $Z$ is the object from the post. We also have the obvious projection $e : Z \to W$. If $h = r \circ e$ is idempotent, then its splitting is initial. The problem is that we can show that $h \circ h$ is equivalent to $h$, but I cannot make this equivalence coherent. So, I cannot construct the initial object even with the assumption of idempotent completeness, but it seems that it might be possible. | |
| May 3, 2018 at 22:35 | comment | added | Valery Isaev | We should be able to define the notion of a small diagram in an indexed $\infty$-category. Then we can say that it is complete if every small diagram has a limit. I would hope that every indexed $\infty$-category with finite limits and product is complete in this sense. If this is true, then the problem is not that $\infty$-lccc is not complete as an indexed $\infty$-category. I would speculate that the problem is that we need to assume that the base $\infty$-category of an indexed $\infty$-category is idempotent complete to prove GAFT and this is not true for an arbitrary $\infty$-lccc. | |
| May 3, 2018 at 21:51 | comment | added | Mike Shulman | My explanation would be the related point that the internal-language expression $\sum_{x:W} \prod_{f:W\to W} f(x)=x$ is not a correct expression of the relevant $\infty$-limit, as it doesn't include any higher coherences. It's an interesting question what the correct definition of "complete indexed $\infty$-category" is and whether the self-indexing of an lccc one always is such; I would hope so since it is still true that an $\infty$-category is complete as soon as it has finite limits and arbitrary products, but maybe in the indexed case this would require an NNO in the base or something. | |
| May 3, 2018 at 17:26 | comment | added | Valery Isaev | @MikeShulman Yes, indeed! So, if I'm right and this is not true for $\infty$-lccc, then this means that GAFT does not hold in the context of indexed $\infty$-categories? Actually, I think that the problem might be that $\infty$-lccc are not necessarily idempotent complete. | |
| May 3, 2018 at 16:24 | comment | added | Mike Shulman | Nice observation! I think this should be essentially the GAFT applied in the world of indexed categories, using the fact that an lccc category is complete and locally small as indexed over itself? I don't think I've seen it in the literature though. | |
| May 3, 2018 at 16:23 | history | edited | Mike Shulman |
edited tags
|
|
| May 3, 2018 at 12:23 | history | asked | Valery Isaev | CC BY-SA 4.0 |