Article
Full entry |
PDF
(0.7 MB)
Feedback
PDF
(0.7 MB)
Feedback
Keywords:
Homotopy type theory; synthetic homotopy theory; univalence axiom; localization; reflective subuniverse; separated type
Homotopy type theory; synthetic homotopy theory; univalence axiom; localization; reflective subuniverse; separated type
Summary:
We study localization at a prime in homotopy type theory, using self maps of the circle. Our main result is that for a pointed, simply connected type $X$, the natural map $X \rightarrow X_{(p)}$ induces algebraic localizations on all homotopy groups. In order to prove this, we further develop the theory of reflective subuniverses. In particular, we show that for any reflective subuniverse $L$, the subuniverse of $L$-separated types is again a reflective subuniverse, which we call $L'$. Furthermore, we prove results establishing that $L'$ is almost left exact. We next focus on localization with respect to a map, giving results on preservation of coproducts and connectivity. We also study how such localizations interact with other reflective subuniverses and orthogonal factorization systems. As key steps towards proving the main theorem, we show that localization at a prime commutes with taking loop spaces for a pointed, simply connected type, and explicitly describe the localization of an Eilenberg-Mac Lane space $K(G,n)$ with $G$ abelian. We also include a partial converse to the main theorem.
References:
[1] Avigad, J., Kapulkin, K., Lumsdaine, P. LeFanu: Homotopy limits in type theory. Math. Structures Comput. Sci., Vol. 25, Iss. 5, 1040-1070, DOI:10.1017/S0960129514000498 DOI 10.1017/S0960129514000498
[2] Bousfield, A. K.: Localization and periodicity in unstable homotopy theory. J. Amer. Math. Soc., Vol. 7, Iss. 4, 831-873, DOI:10.2307/2152734 DOI 10.1090/S0894-0347-1994-1257059-7
[3] Brunerie, G.: On the homotopy groups of spheres in homotopy type theory. https://arxiv.org/abs/1606.05916
[4] Buchholtz, U., Doorn, F., Rijke, E.: Higher groups in homotopy type theory. Proceedings of the 33rd annual ACM/IEEE symposium on logic in computer science, pp 205-214, DOI:10.1145/3209108.3209150 DOI 10.1145/3209108.3209150
[5] Casacuberta, C., Peschke, G.: Localizing with respect to self-maps of the circle. Trans. Amer. Math. Soc., Vol. 339, Iss. 1, 117-140, DOI:10.2307/2154211 DOI 10.1090/S0002-9947-1993-1123451-X
[6] Doorn, F., Rijke, E., Sojakova, K.: Identity types of sequential colimits. In preparation
[7] Farjoun, E. D.: Cellular spaces, null spaces and homotopy localization. Lecture notes in mathematics, Springer-Verlag, Berlin, DOI:10.1007/BFb0094429 DOI 10.1007/BFb0094429
[8] Kapulkin, K., Lumsdaine, P. LeFanu: The homotopy theory of type theories. Advances in Mathematics, Vol. 337, 1-38, DOI:10.1016/j.aim.2018.08.003 DOI 10.1016/j.aim.2018.08.003
[9] Licata, D. R., Finster, E.: Eilenberg-MacLane spaces in homotopy type theory. Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp Article No. 66, DOI:10.1145/2603088.2603153 DOI 10.1145/2603088.2603153
[10] Lumsdaine, P. LeFanu, Shulman, M.: Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society, DOI:10.1017/S030500411900015X DOI 10.1017/S030500411900015X
[11] May, J. P., Ponto, K.: More concise algebraic topology. Chicago lectures in mathematics, University of Chicago Press, Chicago, IL
[12] Rijke, E.: The join construction. https://arxiv.org/abs/1701.07538
[13] Rijke, E., Shulman, M., Spitters, B.: Modalities in homotopy type theory. https://arxiv.org/abs/1706.07526v4
[14] Scoccola, L.: Nilpotent types and fracture squares in homotopy type theory. https://arxiv.org/abs/1903.03245
[15] Shulman, M.: All (\infty,1)-toposes have strict univalent universes. https://arxiv.org/abs/1904.07004
[16] Univalent Foundations Program, The: Homotopy type theory: Univalent foundations of mathematics. Institute for Advanced Study, Princeton, NJ
[17] Vergura, M.: L'-localization in an \infty-topos. https://arxiv.org/abs/1907.03837
[18] Vergura, M.: Localization theory in an \infty-topos. https://arxiv.org/abs/1907.03836
Search
Partner of
