Eckmann-Hilton and the Hopf Fibration in Homotopy Type Theory

Baker, Raymond

Undergraduate Honors Thesis

Eckmann-Hilton and the Hopf Fibration in Homotopy Type Theory Public Deposited

Analytics

Download PDF

Citations

Citeable URL: https://scholar.colorado.edu/concern/undergraduate_honors_theses/m613mz98t

Abstract

This thesis explores the connection between the Hopf fibration and the Eckmann-Hilton argument through the lens of Homotopy Type Theory (HoTT). Both the Hopf fibration and the Eckmann-Hilton argument are familiar constructions from classical homotopy theory. The Hopf fibration is a non-trivial map S3 → S2 whose fiber is S1 . The fiber sequence (and induced long exact sequence of homotopy groups) of the Hopf fibration gives an equivalence Ωn (S2 ) ≅ Ωn (S3 ), for n ≥ 3. This result implies, in particular, that π3 (S2 ) ≅ Z. This is a surprising result. Given that S2 is generated by a single two dimensional loop, why should S2 have any non-trivial loops at dimension three, much less have the same loop space as S3 from there on out?

The Eckmann-Hilton argument provides an answer to this question. The Eckmann-Hilton argument can be phrased in different ways. A simple way to phrase it is simply that a monoid object in the category of monoids is necessarily a commutative monoid. However, a more apt phrasing is the following: for any space X the concatenation of loops in Ω2 (X) is commutative (up to homotopy of paths). Thus Eckmann-Hilton tells us that the concatenation of loops in Ω2 (S2 ) is commutative. But this commutativity only holds up to homotopy. The homotopy itself is a three dimensional pathand this three dimensional path lends a generator of Ω3 (S3 ).The goal of this thesis is to write out an elementary proof of the above claim in the language of HoTT. The thesis is broken up into two parts. Part I serves as a limited introduction to the basics of HoTT. Part II of the thesis culminates in Part III which contains the desired proof.

Creator