ترغب بنشر مسار تعليمي؟ اضغط هنا

The Cayley-Dickson Construction in Homotopy Type Theory

103   0   0.0 ( 0 )
 نشر من قبل Ulrik Buchholtz
 تاريخ النشر 2016
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English




اسأل ChatGPT حول البحث

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.



قيم البحث

اقرأ أيضاً

The Cayley-Dickson Construction is a generalization of the familiar construction of the complex numbers from pairs of real numbers. The complex numbers can be viewed as two-dimensional vectors equipped with a multiplication. The construction can be used to construct, not only the two-dimensional Complex Numbers, but also the four-dimensional Quaternions and the eight-dimensional Octonions. Each of these vector spaces has a vector multiplication, v_1*v_2, that satisfies: 1. Each nonzero vector has a multiplicative inverse. 2. For the Euclidean length of a vector |v|, |v_1 * v_2| = |v_1| |v2|. Real numbers can also be viewed as (one-dimensional) vectors with the above two properties. ACL2(r) is used to explore this question: Given a vector space, equipped with a multiplication, satisfying the Euclidean length condition 2, given above. Make pairs of vectors into new vectors with a multiplication. When do the newly constructed vectors also satisfy condition 2?
215 - Urs Schreiber 2014
We implement in the formal language of homotopy type theory a new set of axioms called cohesion. Then we indicate how the resulting cohesive homotopy type theory naturally serves as a formal foundation for central concepts in quantum gauge field theo ry. This is a brief survey of work by the authors developed in detail elsewhere.
Let $G$ be a discrete group. We prove that the category of $G$-posets admits a model structure that is Quillen equivalent to the standard model structure on $G$-spaces. As is already true nonequivariantly, the three classes of maps defining the model structure are not well understood calculationally. To illustrate, we exhibit some examples of cofibrant and fibrant posets and an example of a non-cofibrant finite poset.
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.
Univalent homotopy type theory (HoTT) may be seen as a language for the category of $infty$-groupoids. It is being developed as a new foundation for mathematics and as an internal language for (elementary) higher toposes. We develop the theory of fac torization systems, reflective subuniverses, and modalities in homotopy type theory, including their construction using a localization higher inductive type. This produces in particular the ($n$-connected, $n$-truncated) factorization system as well as internal presentations of subtoposes, through lex modalities. We also develop the semantics of these constructions.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا