ﻻ يوجد ملخص باللغة العربية
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 to 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.
The purpose of this foundational paper is to introduce various notions and constructions in order to develop the homotopy theory for differential graded operads over any ring. The main new idea is to consider the action of the symmetric groups as par
In previous work, we used an $infty$-categorical version of ultraproducts to show that, for a fixed height $n$, the symmetric monoidal $infty$-categories of $E_{n,p}$-local spectra are asymptotically algebraic in the prime $p$. In this paper, we prov
We define in the setting of homotopy type theory an H-space structure on $mathbb S^3$. Hence we obtain a description of the quaternionic Hopf fibration $mathbb S^3hookrightarrowmathbb S^7twoheadrightarrowmathbb S^4$, using only homotopy invariant tools.
Homotopy type theory is a version of Martin-Lof type theory taking advantage of its homotopical models. In particular, we can use and construct objects of homotopy theory and reason about them using higher inductive types. In this article, we constru
We set up foundations of representation theory over $S$, the sphere spectrum, which is the `initial ring of stable homotopy theory. In particular, we treat $S$-Lie algebras and their representations, characters, $gl_n(S)$-Verma modules and their dual