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 have begun the page homotopy hypothesis for 1-types with a view to giving a proof. It will take some time before it is complete, I will be building it up gradually.
I also added a link pointing to this new page from homotopy hypothesis.
The proof that I will give has some novel aspects, such as using cubical sets, and is I guess slightly original, though it is only really a variation on the usual arguments. It has been known to me for many years.
Notation 3 seems to duplicate Notation 2.
Thanks! I am working offline and then copying in, and sometimes also cutting and pasting things within the edit box too, so this may turn out not to be the only case of this. Do let me know if you find any more.
After originally writing some more abstract material which can be found in the revision history, I have removed this and gone with a completely explicit construction of the fundamental groupoid/nerve adjunction. For the proof that I am giving, one needs an explicit characterisation in the end anyway, so one might as well just define it explicitly in the first place.
I have also explained one direction of the ’equivalence’ part of the Quillen equivalence (although I have not discussed model structures yet). The other direction is the most interesting one, and is the point I am principally looking to explain (it is also where the principal novelty of the proof lies). But in fact the idea of the proof of the other direction is fully present in the direction I have given here, one just needs a little extra step. I will explain this in the next significant update of the nLab page.
Have done some re-arranging, moving some things out of homotopy hypothesis for 1-types to other pages: fundamental groupoid of a cubical set and the cubical nerve of a groupoid (newly created), and cubical truncation, skeleton, and co-skeleton (some minor additions). I also now have an idea for addressing the point that I discussed here, which I hope to write up this evening.
Right now homotopy hypothesis for 1-types is looking pretty broken, e.g., the notation references. Please let us know when you have reached a resting spot where you are at momentarily satisfied.
Yes, sorry about that, I did not find time after all yesterday evening to work on the entry. I will post here when I have made the next update (probably this evening).
Have now fixed the broken stuff at homotopy hypothesis for 1-types as far as I can see, and made the notation consistent with the changes announced here. Also in light of those changes, added Corollary 2.
I am looking forward to writing the other direction of the equivalence, but will not have time this evening.
To add to my instiki TODO list: add a \ref{} which works across pages.
Please consider relative URLs for cross-links between pages: instead of
[Notation 3](https://ncatlab.org/nlab/show/fundamental+groupoid+of+a+cubical+set+and+the+cubical+nerve+of+a+groupoid#NotationFundamentalGroupoid)
better to code
[Notation 3](fundamental+groupoid+of+a+cubical+set+and+the+cubical+nerve+of+a+groupoid#NotationFundamentalGroupoid)
For one its shorter. But also it’s more robust: should the domain of the nLab ever change (again), then these relative links will stay intact.
Done, thanks!
Mostly as a note for myself, I would also like more details of Corollary 2, eventually.
I’m struggling a bit for time, and am unhappy with homotopy hypothesis for 1-types being in its current state. I will try here to outline how I think a nice proof can be given. Maybe somebody would be so kind as to try to help out with putting it on the nLab page, if they are sufficiently interested.
Here is the outline.
1) Replace by a category of algebraic structures which I’ll denote by , which is the same as a strict cubical 2-category also known as edge-symmetric double categories), but where we also have operations which provide certain 2-arrows: one which gives us inverses of 1-arrows ’up to homotopy’, for instance. (The category of topological spaces admits the same kind of structural homotopies).
2) Construct an adjunction between 2-truncated cubical sets and whose left adjoint is as follows: on the 1-truncation, it is the usual free category construction (we will need the explicit description using chains of 1-cubes), and on 2-cubes we do a similar kind of thing, after first throwing in the additional 2-arrows mentioned in 1). Let us denote the left and right adjoints by and respectively.
3) We show that the geometric realisation (to topological spaces) of the adjunction morphism is a homotopy equivalence as follows. We first define a morphism , which takes a zig-zag to the path obtained by composing together in all the paths in the zig-zag; and does something similar on 2-arrows. Because there is no equivalence relation on the arrows of , this is well-defined. The required homotopy inverse is then the geometric realisation of this morphism post-composed with the co-unit . One constructs the required homotopies using a similar trick, and some structural homotopies which exist in .
4) The category has a Gray-like monoidal structure. One defines a homotopy equivalence in using this and the obvious interval. One shows that the adjunction morphism is a homotopy equivalence in this sense by the same kind of argument as in 3) (indeed, this kind of argument can be probably be carried out in a purely abstract setting where the required structural homotopies exist).
5) From this, one should be able to deduce the more conventional statement of the homotopy hypothesis, by using the 2-coskeleton. That will then be enough to demonstrate the homotopy hypothesis at the level of homotopy categories. If we get this written up, I can explain how to bring model structures into the picture, etc.
I will be doing my best to put this in the entry myself. But I would be exceptionally happy if somebody would be interested in getting into this too. I do promise that there is a very rich and rewarding vein of ideas here!
Of course, what I have written here is very sketchy, but I’m happy to elaborate on anything. If people spur me to do so by asking questions, it will probably help the writing up go much faster!
If one wishes to give a more conventional argument, one can stick to and use homotopy groups. But I prefer the above!
1 to 11 of 11