From: Ali Caglayan <alizter@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] Localising spheres in HoTT
Date: Sat, 11 Aug 2018 13:58:54 -0700 (PDT) [thread overview]
Message-ID: <a08e064b-a25e-4e29-beb7-6bee00ff1871@googlegroups.com> (raw)
[-- 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 --]
next reply other threads:[~2018-08-11 20:58 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-08-11 20:58 Ali Caglayan [this message]
2018-08-15 8:51 ` Michael Shulman
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=a08e064b-a25e-4e29-beb7-6bee00ff1871@googlegroups.com \
--to=alizter@gmail.com \
--cc=HomotopyTypeTheory@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
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).