*[HoTT] Localising spheres in HoTT@ 2018-08-11 20:58 Ali Caglayan2018-08-15 8:51 ` Michael Shulman 0 siblings, 1 reply; 2+ messages in thread From: Ali Caglayan @ 2018-08-11 20:58 UTC (permalink / raw) To: Homotopy Type Theory [-- Attachment #1.1: Type: text/plain, Size: 2476 bytes --] So I have been reading https://arxiv.org/abs/1807.04155 In it they detail a construction for localising types at a prime. I want to construct ΩS²ⁿ⁺¹₍₂₎, this is an important space because it appears in the James fibration from classical algebraic topology: Sⁿ₍₂₎ --> ΩSⁿ⁺¹₍₂₎ --> ΩS²ⁿ⁺¹₍₂₎ This is the fibration that gives the EHP spectral sequence at p=2 and allows one to compute homotopy groups (at least 2-primary parts) inductively. So, in HoTT one can hope for a type family ΩS²ⁿ⁺¹₍₂₎ --> U, which has the proper fiber and base space. Now as far as I know, the only homotopy theoretic fibrations that have been formalised in HoTT are the Hopf-fibrations and their general H-space construction. So this is really two questions: 1. How to define ΩS²ⁿ⁺¹₍₂₎ 2. How to come up with the HoTT version of the James fibration Now the first one is kind of already done. Heres how to construct it: Let S : N -> N be defined as S(k) = k if k is prime and k =/= 2. S(k) = 1 otherwise. Now by theorem 4.20, we can define s : N -> N by s(k) = prod 0<=n<=k S(k). So s(k) is the product of all primes less than k, excluding 2. Now consider the diagram: 1 1 1 3 3 3.5 3.5 s(7) X ----> X ----> X ----> X ----> X ----> X ----> X ----> X ----> .... Where the integers k denote the deg(k) map, and X is ΩS²ⁿ⁺¹. The colimit of this diagram should be our desired space ΩS²ⁿ⁺¹₍₂₎. If you recall from the HoTT book, the colimit of a diagram has constructors for each node in the graph, and each arrow. I haven't really worked out the details but this should give us some higher inductive type which is (at least) equivalent to ΩS²ⁿ⁺¹₍₂₎. I'm not even sure this is the kind of HIT that you can write down. Here are my questions: 1. Can we write down a HIT for a type localised at a prime? 2. Does anybody know any work on other fibration in HoTT? 3. Do you think that localisation methods from classical algebraic topology will work in HoTT? -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. [-- Attachment #1.2: Type: text/html, Size: 3068 bytes --] ^ permalink raw reply [flat|nested] 2+ messages in thread

*2018-08-11 20:58 [HoTT] Localising spheres in HoTT Ali CaglayanRe: [HoTT] Localising spheres in HoTT@ 2018-08-15 8:51 ` Michael Shulman0 siblings, 0 replies; 2+ messages in thread From: Michael Shulman @ 2018-08-15 8:51 UTC (permalink / raw) To: Ali Caglayan;+Cc:HomotopyTypeTheory Localizations at arbitrary families of maps are constructed in arXiv:1706.07526 using a recursive HIT. Egbert Rijke has shown that in the case of localizing at maps between omega-compact types, such as circles and spheres (therefore including this case), the localization can be constructed as a non-recursive sequential colimit which is at least similar to the classical construction as a telescope; but I don't think this work is published anywhere yet. On Sat, Aug 11, 2018 at 1:58 PM Ali Caglayan <alizter@gmail.com> wrote: > > So I have been reading https://arxiv.org/abs/1807.04155 > > In it they detail a construction for localising types at a prime. I want to construct ΩS²ⁿ⁺¹₍₂₎, this is an important space because it appears in the James fibration from classical algebraic topology: > > Sⁿ₍₂₎ --> ΩSⁿ⁺¹₍₂₎ --> ΩS²ⁿ⁺¹₍₂₎ > > This is the fibration that gives the EHP spectral sequence at p=2 and allows one to compute homotopy groups (at least 2-primary parts) inductively. > > So, in HoTT one can hope for a type family ΩS²ⁿ⁺¹₍₂₎ --> U, which has the proper fiber and base space. Now as far as I know, the only homotopy theoretic fibrations that have been formalised in HoTT are the Hopf-fibrations and their general H-space construction. > > So this is really two questions: > > 1. How to define ΩS²ⁿ⁺¹₍₂₎ > 2. How to come up with the HoTT version of the James fibration > > Now the first one is kind of already done. Heres how to construct it: > > Let S : N -> N be defined as S(k) = k if k is prime and k =/= 2. S(k) = 1 otherwise. Now by theorem 4.20, we can define s : N -> N by s(k) = prod 0<=n<=k S(k). So s(k) is the product of all primes less than k, excluding 2. > > Now consider the diagram: > 1 1 1 3 3 3.5 3.5 s(7) > X ----> X ----> X ----> X ----> X ----> X ----> X ----> X ----> .... > > Where the integers k denote the deg(k) map, and X is ΩS²ⁿ⁺¹. The colimit of this diagram should be our desired space ΩS²ⁿ⁺¹₍₂₎. > > If you recall from the HoTT book, the colimit of a diagram has constructors for each node in the graph, and each arrow. I haven't really worked out the details but this should give us some higher inductive type which is (at least) equivalent to ΩS²ⁿ⁺¹₍₂₎. I'm not even sure this is the kind of HIT that you can write down. > > Here are my questions: > > 1. Can we write down a HIT for a type localised at a prime? > 2. Does anybody know any work on other fibration in HoTT? > 3. Do you think that localisation methods from classical algebraic topology will work in HoTT? > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. ^ permalink raw reply [flat|nested] 2+ messages in thread

end of thread, other threads:[~2018-08-15 8:51 UTC | newest]Thread overview:2+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2018-08-11 20:58 [HoTT] Localising spheres in HoTT Ali Caglayan 2018-08-15 8:51 ` Michael Shulman

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).