Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorAli Caglayan
   • CommentTimeDec 18th 2018
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexStarted 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). <a href="https://ncatlab.org/homotopytypetheory/revision/spectrum/1">v1</a>, <a href="https://ncatlab.org/homotopytypetheory/show/spectrum">current</a>

   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).

   v1, current

2. • CommentRowNumber2.
   • CommentAuthorAli Caglayan
   • CommentTimeDec 18th 2018
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItexStarted 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). <a href="https://ncatlab.org/homotopytypetheory/revision/diff/spectrum/2">diff</a>, <a href="https://ncatlab.org/homotopytypetheory/revision/spectrum/2">v2</a>, <a href="https://ncatlab.org/homotopytypetheory/show/spectrum">current</a>

   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).

   diff, v2, current

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeDec 18th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexRe: 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 $E_{m,n}$ with equivalences $E_{m,n} \simeq \Omega E_{m+1,n} = \Map_{\ast}(S^1,E_{m+1,n})$ and also $E_{m,n} \simeq \Map_{\ast}(V,E_{m,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 $E_{m+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 $\mathbb{N}$-indexed spectra would specialize only to "naive" $G$-spectra).

   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 $E_{m,n}$ with equivalences $E_{m,n} \simeq \Omega E_{m+1,n} = \Map_{\ast}(S^1,E_{m+1,n})$ and also $E_{m,n} \simeq \Map_{\ast}(V,E_{m,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 $E_{m+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 $\mathbb{N}$-indexed spectra would specialize only to “naive” $G$-spectra).

4. • CommentRowNumber4.
   • CommentAuthorAli Caglayan
   • CommentTimeDec 18th 2018
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItex@Mike what would a representation sphere be in HoTT? Taking $V$ to be $S^1$ 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:\mathcal{U}$ equipped with an action $a : BG \to X$. If we construct spectra over these taking care with the action would we get "naive" G-spectra?

   @Mike what would a representation sphere be in HoTT?

   Taking $V$ to be $S^1$ 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:\mathcal{U}$ equipped with an action $a : BG \to X$. If we construct spectra over these taking care with the action would we get “naive” G-spectra?

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeDec 18th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexA [[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$.

   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$.

6. • CommentRowNumber6.
   • CommentAuthorAli Caglayan
   • CommentTimeDec 18th 2018
   • PermaLink
   Author: Ali Caglayan
   Format: MarkdownItex@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](https://ncatlab.org/nlab/show/equivariant+homotopy+group#definition)? 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.

   @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.

7. • CommentRowNumber7.
   • CommentAuthorDavid_Corfield
   • CommentTimeDec 18th 2018
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexHave people here been following what Urs is doing with Charles Rezk's global equivariant cohesion from about [here](https://nforum.ncatlab.org/discussion/8915/orbifold-cohomology/?Focus=74239#Comment_74239)?

   Have people here been following what Urs is doing with Charles Rezk’s global equivariant cohesion from about here?

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeDec 19th 2018
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThere 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 $O_G$-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 $O_G$, thereby including all of the $\pi_n^H$ at once, even though $H$ isn't visible internally.

   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 $O_G$-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 $O_G$, thereby including all of the $\pi_n^H$ at once, even though $H$ isn’t visible internally.