Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014
    • (edited Nov 3rd 2014)

    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 Grpd\infty Grpd here.

    Namely the story at infinity-action is that given any type VV then the 1-image of its name in the universe is BAut(V)Type\mathbf{B}\mathbf{Aut}(V) \to Type. This we may think of as being a diagram of shape BAut(V)\mathbf{B}\mathbf{Aut}(V) internal in the \infty-topos. And then the statement is that the homotopy coinvariants of this Aut(V)\mathbf{Aut}(V)-action, hence the \infty-colimit of this internal diagram, is the pullback of the universal object bundle over the object classifier TypeType 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 Grpd\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?)

    • CommentRowNumber2.
    • CommentAuthorZhen Lin
    • CommentTimeNov 3rd 2014

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

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014
    • (edited Nov 3rd 2014)

    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 YDY \to D in the ambient \infty-topos H\mathbf{H}. Regard a map to the object classifier J:DTypeJ \colon D \to Type as a DD-shaped diagram internal to the \infty-topos. Consider the object J^H /D\hat J \in \mathbf{H}_{/D} classified by JJ.

    If H=Grpd\mathbf{H} = \infty Grpd then by HTT we have that

    limJDJ^ \underset{\longrightarrow}{\lim} J \simeq \underset{D}{\sum} \hat J limJDJ^. \underset{\longleftarrow}{\lim} J \simeq \underset{D}{\prod} \hat J \,.

    Here the right hand sides make sense in any H\mathbf{H}. And for general H\mathbf{H} I know that at least for DD of the form DBGD \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?

    • CommentRowNumber4.
    • CommentAuthorZhen Lin
    • CommentTimeNov 3rd 2014

    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.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014
    • (edited Nov 3rd 2014)

    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.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014
    • (edited Nov 3rd 2014)

    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?

    • CommentRowNumber7.
    • CommentAuthorZhen Lin
    • CommentTimeNov 3rd 2014

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

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeNov 3rd 2014

    I agree with Zhen, but there is definitely a dearth of people writing about things like indexed categories and internal limits in the (,1)(\infty,1)-case.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014

    Here is a reference:

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

    • CommentRowNumber10.
    • CommentAuthorZhen Lin
    • CommentTimeNov 3rd 2014

    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.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014
    • (edited Nov 3rd 2014)

    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 WW is just a type instead of an internal category, it would seem to be “pseudo” instead of lax.)

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2014
    • (edited Nov 3rd 2014)

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

    • CommentRowNumber13.
    • CommentAuthorZhen Lin
    • CommentTimeNov 4th 2014
    • (edited Nov 4th 2014)

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

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014

    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.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014
    • (edited Nov 4th 2014)

    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?

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeNov 4th 2014

    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.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014
    • (edited Nov 4th 2014)

    Okay, thanks.

    I suppose I know now what I wanted to know. I’ll go and define the internal lim(XFType)\underset{\longrightarrow}{\lim} (X \stackrel{F}{\longrightarrow} Type) of an internal \infty-groupoidal diagram as dependent sum of F^\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 XBGX \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 XBGX \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 XX 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.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeNov 4th 2014

    made a brief note at internal (co-)limit