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.
1 to 32 of 32
For the past week or so I’ve been trying to analyse Kan’s functor in the constructive setting and I keep running into difficulties because I don’t have a geometric realisation functor at hand. Here’s an attempt to construct a surrogate – but it has a nasty flaw I don’t know how to fix.
To begin, let be the category of simplicial sets (or even just finite simplicial sets). Barycentric subdivision defines an endofunctor . Any reasonable geometric realisation functor should have the property that naturally in ; unfortunately, we cannot expect the isomorphism to come from a morphism in , so the usual trick of inverting morphisms won’t work here. Instead, we borrow an idea from stable homotopy theory: if we take to be the (strict) colimit of the sequence
then there is an induced automorphism . Unfortunately, it is only an outer automorphism; to fix this, we take the pseudo-quotient of by the induced -action to get a category with an inner automorphism .
The categories and have the following explicit descriptions:
Sadly, this does not work as well as one might hope. Because acts trivially (up to natural isomorphism) on discrete simplicial sets, the image of ends up having as its automorphism group in . This makes no sense geometrically and induces an unwanted free -action on the the set of “points” of in . Does anyone have any thoughts about how this might be fixed?
What does it mean to say that an automorphism of a category is “outer” or “inner”?
An inner automorphism is one that is isomorphic (as a functor) to the identity. This agrees with the definition from group theory.
Rrrgh, it would agree with the definition from group theory if groups were the same as one-object groupoids. But they’re not. (-:
In category theory, why not just say that such a functor “is the identity”?
The functor as it depends on the very ‘unnatural’ barycentric realisation is bound to be a bit weird. (It is very unnatural at the level of the simplicial sets.) Why not try the ordinal subdivision and any associated completion functor? As the ordinal subdivision works in the models it may be easier to work with. (It depends of course why you are wanting in the first place.)
Hello Zhen Lin,
I was just wondering where your difficulties lie in working with constructively?
I ask because some collaborators (Espen Auseth Nielsen, Erik Rybakken, and Marius Thaule) and I have a proof that is weakly equivalent to for cubical sets that I would consider to be both conceptual and constructive in a very strong sense (it is very different to the usual proof for simplicial sets). Here ’weakly equivalent’ means homotopy equivalent (which we show directly, without appealing to Whitehead’s theorem) after taking the geometric realisation. A paper is in preparation that should be finished quite soon.
This might be irrelevant for your purposes, as I’m not quite sure what you mean by ’not having a geometric realisation functor to hand’; why working constructively means that you do not have one; or exactly what you are trying to achieve with your replacement construction!
I agree with Tim that there is not much hope for naturality of the homeomorphism that you are looking for when using the barycentric subdivision. I recommend the work of Fritsch for more on this (I gave some more precise references in another thread on the simplicial approximation theorem earlier this year).
I am led to believe that topological spaces should be avoided in constructive mathematics. The main difficulty in working with is showing that the canonical embedding is a weak homotopy equivalence (in the sense of becoming a weak homotopy equivalence of Kan complexes, defined combinatorially, after applying ). However, it is more or less clear geometrically why it should be a weak homotopy equivalence.
Regardless, as much as I would like to solve that problem, it is not what I am asking about here. The difficulty with the construction is common to any subdivision functor that acts trivially on . The motivating picture is the simplicial approximation theorem: that is why I want to “become” the identity.
I have thought long and hard about these kind of questions for some years, it is interesting that you are pursuing them too!
With regard to avoiding topological spaces in constructive mathematics, I understand what you mean. If one thinks about it, one rapidly comes to the conclusion that any proof of Milnor’s theorem that is a weak equivalence, for instance via a simplicial/cubical approximation theorem, will rely ultimately on the compactness of the unit interval, and it is impossible to prove that constructively for the usual notion of a topological space. However, I do not necessarily draw from this the conclusion that we should avoid topological spaces at all.
Topological spaces have a lot of structure that does not exist in the category of simplicial/cubical sets. From my point of view, this comes down to the structure of the unit interval: one has what I call (after Kamps, Brown and Higgins, Tim, etc) a ’subdivision structure’, which allows one to compose homotopies. This is impossible in any presheaf model of homotopy types. There are also many other structures (involution, connections, …), but one could modify the definition of the category of cubes, for instance, to include all of these, except those involving a ’subdivision structure’.
This extra structure is crucial for the foundations of homotopy theory. If one wishes to avoid topological spaces, one needs to find this extra structure somewhere else. I think that Kan complexes themselves are something of a will-of-the-wisp here. They are very poorly behaved constructively. One needs, I believe, at least to work not with the category of Kan complexes, but with the category of algebraic Kan complexes. The latter category does have a ’subdivision structure’, but working with it introduces its own difficulties.
For instance, I have thought a lot about equipping the category of cubical sets with a model structure in a constructive way, which is Quillen equivalent to the Serre model structure on Top (or, if you prefer, the usual model structure on cubical sets). I understand conceptually how to do this (it is, as with much of my work in this area and related work on the homotopy hypothesis, in the process of being written up!). There are a number of possible approaches, but one of them was in fact my original motivation for the work on the functor that I mentioned above: one can equip the category of algebraic Kan complexes with a model structure via my thesis in a constructively valid way, and then the idea would be to ’transfer’ this model structure (in a way which, again, I understand, and which is in the process of being written up) to the entire category of cubical sets using .
This ’transfer’ is also constructive (and has nothing to do with the criterion for ’transfer of model structures across an adjunction’ that is well known). The fact that we can prove that is a weak equivalence in the sense of my previous comments demonstrates that this model structure is Quillen equivalent to the usual one.
One has to, though, prove that is a Kan complex, or an algebraic Kan complex, in a constructively valid way, and check various other things. This is my main point: working constructively in homotopy theory does not just mean not using topological spaces! There are also other categories than algebraic Kan complexes that one can use, or one could work with a constructive variant of topological spaces instead.
With regard to proving that the canonical arrow is a weak homotopy equivalence, yes, geometrically one can easily see it in low dimensions, but it is another matter entirely to write down a rigorous proof. The only proof that I am aware of for simplicial sets is very indirect and non-constructive, reducing to Milnor’s theorem and an argument on homotopy groups. One of the main aspects of our work is to give a conceptual way to pass from ’geometric intuition in low dimensions’ to a rigorous proof. For this, the fact that we work with cubical sets, where one has universal properties that are not available in the simplicial setting, is essential, and this is something that I am generally convinced of: cubical sets are much better than simplicial sets for the foundations of homotopy theory, if one wishes to work conceptually and constructively!
Moreover, our proof in fact relies on nothing about Top except the existence of the structures that I mentioned, so could be carried out for any ’alternative’ category (and we are writing it up in this generality). In particular, it does not rely on any of the non-constructive aspects of topological spaces.
Feel free to get in touch over email if you would like to know more about any aspects of this!
Kan complexes are not that badly behaved constructively. Actually, my view is that it is model structures, or more precisely, weak factorisation systems that are badly behaved constructively. For instance, (following van Osdol) using the completeness theorem for regular logic, I can prove that the category of Kan complexes in any regular category forms a category of fibrant objects. It is only slightly harder to transfer the fact that is a fibrant replacement functor over to the setting of -pretoposes. I am confident that we can prove that is a Kan complex in the setting of elementary toposes with NNO – Kan’s original proof should still work. The hard part is proving that is weakly homotopy equivalent to itself. There is no need to select preferred liftings.
As for subdivision: the whole point of the construction I outline in my first post is to obtain a combinatorial model of spaces where the standard simplices are isomorphic to their subdivisions.
From my point of view, this comes down to the structure of the unit interval: one has what I call (after Kamps, Brown and Higgins, Tim, etc) a ’subdivision structure’, which allows one to compose homotopies.
An excellent point. Compare the terminal coalgebra characterization of the unit interval due to Freyd, where the coalgebra structure = subdivision structure , a bipointed map, is what we use to compose homotopies.
Actually, my view is that it is model structures, or more precisely, weak factorisation systems that are badly behaved constructively.
I guess it depends upon what one means by badly behaved, but I agree that it is a very tricky matter to obtain weak factorisation systems constructively, and that to settle for only ’half’ a model structure is much easier. However, there are, of course, reasons that one would like a full model structure. Moreover, I have found it possible to obtain weak factorisations systems constructively, and have found that the methods have given me a lot of insight that I would have not have been led to if I had not been working constructively. This is what the methods of my thesis and the ’transfer’ method that I mentioned concern.
Kan complexes are not that badly behaved constructively.
Again, it obviously depends upon what one means by badly behaved, but I don’t see how one can prove anything constructively about a Kan complex which does not have lifts as part of the structure. In other words, take an arbitrary horn: how do you obtain the ’filling’ constructively? Of course, if one interprets ’there exists’ constructively, there is no problem, but this is exactly to ask for given liftings.
However, it is not the given liftings that are significant about the category of algebraic Kan complexes for the purposes of my previous comment, but the fact that the morphisms preserve these liftings. This gives the category of algebraic Kan complexes a completely different feel from that of ordinary Kan complexes, and is the reason that a subdivision structure exists.
The hard part is proving that is weakly homotopy equivalent to itself. There is no need to select preferred liftings.
Yes, as I wrote, we can prove this cubically, and Kan complexes (with or without specified liftings) do not play any role in the proof. In fact, though, cubically (with connections), it is not that easy to give a nice proof that is a Kan complex, though it is clear geometrically in low dimensions. I agree that the standard proof in the simplicial setting is not difficult, although I feel that the heart of the matter is better captured in a cubical setting.
As for subdivision: the whole point of the construction I outline in my first post is to obtain a combinatorial model of spaces where the standard simplices are isomorphic to their subdivisions.
A ’subdivision structure’ in the sense of my comment has a precise meaning, as in Todd’s comment, which is a priori unrelated to subdivision in the sense you are using it here.
However, I have in fact considered before the kind of idea that you are looking at here, and think it is a very interesting one. I usually think of it as trying to define a foundational category for ’piecewise-linear topology’. One needs to allow morphisms of cubical/simplicial sets ’up to subdivision’. This category does admit a subdivision structure in the technical sense.
There is a well-understood interpretation of intuitionistic logic in elementary toposes. The meaning of in that setting is, roughly speaking, “there locally exists”. The difference between “there locally exists” and “there globally exists” is a subtle one: for instance, any epimorphism satisfies , but that does not mean that every epimorphism splits! But the problem with weak factorisation systems goes deeper than the interpretation of ; for instance, the assertion that the left class is closed under coproducts is equivalent to the axiom of choice. This is not so bad in ultra-constructive settings where is interpreted very strictly like you suggest, but I am more interested in the topos setting.
Yes, I thought that you might have been thinking of in this way. My experience is that once one gives a constructive interpretation, one has to adapt many other aspects of the theory of Kan complexes: one needs to ask for certain kinds of compatibilities between the lifts, or ask for other kinds of structures, as in the recent work of Bezem, Coquand, and Huber. Whilst I have focused on very strong interpretations of constructivity, I would be surprised if these aspects do not manifest themselves in the topos theoretic setting too.
But the problem with weak factorisation systems goes deeper than the interpretation of ∃; for instance, the assertion that the left class is closed under coproducts is equivalent to the axiom of choice. This is not so bad in ultra-constructive settings where ∃ is interpreted very strictly like you suggest
Yes, exactly. Usually one has to work so hard to construct the weak factorisation system in the kind of constructive setting that I work with, that one has a very good understanding of the arrows involved, and does not have any need for facts about the arrows that follow formally from having a weak factorisation system!
Zhen Lin,
What if you consider your diagram not as a diagram of categories, but as a diagram of categories under the category of sets (viewed as the discrete simplicial sets)? It seems like that might cancel out the extra integers worth of automorphisms for these objects.
@Richard Williamson
Yes, I thought that you might have been thinking of in this way. My experience is that once one gives a constructive interpretation, one has to adapt many other aspects of the theory of Kan complexes: one needs to ask for certain kinds of compatibilities between the lifts, or ask for other kinds of structures, as in the recent work of Bezem, Coquand, and Huber. Whilst I have focused on very strong interpretations of constructivity, I would be surprised if these aspects do not manifest themselves in the topos theoretic setting too.
I do not know. However, I remain unconvinced of your assertion that Kan complexes are badly behaved: the fact of the matter is that Kan complexes in Grothendieck toposes have been studied for quite a long time, and at the very least, the homotopy category of Kan complexes in a Grothendieck topos is equivalent to the homotopy category of the corresponding (model!) category of hypersheaves. If something goes wrong in the case of elementary toposes with NNO, that would (to me) suggest a subtle interplay between homotopy theory and arithmetic. That would not be surprising if geometric realisation (and hence ) were somehow indispensible in homotopy theory, but we already know that geometric realisation is not needed in classical mathematics.
Anyway, getting back to the original topic:
@Chris Schommer-Pries
What if you consider your diagram not as a diagram of categories, but as a diagram of categories under the category of sets (viewed as the discrete simplicial sets)? It seems like that might cancel out the extra integers worth of automorphisms for these objects.
I’m not sure what you mean. Slicing under an object doesn’t change connected colimits. But I had a similar thought: since is always a simplicial complex, we could just quotient out by the equivalence relation that makes two morphisms equal if they agree on vertices.
More precisely, is -equivariant (up to natural isomorphism), so we get an induced functor . Forcing this functor to be faithful kills the unwanted automorphisms and hopefully leaves everything else intact…
However, I remain unconvinced of your assertion that Kan complexes are badly behaved: the fact of the matter is that Kan complexes in Grothendieck toposes have been studied for quite a long time, and at the very least, the homotopy category of Kan complexes in a Grothendieck topos is equivalent to the homotopy category of the corresponding (model!) category of hypersheaves. If something goes wrong in the case of elementary toposes with NNO, that would (to me) suggest a subtle interplay between homotopy theory and arithmetic. That would not be surprising if geometric realisation (and hence R) were somehow indispensible in homotopy theory, but we already know that geometric realisation is not needed in classical mathematics.
I don’t know exactly what you are trying to do, and, of course, you may be able to work constructively with ordinary Kan complexes to achieve it! I do not particularly see that the facts you mention are closely related to the sense in which I asserted that they are, from a certain constructive point of view, badly behaved, though!
But this is not important: I just wished to record the observation, in case you or anyone else reading finds it helpful, that I have found, in the constructive setting in which I work, the category of Kan complexes to be badly behaved/not nice enough if one is trying to erect constructively a foundations for homotopy theory on a category of presheaves, and that if you/anybody else reading arrives at this conclusion too, there are alternatives; that , by which I really mean and not one of its cartesian closed variants, is actually a very nice category for many (not all!) purposes in homotopy theory, and that it is worth considering replacing it by a constructive variant as opposed to ignoring it completely; and that it is possible constructively to prove the result that you are looking for in a cubical setting.
In addition, I wished to say that a variant of the category that you consider is definitely interesting (to me!), and admits a notion of ’geometric realisation’ for which one can prove that is a homotopy equivalence in this category. This may not be helpful for your purposes, though.
since Sd(X) is always a simplicial complex
This is not necessarily the case. This is closely related to Tim’s comment and my first comment. See my comment on the simplicial approximation theorem that I referred to earlier.
Hmmm, yes. As long as is “eventually” a simplicial complex, there should be no problem.
Unfortunately, as can be seen in the example of the model of 2-sphere mentioned in the other thread, one may never obtain a simplicial complex by iterated barycentric subdivision! If one uses semi-simplicial sets, one obtains a simplicial complex after two steps. There are ways to do it for cubical sets in one step.
Ah. That’s annoying. Ordinal subdivision doesn’t work there either.
Perhaps it doesn’t actually matter? The barycentre of every “simplex” in is itself a vertex, so there shouldn’t be any essential information lost by passing to the map of vertices.
I believe one particular thing that goes wrong with Kan complexes constructively is that even if they are algebraic, one cannot prove that is a Kan complex when and are, not unless the degenerate simplices are a decidable subset. Thierry Coquand has thought a lot about these issues in the attempt to produce a constructive model of the univalence axiom, and ended up using cubical sets instead; you may want to ask his opinion.
Re: second half of 15:
Slicing under Sets does change the “pseudo-quotient”. In particular you note that on D the functor Sd is not equivalent to the identity, however when restricted to Set it becomes the trivial functor (with a canonical trivialization). Now when you take the “pseudo-quotient” in categories under Set, you universally trivialize the Z action, but subject to the condition that it agrees with the trivial trivialization on Set. This is different than your category E.
@Mike Shulman
That makes sense. Even in a cartesian model category, we should only expect to be fibrant when is cofibrant and is fibrant. For instance, on a site with the “chaotic” topology (Why isn’t there a good name for this?!), the locally fibrant simplicial presheaves coincide with the projectively fibrant simplicial presheaves, but in general not all simplicial presheaves are projectively cofibrant. Having “free degeneracies” is a sufficient condition for cofibrancy in this case.
@Chris Schommer-Pries
I see now, yes. It sounds like a good idea, but I do not know how to compute that pseudo-quotient. I guess it should be the same as taking the strict quotient of by the smallest congruence that makes all the automorphisms of the discrete things trivial? In that case we would get a comparison between your construction and the category described at the end of #15. With luck, it will be an isomorphism…
Perhaps it doesn’t actually matter? The barycentre of every “simplex” in Sd∞ is itself a vertex, so there shouldn’t be any essential information lost by passing to the map of vertices.
I don’t quite follow here: it seems to me that one will definitely lose information.
[Edit: My instinct is that the construction you are trying to carry out is a little contrived: it seems unlikely to me that one can ’force’ it to work in the manner you are trying. There are various other categories and realisation functors that one can consider that, to me, have a more ’conceptual’ feel, such as by an appropriate localisation in the sense of Bousfield that I had originally mentioned here, but it does not, following subsequent discussion, seem that it would achieve much to outline them here.]
No, I definitely do not want to localise at morphisms or . For one thing, those morphisms generally do not become homeomorphisms after geometric realisation.
Then I am somewhat lost as to what you are trying to achieve!
Indepedently of what you are trying to do, the localised category that I mentioned is a very interesting category in this circle of ideas. The way that I am looking at it, whether or not we are localising at arrows which become homeomorphisms after topological geometric realisation is irrelevant.
If you are looking for a natural homeomorphism between the topological geometric realisations of and , then, as TIm and I mentioned towards the top of the thread, there is not much hope, as you will see if you look at the work of Fritsch!
[Edit: Just for clarity, in case anyone stumbles on this thread in the future: the two possible arrows that I was referring to are . I got my wires crossed slightly with another setting that I am working on when I wrote the description of the localised category, but the essential idea is the same.]
I don’t actually know what morphisms you are referring to. There is a natural morphism but it does not split in general.
The fact that the geometric realisations of and are not naturally homeomorphic is unfortunate. That does not change the fact that they are homeomorphic, at least for simplicial complexes .
Yes, they are homeomorphic for all simplicial/cubical sets. What I have lost is the thread of your reflections, but it’s no problem, maybe somebody else can help.
[Edit: with regard to the direction of the morphisms, my apologies, I got my wires crossed with some other setting that I am working in. I was thinking of the two morphisms , and their analogues for higher cubes. You are absolutely correct that we have a morphism , and that we do not in general have an interesting morphism in general the other way.]
Since when did the topic of discussion change to cubical sets???
I would have thought that it would be possible to discuss on this thread matters around and closely related to the question that you asked, and maybe there are others than yourself who are/might have been interested in that discussion. Considering not only simplicial but cubical sets, especially since you are trying to work constructively and I have been arguing (as are others, such as Coquand, as Mike mentioned) that cubical sets have advantages over simplicial sets for this, would not seem too large a leap.
However, it is absolutely fine for me if you are not interested, and I will cease the conversation here.
I am aware that cubical sets have advantages, just as I am aware that topological spaces have advantages. However, I am trying to understand what is happening for simplicial sets, if only because there are so many simplicial constructions that need to be accounted for. For instance, the Čech nerve of a covering, the ordinary nerve of a category, the theory of simplicial resolutions…
The philosophy from the point of view of cubical sets would, naturally, be to adapt these constructions to the cubical setting. I have worked a lot with cubical nerves of ordinary and higher categories, for instance, and have again found advantages over the simplicial ones.
Anyhow, best of luck with your work on this, and I hope that you can get your idea to work for you!
1 to 32 of 32