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.
I created n-connected map. If anybody knows sources for Propositions 2 and 4 which actually prove them it would be nice to add them.
Thanks!
When you have a minute, could you maybe cross-link that with the discussion of -connected morphisms more generally in n-connected morphism ?
(Your entry should say “see also n-connected morphism for the general case” and that entry should say “see also n-connected map for a special case”. Or something like that.)
Thanks! But I object to taking over the word “map” to mean “morphism in Top”. Can’t we call this page something like “n-connected map of spaces” or “n-connected continuous map” or “n-connected functor of infinity-groupoids”?
I also corrected the first sentence: Top is not itself an -topos, it only presents one.
I agree with all your remarks, but apparently I shouldn’t change page titles because of some cache bug. I’ve taken the phrase “(∞,1)-topos Top” from n-connected space without thinking too much about its correctness. I’ve edited this entry accordingly.
We might think about whether it’s a good idea, but currently the page Top says that “Top” can stand for lots of different things, including the 1-category and the -topos.
I think if it is clear from the context there is no harm. We won’t get Lab-global conventions anyway.
I think there is harm in saying “the -topos ”. Not for those of us who know what is meant, but for the newcomer still trying to wrap their head around all these ideas.
Yeah, we should really have more discussion at Top .
That might help, but I still think it would be better to avoid saying “the (∞,1)-topos Top” entirely.
I’ve seen Urs write that long enough that I’m quite familiar with it, but maybe it’s not the best. But then what should we call that -topos? OK, sure, we could call it , but calling it specifies a way of looking at it, and indeed a way that may well be most familiar to most mathematicians.
Well, I guess I see how you wrote it, Mike.
I shouldn’t change page titles because of some cache bug
Yes, you can! The cache bug clears itself eventually; don’t let it stop you.
what should we call that (∞,1)-topos?
Well, of course.
I’ve seen Urs write that long enough
Hm? You mean you saw me point out the subtlety often enough? The only time that I use to denote the -topos is when I amplify that the cohesive is geometric realization of -stacks under the “homotopy hypothesis”-equivalence .
Well, I’ve seen somebody write that, I’m sure. I thought that it was you.
I am confused by this discussion. When exactly are we allowed to say “ is an (∞,1)-category”? From the (∞,1)-category page I conclude that this is OK whenever is a quasi-category, complete Segal space or simplicially enriched category. I don’t see why any of these notions deserves the privilege of “being (∞,1)-category” (as opposed to “presenting one”) any more than a model category does. After all we don’t have one preferred, canonical definition of (∞,1)-categories, so it could be argued that any particular definition merely defines “presentations of (∞,1)-categories” not (∞,1)-categories themselves.
I like to think of “presenting an -category” really in the technical sense of: exhibiting it as the free hocolim completion of a small set of generating objects followed by quotienting out relations.
Then a combinatorial model category in the form of a category of -valued presheaves is such a presentation.
I then probably tend not to care about making explicit and so then also speak of model structures of -valued presheaves as presentations. For a single generating object that’s itself, and so it “presents” .
I agree that this last way of speaking may be objectionable as a technical statement. But then, in casual discussion we need to be able to speak without falling over own feet each time.
The worry with just saying “” that people are expressing here is that more often than not one sees people new to this topic get confused over the distinction between topology and homotopy theory presented by topology, hence between the plain 1-category (no model structure) and various other things that this 1-category “presents”, which have really nothing at all to do with topology. In other words, it’s the the misappreciation of how much rearranging actually happens when one passes along that tends to fool beginners. I could point to places where this is happening just recently here and on other forum, but maybe that won’t be helpful.
A good example of this, which I guess Mike has in mind, are various discussions one could see between type theorists who now are learning about homotopy theory for the first time, and are trying to understand what it really means that their “types” are homotopy types. Often one could see them speak and think as “We have learned that types in intensional type theory are topological spaces.” and put this way it is an awefully misleading and often also misled statement.
(A discussion of this sort on the HoTT forum once was what made me create this entry with the discussion it has about the difference between the geometric interval / circle and the homotopy-theoretic interval/circle. Because not making that distinction had led to some confusion on a type theory discussion forum.)
Coming back to the original issue: one quick way to make sure that everybody thinks of the right -category when seeing the symbols “” is to decorate them appropriately as or maybe or the like.
Just thought of what might be a good analogy:
also (category of posets) gives a “presentation” of . In terms of this the worry expressed here is that people may misunderstand what it means to say “the -category “and will start saying things like “A homotopy type is a poset” or similar. Which is all correct if one knows how to read it, but which is all too easily instead read in a wrong way if not accompanied by more detailed technical qualification.
I would say that I understand all those things (unless there is some subtlety that eludes me here). My question was more about the use of language than about mathematics. Let me try to rephrase by asking whether you agree with the following.
There are Quillen equivalences between various model categories (in fact Dwyer-Kan equivalences between relative categories suffice) whose objects are topological spaces, simplicial sets, posets etc. Therefore it is OK to adopt a convention of saying that “a topological space is a homotopy type”, “a simplicial set is a homotopy type” or “a poset is a homotopy type” because those Quillen equivalences tell us how to understand objects of those various types as objects of the same (classical) homotopy theory.
Similarly, there is a Quillen equivalence between the category of simplicial sets with the Joyal model structure and the category of relative categories with the Barwick–Kan model structure. Therefore if it is OK to say that “a quasi-category is an (∞,1)-category” then it should be OK to say “a relative category is an (∞,1)-category”. In particular since model categories are relative categories with some extra structure it should be OK to say “a model category is an (∞,1)-category”.
All that was remarked here is that while all this is indeed OK, it can be misleading to readers. I guess there is nothing we disagre about, technically. The only thing that was remarked was that in a wiki entry where the context is less fixed than in a single textbook volume, say, one should be careful to use notation such as to make clear what is really meant.
But I guess we’ll easily agree on that, too! :-)
Therefore it is OK to adopt a convention of saying that “a topological space is a homotopy type”, “a simplicial set is a homotopy type” or “a poset is a homotopy type”
I’m not sure I agree with that. I would say that all of those things (can) present homotopy types rather than being homotopy types. There are other model structures on Top, sSet, and Pos, for instance, which are not Quillen equivalent to all of these (notably the trivial model structures, but also the Hurewicz model structure, the Joyal model structure, etc.). So there is nothing intrinsic to the notion of “topological space” which forces us to regard it as living in the Quillen model structure, which is what “a topological space is a homotopy type” implies to me.
Perhaps part of the difference is between local conventions and global ones. Certainly, in the context of a particular paper, it is okay to talk about topological spaces as “being” homotopy types, when you have established at the beginning that the model structure you care about is the Quillen one. What I’m objecting to is as a global convention for mathematics. And I think that on an nLab page, we should avoid local conventions, because we know nothing about the background of someone coming to an nLab page from outside.
I would say that all of those things (can) present homotopy types rather than being homotopy types. There are other model structures on Top, sSet, and Pos, for instance, which are not Quillen equivalent to all of these (notably the trivial model structures, but also the Hurewicz model structure, the Joyal model structure, etc.). So there is nothing intrinsic to the notion of “topological space” which forces us to regard it as living in the Quillen model structure, which is what “a topological space is a homotopy type” implies to me.
I definitely agree. What I meant by “convention” is that we fix those specific model categories (and Quillen equivalences between them). So it shouldn’t apply for example if we talk about simplicial sets in the context of the Joyal model structure. I guess this is what you call a local convention.
Just let me clear one thing. If we don’t fix any such convention, then no specific object can “be a homotopy type” or “be an (∞,1)-category”, it can only present one, right?
That’s an interesting question. I think I can imagine some structure for which the homotopy-type-ness is so obvious and fundamental to its being that I wouldn’t mind saying that it ’is’ a homotopy type. Something like a Batanin/Grothendieck infinity-groupoid, perhaps. But I haven’t thought about that a lot, so I might have to retract it after further consideration.
Or a type in homotopy type theory?
(And why does my web browser’s default spell-check dictionary recognise ‘homotopic’ but not ‘homotopy’?)
Yes, certainly! But I think that’s a bit of a different sort of ’is’ – a type in hott ’is’ a homotopy type in the same sense that a set in ZFC ’is’ a set, namely by definition (plus axioms or rules that make that definition reasonable). In particular, we couldn’t say that types in hott form a model category that’s Quillen equivalent to the other ones Karol mentioned.
Something like a Batanin/Grothendieck infinity-groupoid, perhaps.
I don’t know anything about them, but from the Morphisms section of Batanin omega-category I gather that some extra information is required to explain exactly how Batanin ∞-categories “are” ∞-categories. This extra information seems to be not unlike a model structure. My question was perhaps too broad in asking about all potential definitions, but maybe we can agree that all presently established definitions of (∞,1)-categories only define presentations.
This raises a question: does the bare phrase “(∞,1)-topos ∞Grpd” have any meaning? I can see two ways of giving it a meaning.
I’m asking this because phrases like this show up all over the nLab (especially in articles which are supposed to be independent of particular models) often without any further specifications, which makes me think that some convention of reading them is in place, but I don’t really know what this convention is.
Or a type in homotopy type theory?
That’s a nice thought, but as Mike remarked it’s not really what I had in mind. On the other hand maybe homotopy type theory could offer a language to express the universal property of ∞Grpd which could then be interpreted in whatever model we like. However, as far as I understand homotopy type theory can presently handle (∞,k)-categories only for , is that right?
I gather that some extra information is required to explain exactly how Batanin ∞-categories “are” ∞-categories. This extra information seems to be not unlike a model structure.
I agree. However, I would argue that in contrast to topological spaces, simplicial sets, or posets, there is no other competing potential way of thinking about Batanin ∞-categories. There is clearly only one interesting model structure (or model-structure-like-thing) on them.
Obviously, this is a statement more about the current mental state of the society of mathematicians than about mathematics, but I don’t think that makes it invalid, since what we are talking about is just conventions of language.
some convention of reading them is in place
I think the convention is “pick your favorite model; then whatever I just said will be true about that model”. “Picking a model” might entail picking a model category that presents , or it might entail picking a model category that presents and inside which has a known characterization.
It’s really not conceptually dissimilar to the phrase “the real numbers”, which can be constructed using Cauchy sequences, Dedekind cuts, or any number of other ways, or characterized universally as a terminal coalgebra or a complete ordered field, all producing isomorphic results. When I say something about “the real numbers”, it’s understood that you can use any definition of them that you wish, and what I said will still be true. (This is an aspect of the principle of equivalence, of course.)
So we also object to saying ‘a Dedekind cut of rational numbers is a real number’ or ‘a Cauchy sequence of rational numbers is a real number’? They’re just presentations, not the thing itself?
I would probably object if I heard someone say ’the complete ordered field of Cauchy sequences of rational numbers’. For one thing, you have to impose an equivalence relation on Cauchy sequences of rationals to make them present the reals, which is the same sort of thing as homotopically inverting weak homotopy equivalences in Top. Dedekind cuts are a bit more like Batanin omega-groupoids, but one could argue that there’s still a nonvacuous step of choosing to regard a Dedekind cut of rationals as a real number. I guess you could theoretically regard it as something else, like a surreal number, although since the reals embed in the surreals that’s not so different. Maybe the deeper point is that if someone thinks that real numbers are Cauchy sequences, or Dedekind cuts, or something else specific, then that person hasn’t really understood the concept of ’real number’ yet.
All that is fine with me, but the situation with (∞,1)-categories is significantly more delicate than with real numbers, isn’t it?
Various ways of constructing real numbers all yield a structure of a specific type. We have specific second-order axioms that they all satisfy and (we can prove in some ambient set theory that) those axioms have essentially unique model. That’s a very satisfactory state of affairs and in my mind it removes all possible ambiguities we could run into when talking about real numbers.
On the other hand has many presentations by structures of various kinds so we have to put some serious effort into explaining how they are canonically equivalent. We know that satisfies a universal property, but this property is itself expressed in (∞,1)-categorical language. So we would have to fix some particular presentation of the ambient (sufficiently large) (∞,1)-category of (∞,1)-categories and then explain how each of our original presentations is (or presents) an object of this ambient (∞,1)-category. Mathematically this is good enough for me, but I would like to have something more conceptual which would avoid the arbitrary choice of the presentation of ambient (∞,1)-category. Perhaps there is some homotopy type theoretic way of doing this.
If you adopt homotopy type theory as foundations (of course you might argue that this, too, is a choice), then the ambient -categorical context that you mention above is given.
I think that’s clearly where things are headed…
Are you saying that we already know how to do it or that we hope that it can be done? I asked above “However, as far as I understand homotopy type theory can presently handle (∞,k)-categories only for k=0, is that right?”
More delicate technically, perhaps, but I would argue not conceptually different. E.g. with real numbers you have to choose an ambient set theory in which to work. At some ’outer’ level you always have to make a choice of something concrete.
That’s true, but my thinking was that there is a conceptual difference here. Namely, in the first case we can use set theory as an ambient theory which is independent of the theory of real numbers. In the second case the ambient theory is the theory of (∞,1)-categories which is the same (up to universe shift) theory as the one we are trying to characterize by a universal property.
Maybe the difference is only psychological and not really conceptual. I guess what’s bugging me is that when we make the choice of the presentation of the ambient (∞,1)-category we don’t know yet that our result is going to be independent of this choice. We know this only after proving the result itself (and provided that we do it in a universe independent manner). As I said, mathematically this is a right thing, it just seems somewhat inelegant.
Namely, in the first case we can use set theory as an ambient theory which is independent of the theory of real numbers. In the second case the ambient theory is the theory of (∞,1)-categories which is the same (up to universe shift) theory as the one we are trying to characterize by a universal property.
I’d think this becomes a very useful analogy as follows:
in analogous to
And it’s being done: maybe the most wide-spread approach is via Bishop sets (or “setoids”). I have just collected some relevant pointers there.
So in this context one takes type theory as the ambient context and then tries to formalize the notion of set in there. Interestingly, the definition of Bishop set in type theory is in the same spirit as the definition of internal (infinity,1)-category in homotopy type theory: where the latter is a
a homotopy type “of objects”
a homotopy type “of morphisms”
etc.
such that there is a coherent compositon operation, a Bishop set is
a type “of elements”
a type “of equalities”
such that this becomes an equivalence relation. So a Bishop set is something like a “complete Segal 0-groupoid” (in the sense of “complete Segal space” – which is a really bad term that should better read “-category internal to an -topos”).
So I think this analogy is great: doing -category theory in homotopy type theory is analogous to doing constructive set theory internal to type theory.
@Karol, I think I basically agree with you that the situation is inelegant. But I’ve been doing my best to get used to the situation, since I don’t really see much prospect of improving it in the near future. I think we’ve had some discussions about related things in the past, e.g. this comes to mind.
I had completely forgotten about the above discussion from over three years back. Only by chance did I run into the entry “n-connected map” again, while trying to record the traditional concept of “n-equivalence” in algebraic topology somewhere on the Lab.
I have now:
edited the Idea-section a little for better consumption
renamed the entry to “n-connected continuous function” (but left the old name in place as redirect for the moment)
made also “n-equivalence” etc. a redirect;
pointed to this entry from the Examples-section (here) at n-connected objct of an (infinity,1)-topos
1 to 36 of 36