10
$\begingroup$

The general adjoint functor theorem implies that a complete locally small category has a weak colimit of a diagram if and only if it has a colimit of this diagram. It seems that this is also true for finite colimits in locally cartesian closed categories. For example, if a locally cartesian closed category has a weakly initial object $W$, then we can define the initial object using the internal language: $$\sum_{x : W} \prod_{f : W \to W} f(x) = x.$$ The proof that this object is initial is similar to the proof of this fact for complete categories. Does this fact about locally cartesian closed categories appears in the literature?

The second question is whether this fact is true for $\infty$-categories. It is true for locally small complete $\infty$-categories as was shown in this paper (Proposition 2.3.2), but I think that it does not hold for locally cartesian closed $\infty$-categories. So, what is an example of a locally cartesian closed $\infty$-category with a weakly initial object, but without the initial one?

UPD: I proved that every weakly initial object in a locally cartesian closed $\infty$-category is initial in my answer, but there is still a more general question: does every locally cartesian closed $\infty$-category with weak finite colimits has finite colimits?

Improve this question
$\endgroup$
12
  • 2
    $\begingroup$ 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. $\endgroup$
    – Mike Shulman
    Commented May 3, 2018 at 16:24
  • 1
    $\begingroup$ @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. $\endgroup$
    – Valery Isaev
    Commented May 3, 2018 at 17:26
  • $\begingroup$ 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. $\endgroup$
    – Mike Shulman
    Commented May 3, 2018 at 21:51
  • $\begingroup$ 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. $\endgroup$
    – Valery Isaev
    Commented May 3, 2018 at 22:35
  • 1
    $\begingroup$ 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. $\endgroup$
    – Valery Isaev
    Commented May 4, 2018 at 10:30

1 Answer 1

Reset to default
1
$\begingroup$

This is a partial answer that summarizes the discussion in the comments.

It doesn't seem that this fact appears in the literature, but it easily follows from the general adjoint functor theorem for indexed categories applied to locally cartesian closed category with its canonical indexing over itself as Mike Shulman noted.

Now, let us discuss the $\infty$ case. First, let us note that it is not clear how complete indexed $\infty$-categories should be defined: as indexed $\infty$-categories with small products and finite limits or the ones with all small limits. It seems that the latter condition is stronger than the former in general. It is not clear if locally cartesian closed $\infty$-categories satisfy the latter condition, but it seems that they do satisfy the former. Anyway, can we prove the general adjoint functor theorem for indexed $\infty$-categories using either of the definitions of completeness? I don't know if the stronger condition can be used to prove it, but it seems that the weaker one alone is not enough. Nevertheless, I believe that it is enough if we assume additionally that the base $\infty$-category is idempotent complete. We cannot apply this fact to locally cartesian closed $\infty$-categories since they are not idempotent complete in general.

So, it seems that we cannot use the general adjoint functor theorem for indexed $\infty$-categories to prove this fact for locally cartesian closed $\infty$-categories. Nevertheless, we can prove directly that a weakly initial object in a locally cartesian closed $\infty$-category is initial. I will use the internal language (that is, HoTT with identity types, $\Sigma$-types, and extensional $\Pi$-types) to prove this. If $W$ is weakly initial, then it is a proposition (that is, a subterminal object). This follows from the fact that we have a map $W \to \mathrm{isProp}(W)$, where $\mathrm{isProp}(W) = \prod_{(x,y : W)} x = y$. This implies that every map $D \to W$ has a section, which implies that $W$ is initial. Indeed, if we consider $D = \sum_{(x : W)} f(x) = g(x)$, then a section of the obvious projection $D \to W$ proves that $f = g$. Note that this is a proof in the internal language, so this indeed proves that the space $\mathrm{Hom}(W,X)$ is contractible and not just that it is connected.

This answers the question in the original post, but I don't know if this argument can be applied to other weak finite colimits. The problem is that every weakly initial object is initial in a locally cartesian closed $\infty$-category, but this is not true for other weak colimits. I updated the post to include this more general question.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .