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.
    • CommentAuthorZhen Lin
    • CommentTimeAug 7th 2013

    Created modelizer. It’s not clear to me exactly what Grothendieck is taking as a property or as a structure in his definitions, but I tried to make a guess.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeAug 7th 2013

    Can you say anything about why this is considered an important enough concept to merit a neologism?

    • CommentRowNumber3.
    • CommentAuthorZhen Lin
    • CommentTimeAug 7th 2013

    The word is Grothendieck’s, not mine. (It’s older than I am!) I came across it in Pursuing Stacks and had always assumed that it was just his word for category with weak equivalences until I looked it up properly.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeAug 8th 2013

    I knew it was Grothendieck’s; I was just wondering whether you had any insight into his thoughts. (-:

    • CommentRowNumber5.
    • CommentAuthorTim_Porter
    • CommentTimeAug 8th 2013

    Certainly he thought it one of the most important aspects of PS as there was a whole section called ‘the Modelizer story’ if I remember rightly.

    • CommentRowNumber6.
    • CommentAuthorZhen Lin
    • CommentTimeAug 8th 2013

    I haven’t read enough of PS to say much about Grothendieck, but I can say that my own interest lies in the following questions:

    1. Why weak homotopy types, as opposed to strong homotopy types? I think this is especially mysterious from the point of view of derivators, because (at least on the face of it) derivators are an abstraction of what one might call the “local 2-category theory” of a complete and cocomplete 1-category.
    2. Put it another way, where does hypercompleteness come from? This surely has something to do with higher induction.
    3. Of the shapes for higher category theory, why simplices?
    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeAug 8th 2013

    I think weak homotopy types vs strong homotopy types is a red herring. “Weak homotopy types” are just an archaic name for \infty-groupoids, and those are obviously the important things. And if by “hypercompleteness” you mean the truth of Whitehead’s theorem, that’s a classicality axiom like LEM and AC.

    • CommentRowNumber8.
    • CommentAuthorZhen Lin
    • CommentTimeAug 8th 2013

    I can see that \infty-groupoids are important, but it’s not obvious to me why they should be more important than strong homotopy types. As for Whitehead’s principle – I think it’s much closer in spirit to well-pointedness (in ETCS) or extensionality (in ZFC) than to LEM or AC, because it’s telling us that a homotopy type is determined by its points, paths, etc. Then again, I don’t know anything about (,1)(\infty, 1)-toposes, so my understanding of hypercompleteness is probably too naïve.

    And there’s still the question of why \infty-groupoids show up in frameworks that don’t explicitly mention them, such as derivators or model categories. The more I think about the more confused I feel. Here is the story that I try to tell myself:

    It’s not surprising that the theory of \infty-groupoids is the free cocomplete homotopy theory on one object: after all, an \infty-groupoid is constructed by transfinite sequence of cell attachments.

    But I’m not completely convinced: just because a system is generated by some constructors doesn’t mean it is freely generated. On the other hand it is somewhat tautological that the free cocomplete category on one object is SetSet, the core observation being that there is always a canonical natural map

    lim c:Ccolim d:DHom(Xc,Yd)Hom(colim c:CXc,colim d:DYd)\operatorname{lim}_{c : C} \operatorname{colim}_{d : D} Hom(X c, Y d) \to Hom(\operatorname{colim}_{c : C} X c, \operatorname{colim}_{d : D} Y d)

    which happens to be a natural bijection when XX and YY are the constant diagrams with value 11 in SetSet. And then from here it’s perhaps unsurprising that the minimal basic localiser for CatCat is intimately connected to the free cocomplete derivator on one object. But that still doesn’t explain why that turns out to be -Grpd\infty\text{-Grpd}, or why that has the properties that it has!

    • CommentRowNumber9.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 9th 2013

    Mike was saying at CT2013 that if one takes HoTT as a model of weak \infty-groupoids, then there are no relations, merely free generators one dimension higher. I expect this point of view is largely model-independent.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeAug 9th 2013

    Homotopy type theory teaches us that \infty-groupoids are the inevitable result of studying the notion of sameness. So it shouldn’t be at all surprising that they are a fundamental part of mathematics.

    By contrast, the notion of strong homotopy type is tied to the notion of topological space, which, while certainly important, is nowhere near as fundamental, and admits of many modifications (sequential space, compactly generated space, pseudotopological space, convergence space, etc.) that would at least potentially change the resulting notion of strong homotopy type.

    Well-pointedness and extensionality are about internality versus externality. Internally, the logic of a topos is always well-pointed, where its objects are regarded as “sets” and determined by their points. Similarly, the internal logic of an (,1)(\infty,1)-topos is always well-pointed, where its objects are regarded as \infty-groupoids and also determined by their points. For instance, it’s true internally that if f,g:ABf,g:A\to B are two maps such that f(x)=g(x)f(x)=g(x) for all x:Ax:A, then f=gf=g; this is the principle of function extensionality. Whitehead’s principle is instead about whether an \infty-groupoid is determined by its truncations, which is a different thing than being determined by its points.

    I would say that \infty-groupoids are the free cocomplete homotopy theory because a “homotopy theory” is a category enriched over \infty-groupoids, just as Set is the free cocomplete 1-category because every 1-category is enriched over Set. (Why this also works with derivators is somewhat more mysterious, but I don’t think that issue has any bearing on your questions in #6.)

    • CommentRowNumber11.
    • CommentAuthorTim_Porter
    • CommentTimeAug 10th 2013

    As an unreformed (strong) shape theorist, the importance of strong homotopy type is that it is not the same a weak homotopy type. The interesting objects amongst the spaces include those where the simple idea of sameness of points, given by probing with arcs, fails to give enough information. Perhaps this relates to ’maps from models into’ and maps to some sort of ’comodels’ and ’maps out of’. I agree with Mike that this is not as foundational nor as basic as the weak homotopy type story.

    On another hand, I have wondered about its relationship to duality. The nice models of weak homotopy types are cofibrantly generated. Some of the models for pro-categories and thus for the other side of the coin, so to speak, are fibrantly generated. Does that suggest some large scale duality? There are quite recent papers (Barnea and Schlank) on variants of the cosmall ‘co-object’ argument… it is horribly tempting to write co-argument!!!!

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeAug 10th 2013

    By the way, the fact that the derivator of ∞-groupoids is the free left derivator on one object depends on the fact that every \infty-groupoid can be presented as the localization of some 1-category. This is an accident of classical mathematics, due to the axiom of choice and Whitehead’s principle. Hence it is unlikely to be true constructively that derivators characterize the theory of ∞-groupoids, and thus, one might argue, there is unlikely to be a good reason for it to be true. (-:

    • CommentRowNumber13.
    • CommentAuthorZhen Lin
    • CommentTimeAug 10th 2013

    Interesting! I suppose you are referring to Thomason’s proof that the Thomason model structure on CatCat is Quillen-equivalent to the standard model structure on sSetsSet. But if I understand correctly, Cisinski has proved a closely related general result:

    For any basic localiser 𝒲\mathcal{W}, there is a class of weak equivalences for sSetsSet such that the resulting left prederivator is equivalent to Cat[𝒲 1]Cat [\mathcal{W}^{-1}]; if 𝒲\mathcal{W} is accessible, then the weak equivalences come from a Cisinski model structure.

    (Put together Exemple 4.1.21, Proposition 4.2.7, and Corollaire 4.2.18 in Astérisque 308.) The level of generality suggests that the use of Whitehead’s principle in Thomason’s proof may be inessential. Perhaps it is only needed to show that the weak homotopy equivalences in CatCat are the weak equivalences of some model structure.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeAug 10th 2013

    Whitehead’s principle (along with a related classicality axiom that one might call the “set-presentation axiom”, that every type admits a surjection from a set, which follows from a sufficiently strong form of AC) is also necessary to show that simplicial sets present all \infty-groupoids. So moving from Cat to sSet changes nothing.

    • CommentRowNumber15.
    • CommentAuthorZhen Lin
    • CommentTimeAug 10th 2013

    Hmmm. What do you mean by \infty-groupoid? You must have a specific definition in mind in order to be able to say that simplicial sets don’t always present all of them!

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeAug 10th 2013

    In homotopy type theory, “\infty-groupoid” is an undefined term, like “set” in ZFC. (We usually pronounce it as “type”, though.)

    • CommentRowNumber17.
    • CommentAuthorZhen Lin
    • CommentTimeAug 11th 2013

    OK, but then I don’t understand what you mean by “show that simplicial sets present all ∞-groupoids”. Where is this comparison happening?

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeAug 11th 2013

    We have sets in homotopy type theory, so we can define simplicial sets therein.

    • CommentRowNumber19.
    • CommentAuthorZhen Lin
    • CommentTimeAug 11th 2013

    I see. I was under the impression that simplicial types were problematic to define.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeAug 11th 2013
    • (edited Aug 11th 2013)

    General simplicial types are problematic, because they correspond to genuinely homotopy coherent simplicial diagrams involving lots of coherence cells that are troublesome to axiomatize. But for simplicial sets = simplicial 0-truncated types this problem is alleviated.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeAug 11th 2013

    But even if it were still a problem to define simplicial sets in HoTT, we could still say confidently that if we could define them, then they wouldn’t model all types, since the problem of defining simplicial types is due to technical limitations of current type theory, while the failure to model all types is justified by higher topos models, which we understand.

    • CommentRowNumber22.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 12th 2013

    This has probably been discussed before in venues I haven’t been, but has anyone tried defining the category Δ\Delta by its universal property? This might not help with the problem of simplicial types in toto, but a partial solution?

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeAug 12th 2013

    Do you mean Δ +\Delta_+ as the free monoidal category on a monoid? That seems to reduce the problem to the no-easier one of defining coherent monoidal structures and monoids…

    • CommentRowNumber24.
    • CommentAuthorzskoda
    • CommentTimeAug 12th 2013

    David 22, if you mean the duality of Δ\Delta with the category of intervals people like Lawvere and Joyal like to put some other gadgets into the role of intervals, including internally in some topoi when it can be even more natural. I understood unfortunately just the surface of this discussion.

    • CommentRowNumber25.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 13th 2013

    Mike - hmm, ok. Zoran - I meant what Mike was talking about, but your suggestion raises different sorts of questions.