Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeNov 3rd 2014
   • (edited Nov 3rd 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexA 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](http://ncatlab.org/nlab/show/limit+in+a+quasi-category#WithValInooGrpd). 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](http://ncatlab.org/nlab/show/limit+in+a+quasi-category#WithValInooGrpd). 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](http://ncatlab.org/nlab/show/limit+in+a+quasi-category#ColimitsInInfinityCat). 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?)

   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?)

2. • CommentRowNumber2.
   • CommentAuthorZhen Lin
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexIt's not so obvious to me how to invert morphisms in an internal category, which is an important step in constructing homotopy colimits.

   It’s not so obvious to me how to invert morphisms in an internal category, which is an important step in constructing homotopy colimits.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeNov 3rd 2014
   • (edited Nov 3rd 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexLet'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](http://ncatlab.org/nlab/show/limit+in+a+quasi-category#WithValInooGrpd) 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?

   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?

4. • CommentRowNumber4.
   • CommentAuthorZhen Lin
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexI 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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeNov 3rd 2014
   • (edited Nov 3rd 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexWhat'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](http://ncatlab.org/nlab/show/limit+in+a+quasi-category#ColimitsInInfinityCat).

   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.

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeNov 3rd 2014
   • (edited Nov 3rd 2014)
   • PermaLink
   Author: Urs
   Format: MarkdownItexActually, given the relation of the categorical version of the [external statement](http://ncatlab.org/nlab/show/limit+in+a+quasi-category#ColimitsInInfinityCat) 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?

   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?

7. • CommentRowNumber7.
   • CommentAuthorZhen Lin
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexThe yoga of internal limits and colimits for is well established for ordinary indexed categories. This is the evident $(\infty, 1)$-categorical analogue.

   The yoga of internal limits and colimits for is well established for ordinary indexed categories. This is the evident $(\infty, 1)$-categorical analogue.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexHere is a reference: * Claudio Pisani, _Balanced Category Theory II_ ([arXiv:0904.1790](http://arxiv.org/abs/0904.1790)) Colimits via dependent sum is on p. 18, limits via dependent product is on p. 23.

   Here is a reference:

   • Claudio Pisani, Balanced Category Theory II (arXiv:0904.1790)

   Colimits via dependent sum is on p. 18, limits via dependent product is on p. 23.

10. • CommentRowNumber10.
    • CommentAuthorZhen Lin
    • CommentTimeNov 3rd 2014
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexIf 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](http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/FibLec.pdf).

    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.

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014
    • (edited Nov 3rd 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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.)

    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.)

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014
    • (edited Nov 3rd 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItex@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.

    @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.

13. • CommentRowNumber13.
    • CommentAuthorZhen Lin
    • CommentTimeNov 4th 2014
    • (edited Nov 4th 2014)
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexOops, 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.)

    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.)

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, 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.

    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.

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014
    • (edited Nov 4th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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?

    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?

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexGood 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.

    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.

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014
    • (edited Nov 4th 2014)
    • PermaLink
    Author: Urs
    Format: MarkdownItexOkay, 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.

    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.

18. • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014
    • PermaLink
    Author: Urs
    Format: MarkdownItexmade a brief note at _[[internal (co-)limit]]_

    made a brief note at internal (co-)limit