Stable homotopy groups

[fredrik-bakke]

Building on #834, a next goal is to define stable homotopy groups. Some intermediate steps include

• Define colimits of sequential diagrams of pointed types
• Prove the Freudenthal Suspension theorem
• Define the stable homotopy groups as colimits of sequential diagrams of pointed types
• Prove that the stable homotopy groups are attained at finite indices of these sequential diagrams using the Freudenthal Suspension theorem
• Define the homotopy groups of prespectra
• Show that the stable homotopy groups agree with the homotopy groups of the sphere prespectrum in non-negative degrees

References

• Homotopy Type Theory – Univalent Foundations of Mathematics, chapter 8

[djspacewhale]

This is a hacky approach and maybe a direct colimit definition would be more tractable (I'm working on homotopy groups currently...), but stable homotopy groups do form a generalized homology theory and we already have smash products and the sphere prespectrum. Is the genuine sphere spectrum tractable from this? Doesn't look like we have the spectrification functor defined, but I'm relatively new to stable homotopy stuff and don't know if the sphere spectrum is independently definable except as "the spectrification of the sphere prespectrum" or "the free infinite loop space on a point".

[fredrik-bakke]

This is a hacky approach and maybe a direct colimit definition would be more tractable (I'm working on homotopy groups currently...),

Nice! @EgbertRijke has done some initial work on homotopy groups in an unmerged branch here: #836. Keep in mind that it is very desirable to have good infrastructure and good definitions for the basic concepts relating to homotopy theory, so that it can be built upon with minimal friction.

but stable homotopy groups do form a generalized homology theory and we already have smash products and the sphere _pre_spectrum. Is the genuine sphere spectrum tractable from this? Doesn't look like we have the spectrification functor defined, but I'm relatively new to stable homotopy stuff and don't know if the sphere spectrum is independently definable except as "the spectrification of the sphere prespectrum" or "the free infinite loop space on a point".

Indeed, I would anticipate that this is one potential way to do it. However, spectrification is a complicated construction, and it is unclear to me whether it lets itself formalize (easily). Attempts at formalizing it are most welcome!

In case it is of help in your review of the field, here are some references on stable homotopy theory in HoTT:

1. Synthetic cohomology theory in homotopy type theory by Evan Cavallo, PhD thesis. This resource introduces some fundamentals of spectra and cohomology theories in HoTT.
2. Higher groups in homotopy type theory by Buchholtz, van Doorn and Rijke. This resource considers infinitely deloopable spaces among other things.
3. Synthetic homology theory in homotopy type theory by Robert Graham. This resource uses stable homotopy groups to define homology.
4. Eilenberg–Maclane spaces and stabilisation in homotopy type theory by David Wärn. I am unsure of the relevance of this resource, but perhaps it is useful to have a look at.
5. A bunched homotopy type theory for synthetic stable homotopy theory by Mitchell Riley, PhD thesis. This resource explores an extension of HoTT where parametrized spectra are basic objects. Perhaps it gives some pointers to what can and cannot be done (or is exceedingly hard) with spectra in basic HoTT.