Timeline for Equivariant homotopy, simplicially
Current License: CC BY-SA 3.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 31, 2014 at 14:57 | comment | added | Zhen Lin | @AntonFetisov The identification of equal things is not really a problem (after all, what are equal things if not identical?); rather it is that equality is too coarse in homotopy type theory for that purpose: a group inside HoTT will be more like some kind of $A_\infty$-group, actions will only be up to coherent homotopy, etc. | |
| Jan 31, 2014 at 12:33 | comment | added | Tim Porter | (I avoid $BG$ and prefer $G[1]$ for the corresponding groupoid.) I was meaning simplicially enriched functors (were you)? The actions that one gets are sensible in their interpretations. If you then go towards the questions you asked in the original post, then there may be a need to use the homotopy coherent nerve of $G[1]$ and to have homotopy actions to get something sensible. | |
| Jan 31, 2014 at 11:46 | comment | added | Anton Fetisov | I can reasonably see why functors $BG\to SSet$ should work for discrete groups. I'm not so sure if we start talking about the general ones. | |
| Jan 31, 2014 at 11:44 | comment | added | Anton Fetisov | I was talking about Higher Topoi, but HoTT also has relevance. My question stems from it: how do you define G-spaces in HoTT? Even if you shun some obvious problems (like defining categories and actions type-theoretically) the problem remains: HoTT cannot define the standard G-equivariant category, since it identifies equal objects, like equivalent types and homotopic maps (it would imply that $EG$ and $pt$ have the same type of G-structures). Since HoTT is very simplicial-like, the obvious first step would be to know what happens in $SSet$. | |
| Jan 31, 2014 at 11:43 | comment | added | Tim Porter | Another way forward is to encode things as being homotopy coherent. Think of $G$ (a simplicial group) as a simplicially entriched groupoid with one object, and then a $G$-simplicial set is just a functor from $G$ to $SSet$ and go on from there. | |
| Jan 31, 2014 at 11:41 | comment | added | Tim Porter | You say:it doesn't really explain what a G-space is, simplicially? It may do as then it is probably built up from various models such as that one by a colimiting process. | |
| Jan 31, 2014 at 11:38 | comment | added | Tim Porter | Can I ask why you do not want the presheaves on orbits idea? I can see that this may be awkward if $G$ is a simplicial group, but then the way forward may be to replace presheaves by $SSet/\overline{W}G$, and work with the Quillen m.c. structure on that. | |
| Jan 31, 2014 at 11:35 | comment | added | Tim Porter |
Which use of HTT are you intending? I know of homotopy type theory' and Lurie's homotopy topos theory', and perhaps you intend one of these or another that I have not thought of.
|
|
| Jan 31, 2014 at 11:32 | comment | added | Anton Fetisov | Thank you, Tim, I'll take a look at those papers. However, using $G/H \times \Delta^n$ seems just the same as considering simplicial presheaves on orbits. From this PoV the theory doesn't differ from the general HTT nonsense. While fun and useful, it doesn't really explain what a G-space is, simplicially. | |
| Jan 31, 2014 at 11:25 | history | answered | Tim Porter | CC BY-SA 3.0 |