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.
Started a page on spectra. Haven’t got the energy to finish this right now. I will add more in the future and link it to some more literature. The most comprehensive study of them is stil however Floris’ thesis. I want to also talk about alternative definitions (such as changing the indexing or coinduction. Coinduction would however force me to mention non-wellfounded trees and their inestigation by Ahrens et. al.).
I have also added some links on some possible future pages (but for now it probably seems appropriate to write them up all here).
Started a page on spectra. Haven’t got the energy to finish this right now. I will add more in the future and link it to some more literature. The most comprehensive study of them is stil however Floris’ thesis. I want to also talk about alternative definitions (such as changing the indexing or coinduction. Coinduction would however force me to mention non-wellfounded trees and their inestigation by Ahrens et. al.).
I have also added some links on some possible future pages (but for now it probably seems appropriate to write them up all here).
Re: changing the indexing, one possibility that I think ought to be explored is spectra that also “deloop” by an arbitrary pointed type V, so you have a doubly-indexed grid Em,n with equivalences Em,n≃ΩEm+1,n=Map*(S1,Em+1,n) and also Em,n≃Map*(V,Em,n+1). And perhaps generalized to finite families of such types V. It’d be tricky because you want some commutativity between the two equivalences for Em+1,n+1, but might be doable at least for a single type V. I think this would be useful semantically because in models of equivariant homotopy theory it could be specialized to “genuine” G-spectra by taking the V types to be the representation spheres (whereas the ordinary ℕ-indexed spectra would specialize only to “naive” G-spectra).
@Mike what would a representation sphere be in HoTT?
Taking V to be S1 would give us something that is a spectrum in two directions. With proper commutativity of equivalences I can imagine a doubly-indexed grid with equivalent diagonals. Which would easily be flattened into the usual notion of spectrum. I have no idea what a representation sphere is really, but surely it would be more natural to stick a BG as V. I can’t help but feel I am missing something obvious here.
I can conjure up a definition of G-space, some X:𝒰 equipped with an action a:BG→X. If we construct spectra over these taking care with the action would we get “naive” G-spectra?
A representation sphere isn’t something you can expect to define in HoTT (at least, I don’t see any way to do it); it’s something that exists in a particular “nonstandard” model (equivariant homotopy theory) that would just have to be postulated internally as an unspecified type when interpreting type theory in that model. I’m not talking about having a G inside type theory that acts on things, but about a model of all of HoTT in which all types are interpreted as G-spaces for some meta-theoretic group G.
@Mike ah that makes more sense now. So this “G-HoTT” would give us the “usual” HoTT for trivial G? I don’t see how the meta-theoretic group G interacts with what goes on internally though. For example how would we define unstable H-equivariant homotopy groups? It seems to me that H is another metatheoretic group. In which case what does it mean to have fixed points of a type with respect to a metatheoretic group.
Have people here been following what Urs is doing with Charles Rezk’s global equivariant cohesion from about here?
There is no separate “G-HoTT”, it’s just regular HoTT that can be interpreted in G-spaces. But it’s really better to think of G-spaces as OG-spaces here, by Elmendorf’s theorem. The homotopy groups in HoTT are defined internally in HoTT, so when interpreted in that model they are also “G-objects”, or more precisely diagrams of sets indexed by OG, thereby including all of the πHn at once, even though H isn’t visible internally.
1 to 8 of 8