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.
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.
Can you say anything about why this is considered an important enough concept to merit a neologism?
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.
I knew it was Grothendieck’s; I was just wondering whether you had any insight into his thoughts. (-:
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.
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:
I think weak homotopy types vs strong homotopy types is a red herring. “Weak homotopy types” are just an archaic name for -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.
I can see that -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 -toposes, so my understanding of hypercompleteness is probably too naïve.
And there’s still the question of why -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 -groupoids is the free cocomplete homotopy theory on one object: after all, an -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 , the core observation being that there is always a canonical natural map
which happens to be a natural bijection when and are the constant diagrams with value in . And then from here it’s perhaps unsurprising that the minimal basic localiser for is intimately connected to the free cocomplete derivator on one object. But that still doesn’t explain why that turns out to be , or why that has the properties that it has!
Mike was saying at CT2013 that if one takes HoTT as a model of weak -groupoids, then there are no relations, merely free generators one dimension higher. I expect this point of view is largely model-independent.
Homotopy type theory teaches us that -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 -topos is always well-pointed, where its objects are regarded as -groupoids and also determined by their points. For instance, it’s true internally that if are two maps such that for all , then ; this is the principle of function extensionality. Whitehead’s principle is instead about whether an -groupoid is determined by its truncations, which is a different thing than being determined by its points.
I would say that -groupoids are the free cocomplete homotopy theory because a “homotopy theory” is a category enriched over -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.)
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!!!!
By the way, the fact that the derivator of ∞-groupoids is the free left derivator on one object depends on the fact that every -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. (-:
Interesting! I suppose you are referring to Thomason’s proof that the Thomason model structure on is Quillen-equivalent to the standard model structure on . But if I understand correctly, Cisinski has proved a closely related general result:
For any basic localiser , there is a class of weak equivalences for such that the resulting left prederivator is equivalent to ; if 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 are the weak equivalences of some model structure.
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 -groupoids. So moving from Cat to sSet changes nothing.
Hmmm. What do you mean by -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!
In homotopy type theory, “-groupoid” is an undefined term, like “set” in ZFC. (We usually pronounce it as “type”, though.)
OK, but then I don’t understand what you mean by “show that simplicial sets present all ∞-groupoids”. Where is this comparison happening?
We have sets in homotopy type theory, so we can define simplicial sets therein.
I see. I was under the impression that simplicial types were problematic to define.
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.
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.
This has probably been discussed before in venues I haven’t been, but has anyone tried defining the category by its universal property? This might not help with the problem of simplicial types in toto, but a partial solution?
Do you mean 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…
David 22, if you mean the duality of 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.
Mike - hmm, ok. Zoran - I meant what Mike was talking about, but your suggestion raises different sorts of questions.
1 to 25 of 25