Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 18 of 18
A thought: the way that homotopy invariants and coinvariants are built abstracly as described at infinity-action is just the internal version of the construction of $\infty$-colimits and $\infty$-limits in terms of the object classifier of $\infty Grpd$ here.
Namely the story at infinity-action is that given any type $V$ then the 1-image of its name in the universe is $\mathbf{B}\mathbf{Aut}(V) \to Type$. This we may think of as being a diagram of shape $\mathbf{B}\mathbf{Aut}(V)$ internal in the $\infty$-topos. And then the statement is that the homotopy coinvariants of this $\mathbf{Aut}(V)$-action, hence the $\infty$-colimit of this internal diagram, is the pullback of the universal object bundle over the object classifier $Type$ along this map, and the homotopy invariants, hence the $\infty$-limit of the internal diagram, is the sections (i.e. dependent product) of the resulting colimit.
Done in $\infty Grpd$ this is just a special case of the discussion here.
So I am wondering: the above has an evident generalization to a construction that seems to give internal $\infty$-(co-)limits over any internal $\infty$-groupoidal diagram. And then boosting the type universe to its canonical Rezk-complete category object, one may easily mimic internally also what is done for $\infty$-category-indexed (co-)limits here.
Has this way of approaching internal $\infty$-(co-)limits already been considered anywhere?
(Sorry, this is sort of obvious, now that I think about it. Probably it’s an old hat. What’s a reference?)
It’s not so obvious to me how to invert morphisms in an internal category, which is an important step in constructing homotopy colimits.
Let’s first look at the case of groupoidal diagrams. What is known?
So given an “internal $\infty$-groupoid”, hence equivalently just a 1-epi $Y \to D$ in the ambient $\infty$-topos $\mathbf{H}$. Regard a map to the object classifier $J \colon D \to Type$ as a $D$-shaped diagram internal to the $\infty$-topos. Consider the object $\hat J \in \mathbf{H}_{/D}$ classified by $J$.
If $\mathbf{H} = \infty Grpd$ then by HTT we have that
$\underset{\longrightarrow}{\lim} J \simeq \underset{D}{\sum} \hat J$ $\underset{\longleftarrow}{\lim} J \simeq \underset{D}{\prod} \hat J \,.$Here the right hand sides make sense in any $\mathbf{H}$. And for general $\mathbf{H}$ I know that at least for $D$ of the form $D \simeq \mathbf{B}G$ they do give the correct limts and colimits as on the left.
Is this true more generally? Is this in general a sensible concept of internal $\infty$-(co-)limits over groupoidal diagrams?
I agree that colimits and limits of diagrams indexed over internal groupoids are just $\Sigma$ and $\Pi$. But I think diagrams indexed over internal categories are more complicated.
What’s your agreement based on?
For internal categorical diagrams of internal categories one will need the analog of inverting cartesian morphisms as in the external statement.
Actually, given the relation of the categorical version of the external statement to the Grothendieck construction, it ought to be true that not inverting anything gives internal (co-)limits that are “lax” or “comma” or whatever it’s to be called.
So we could make that a defininition of suitable internal $\infty$-(co-)limits. What I am trying to ask is: has anyone thought and maybe written about that definition and its relation to other possible definitions? Has this been considered? What’s a source?
The yoga of internal limits and colimits for is well established for ordinary indexed categories. This is the evident $(\infty, 1)$-categorical analogue.
I agree with Zhen, but there is definitely a dearth of people writing about things like indexed categories and internal limits in the $(\infty,1)$-case.
Here is a reference:
Colimits via dependent sum is on p. 18, limits via dependent product is on p. 23.
If you’re looking for a textbook reference for the ordinary version, see §B1.4 in [Sketches of an elephant]. See also §§6–8 Streicher’s notes.
I see that section 6.12 in the HoTT book sort of makes the statement regarding dependent sum and colimit. (However, why does it say “lax colimit” there? As long as the base $W$ is just a type instead of an internal category, it would seem to be “pseudo” instead of lax.)
@Zhen Lin, re #10, Johnstone and Streicher introduce and/or motivate the terminology “dependent product” or “indexed product”.
I am looking for places that develop a theory of internal (co-)limits over diagrams, hence over diagrams with some edges in there. Some actual discussion justifying terminology etc.
I don’t doubt that what I said in #3 is plausible, by analogy. That’s why I am suggesting it. But I am wondering if anyone has discussed this with a bit of more theory than saying “it’s plausible by analogy”.
Pisani comes closer, in that he shows how ordinary limits and colimits in $Set$ are given by suitable dependent sum and dependent product.
The HoTT book in section 6.12 at least sort of considers groupoidal diagrams (without really saying so) and at least sort of makes the statement about colimits over them being given by dependent sum.
Oops, I forgot to mention Proposition B2.3.20. (Of course, this result couldn’t have appeared earlier in the book because internal diagrams had not been defined yet.)
Yes, B2.3 is what you want for the 1-categorical case.
@Urs #11, I think the book says “lax colimit” because a Grothendieck construction is, in general, a lax colimit. It so happens that when the diagram shape is a groupoid, lax colimits are the same as pseudo ones. (Although perhaps it would be helpful to remark on this.) Some more general kinds of colimits are discussed in exercises 7.2 and 7.16.
I have checked out prop. B2.3.20 now. Thanks!! Yes, that’s better.
I am still thinking that for the self-indexing of a topos there should be a way to see internally that this construction “looks right” from the inside. From the inside one should consider an internal diagram and find that its (co-)limit (defined via dependent sum/product as we are discussing) is its object of internal (co-)cones.
I sort of see how to do this. Does Johnston also discuss this anywhere?
Good question; I don’t think he does. That’s the sort of thing that’s “obvious” to the people to whom it is obvious, but I’m not sure right now of a place where it’s written out.
Okay, thanks.
I suppose I know now what I wanted to know. I’ll go and define the internal $\underset{\longrightarrow}{\lim} (X \stackrel{F}{\longrightarrow} Type)$ of an internal $\infty$-groupoidal diagram as dependent sum of $\hat F$ and will say something like: “In traditional topos theory this is either known or widely agreed to be the correct internal formulation of colimits, and so here we take it as our definition of internal groupoid-shaped $\infty$-colimits”.
It just seems an important fact to highlight. We should not fall into the trap of being arrogant towards simplicity of concepts in higher topos theory. On the contrary, that’s the whole point: what internally in the $\infty$-topos looks like kindergarten, externally is going to be sophisticated.
We see this here: internal $\infty$-(co-)limits of the above form already for the special case that $X \simeq \mathbf{B}G$ are highly interesting externally. They are the $\infty$-topos generalization of the Borel construction. They are externally given by simplicial-shaped homotopy colimits, hence by non-finite colimits. They encode the entire derived representation theory etc. pp.
I have proven these things for the case $X \simeq \mathbf{B}G$. The external version of even just this special case of the internal simplistic concept subsumes a long series of work by many people. The case of general $X$ will be analogous, but may require a tad of thinking. Or of being more awake. In any case, it will be still a bit richer.
So it might be good to highlight the internal concept more.
made a brief note at internal (co-)limit
1 to 18 of 18