From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vk1-xa37.google.com (mail-vk1-xa37.google.com [IPv6:2607:f8b0:4864:20::a37]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 70fc1f33 for ; Thu, 14 Nov 2019 18:36:32 +0000 (UTC) Received: by mail-vk1-xa37.google.com with SMTP id k127sf3001124vka.10 for ; Thu, 14 Nov 2019 10:36:31 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1573756590; cv=pass; d=google.com; s=arc-20160816; b=pUyCFq/PyF99vAVGSyB7KHxCCioVRJlOTGKXwy4ymyBPsXqOxYEU9RLoRIEsqZuu0/ dAhcJ3pkR8yphutzK+zhk1DzNG7KyyNKOJ/zdtGCqEVchgdpXescSgYP+aYgjBGj35CJ SdFcGh2e/60EiaCORYY98K2/fdUqEik8P3qjGSINgVZV7pDe3tDvImDw5LiHb17hqc0c Cvh0Qz+6rwOFg2DRMQE2HX9qzu1TVl/8woQLOMjq4pXZceiYxcMP/zymrMvvUsdIUZ+a 5vWWqWdDzDezL364KHpHEqen3UX7tVYIZAKFvfGNFuczkfRGOMC0KeZ8h78jtTrUN++B T/Qg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=n9SssBbWOpZqHnw8DqgiJPI9+J58vbE2LW2lDlCG7Jw=; b=FGif1pwwIn5bSG7eXvlUd8qRRjCD7LMWtLhMUG/xsBAT/A5feHoYNZ0JmvdYoD0ixO Mhdz0nQ19OiE0kWs/kYC0l+Y8VJrEB4xABl2aRtpEpx0wvdALm8pKhcrtWFqzTnuN48V 9ziEP7P/ZTCA3+vYdKDXj9ZxWUZUtzPC1l+JJpXR+ou5+9NI5iN+VTkitO0Fm21GFfTx Ps0T6m/AwTPTRiU+siOJdClxRkV+7mTTg4yByNvea59LbbqIq+rH3evfgWe9pg8vVffw GVkhTE4PQQF4xX6IxfuBCuUysQgrEjViZPMxMCZMEXzCbgZlXYhhSSGo0rPeAzUSDxPP 0CZA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=H2UHUXQ9; spf=pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::62a as permitted sender) smtp.mailfrom=alizter@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=n9SssBbWOpZqHnw8DqgiJPI9+J58vbE2LW2lDlCG7Jw=; b=QTlN7JYQjQ97tXZ2HoZlJfX4QfBbaYnGKQpH5EzwcKMx18Ql3ApwTeHXRypAfTo8ra TWzOvy8syFZps13M645dUK5ictdSDPqkX9adO1MxItWr3Oz0KXeIEdqlIk3ZrQbuzGWA JD35Qg8OodnV4Gep6ZAkZWjXaHyg4p9iK7vLO1gTspWlelx0s94EpwwPf9Z4FQRNymO5 RSUPHwhUyrMw9m5+OJx9O7smRAWCkMxq359re2Hao9Dlp1Ac1/VMIHq6HQvfLUbwLibm Q+1EJEzi85Tbv1bXwELFe4HCH0mmuvowxafZ+YkBJNtvJyBYI/qqI73fe0KTVpzJfulJ idbQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=n9SssBbWOpZqHnw8DqgiJPI9+J58vbE2LW2lDlCG7Jw=; b=qfWxXXYrpymeVT/MQQLdX9Y38okkScbhToHedpMo7iHWUPQ5GHWtEJU+LIgMBhY0H6 W9IjqzZIUKh+67P1DRXA9uhswHz0kiVN3+9a+A+Ut9TjUmsS2n6+2Vn4fW5rhbJxuEwJ jOOVaJvUqWQ20e07Uiq/k3yRZCZ+gOfwwK1xBkfj83fZEoOHYXBYEONIdKjvWBtLkElE AxY9+3DFHQxE/LjTPTFL5vcSypcRH3QKcr6UhQUtwuJFe8q9lksQR7IdgWz9d2Cc8RSo Lazx/u833MLKqsXOGIPy4at6kBCV0LdtzdvWifIbFI3dH9hxYvOjCrTzTJlEvrJIkg6y FIMQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=n9SssBbWOpZqHnw8DqgiJPI9+J58vbE2LW2lDlCG7Jw=; b=P1mpADHdfu3e+0lA8c14nrCdIp6wy8X1lDL3TrFOB7bEwM7eulbsWtyuQle17B+1yP dEFWEBPmLcidPU6kA5lM2iyb2O/2/DHGXHVgDSvsYCDPX88aKIiJJ7skQ9cEZ0esK7mf eGtThuuq1ajaeW+X6kFHxf8TH5rcdv9cAR7owH+IAwcCA3i/UjwSgGyG717CMNWd9RG5 evwP0lVE4XKUkVhMCPmmQA8Huf1GObICVKX5OIwerkHUVvU/jKXQslhZgisCtJn31si6 Bid+bQfPCktUqTSPUbghPfZpr7cPYPEcY8YzbWXDSmTlW45YvpBKGALw87rnJqeqitCV ZRQA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXqmLY+cKfXstyD3ZpoQIhbWI00qnmGrUKYtmLAoQVQ3FLQrSNj o9QmY3sslzz6S8wHOrT7hDc= X-Google-Smtp-Source: APXvYqx1HQh/0ytC2jZDgwJYynw6nNheeMvz9Qbrg13hcBiY8RqGwI9tOHLvm28TDrfgv8xAn7WKEw== X-Received: by 2002:a67:6ac7:: with SMTP id f190mr6681852vsc.55.1573756590174; Thu, 14 Nov 2019 10:36:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ab0:614b:: with SMTP id w11ls177803uan.11.gmail; Thu, 14 Nov 2019 10:36:29 -0800 (PST) X-Received: by 2002:a9f:3772:: with SMTP id a47mr6734670uae.53.1573756589773; Thu, 14 Nov 2019 10:36:29 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1573756589; cv=none; d=google.com; s=arc-20160816; b=jpUefPDu7nhTA9NgrZncHahshudWAgPyxps/WT0HjPE7/bSIKVyUfH9O7jU7BhAyW2 fgi6NCSRnE9TNXmVGRyvkiFwIZh4DTTEl0tPeiwA6/XG+/UIabbnivnhfRczS29atBiO twZND57I9kBvHvONw5kSIuDTBymEQ5+8s4Sr4N3qqgIv0W/0+FX9Zz1jw4U4vmfIkWY/ IoU6b2wTT8dc3vvkS5iugV2KGuPD1P7EVo+0Jsw/5yFH9AIJ/7SFdur09mek6wS3fEkC P6gFClT9VAvYlvfdGcfif9PLw/Ee6YF3I+azl4WzQy9MPqyF7jN0k9U8+RHD+9iBeE8T hNxw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=Dxht3VMjXAelJ9wMvPCHFjaEDWQkCAXWosglM51D1qs=; b=ir3rvs1oOVnpiZDQdS8MuCH+Q+6zuV4Q8TKtiSAfIHrTAW5EEisj+Ic7MJKO8fyLl+ NJd2RunxsbMviBCRNkk9p2Ri6fNQ4qc3ud/oCZAmHwhJiPrucinDQLVvESRXakQ/5zkX qn6O+9EFBUK9yiSf13qK5C1YD0Dd8dzIbSMt5TJb4Cq2Zpwh9h10g8MR8tXKQtThF0jy v1xK7O8yYbpsipGTlPMALr440BhONwN8mKR63wJVYOmIIP2fE2llbAe+nORPGxLBNMd5 lO8S9kuD0GviY0DOkeXhdIkEowBgEvbwprJpBNCKLFAjMf8bHZmFy8eRFoerMtek6iQ0 ll+A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=H2UHUXQ9; spf=pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::62a as permitted sender) smtp.mailfrom=alizter@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pl1-x62a.google.com (mail-pl1-x62a.google.com. [2607:f8b0:4864:20::62a]) by gmr-mx.google.com with ESMTPS id s197si357300vkd.5.2019.11.14.10.36.29 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 14 Nov 2019 10:36:29 -0800 (PST) Received-SPF: pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::62a as permitted sender) client-ip=2607:f8b0:4864:20::62a; Received: by mail-pl1-x62a.google.com with SMTP id o9so3012069plk.6 for ; Thu, 14 Nov 2019 10:36:29 -0800 (PST) X-Received: by 2002:a17:902:8c8a:: with SMTP id t10mr4008776plo.325.1573756588337; Thu, 14 Nov 2019 10:36:28 -0800 (PST) MIME-Version: 1.0 From: Ali Caglayan Date: Thu, 14 Nov 2019 18:36:19 +0000 Message-ID: Subject: [HoTT] Whitehead products in HoTT To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000693020059752c2a0" X-Original-Sender: alizter@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=H2UHUXQ9; spf=pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::62a as permitted sender) smtp.mailfrom=alizter@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --000000000000693020059752c2a0 Content-Type: text/plain; charset="UTF-8" Hello HoTT list! I have recently been thinking about Whitehead products and how we can talk about them in homotopy type theory. I have always thought that their construction was slightly convoluted, and I failed to see why they were interesting operations to think about. Recently, Jacob Lurie gave a really nice talk about Lie algebras and homotopy theory: https://www.youtube.com/watch?v=LeaiPHAh0X0 I will give a quick and dirty summary of the start of his talk. If you don't care to hear it you can scroll past it to the section heading. The Whitehead product is a binary operation on homotopy groups of spheres. Explicitly, for a pointed space X this is a group homomorphism: Pi_{n + 1} (X) x Pi_{m + 1} (X) --> Pi_{n + m + 1} (X) Now at first glance this seems to be an ugly operation. The indexing, for example, doesn't quite line up, so it doesn't quite become what some people would consider to be a graded map. This is simply because this is the wrong way to look at it. What the Whitehead product really is is the following: Pi_n (loops X) x Pi_m (loops X) --> Pi_{n+m} (loops X) This is much better. But still the question arises, why do we care about such a map? To understand the picture, we take a few step backs and look at Lie theory. You don't need to know anything about Lie theory to understand this story however. Classically given a group G, we are often interested in the behavior of the commutator map: G x G --> G (g, h) |-> g h g^-1 h^-1 This map gives us a measure of how commutative our group operation is. Now often we have some extra structure on a group G, which lets us understand our commutator map better. Suppose G was also a smooth manifold in a compatible way with our group operation. We call such a group, a Lie group. Notably our group operation is now a smooth map, which means we can differentiate it as many times as we wish. It isn't too difficult to also show that our commutator map is also smooth. So using the tools at our disposal we can differentiate our commutator map (at the identity of G). Doing so we get the following bilinear map: TG x TG -> TG Which we will call our Lie bracket [-,-]. This bracket satisfies some extra identities which aren't so important for now: - Skew-symmetry [x, y] + [y, x] = 0 - Jacobi identity [x, [y, z]] + [y, [z, x]] + [z, [x, y]] = 0 Together an Abelian group with its Lie bracket operation satisfying the above identities is called a Lie algebra. As a quick example, consider the group SU(2) of unitary 2x2 matrices with determinant 1, or equivalently pairs of complex numbers (alpha, beta) such that |alpha|^2 + |beta|^2 = 1, or equivalently the group of unit quarternions. Now take my word for it, and note that the tangent space of SU(2) at the identity is essentially the vector space R^3. So the commutator operation we defined on SU(2) becomes a bilinear map R^3 x R^3 -> R^3. What is this map exactly? Well its just the cross product on R^3! Now it turns out in Lie theory, that no information was lost when differentiating this commutator map. By this I mean every Lie group has an associated Lie algebra and every Lie algebra has an associated Lie group. This correspondence let's you study these two worlds with the help of each other. We can develop the following heuristic: commutator maps in group-like objects can shed light on the structure of said object. How does this relate to homotopy theory? Well in homotopy theory, we have something that kind of looks like a group. The loop space of a pointed space X. If you are familiar with homotopy theory or homotopy type theory you will know that we have a concatenation map: loops X x loops X -> loops X Which takes a loop p and a loop q, and sends it to the loop pq. In classical homotopy theory loops are points in X parameterized by the interval. Concatenation is constructed by going twice as fast round p, then twice as fast round q, leaving you a loop pq. In homotopy type theory we can define the concatenation by path induction (see Ch2 of the HoTT book). Now we can also take inverses p^ of a path p in classical homotopy theory and HoTT. In classical homotopy theory you just go backwards along your paramterization. In HoTT you can define the inverse by path induction. With both you can show that inverse and identity laws kind of hold but with a catch: They only hold up to homotopy. When you look at homotopy classes of such loops when taking the fundamental group, this is fine because it ends up being associative "on the nose". In HoTT we define the fundamental group as the set-truncation of the loop space, which lets us show that any two "associativity proofs" are in fact the same. Observe that we can create a "commutator" map for loop spaces also: loops X x loops X --> loops X ( p , q ) |-> p q p^ q^ However as mentioned before, loop spaces aren't really groups, but groups up to homotopy (or H-groups). However when looking at the fundamental group of X, we see that our "commutator" becomes the actual commutator on the fundamental group. Now just as we did in Lie theory, we can exploit this "extra structure" that we have to study our "commutator" map. We do this by looking at the higher homotopy groups of our space, and see how it interacts with the commutator map. This is the story that Jacob Lurie told in his talk, which I was following up until he wrote the following: Pi_a (loops X) x Pi_b (loops X) --> Pi_{a + b} (loops X) and said that this was the Whitehead product. Now I didn't quite follow this step, and since I was watching the talk online, I couldn't put my hand up and ask a question. Since this wasn't really relevent to the pointed Jacob was trying to make, he didn't talk so much about it. Instead I devised my own explanation: What we really want to do is construct the following map: [Y, loops X] x [Z, loops X] --> [Y /\ Z , loops X] you can see if we plug in Y := S^a, Z := S^b we get [S^a, loops X] x [S^b, loops X] --> [S^a /\ S^b, loops X] Now a property of the smash product is that we have S^a /\ S^b being equivalent to S^(a+b) (which I will come back to since this isn't so obvious). And since higher homotopy groups are just the set of pointed maps from the spheres to a space, we can see that in classical homotopy theory and HoTT that we have a map: Pi_a (loops X) x Pi_b (loops X) --> Pi_{a+b} (loops X) Or in order words, we have as a special case, the Whitehead product. So the question becomes, how do we create this "generalized Whitehead product"? What we will see is that it is a pretty natural thing to consider. In fact it is just the composition of two maps: [Y, loops X] x [Z, loops X] -> [Y /\ Z, loops X /\ loops X] -> [Y /\ Z, loops X] Here by [-,-] I really mean the space of pointed maps, not the set as before. And all our arrows are also pointed. Mapping spaces are pointed spaces by taking the 'constant map at the basepoint' as the basepoint. Now the first map is just the bifunctoriality of the smash product. i.e. given two pointed maps Y -> loops X and Z -> loops X, we have a third pointed map Y /\ Z -> loops X /\ loops X. Furthermore, this construction of the pointed map is pointed itself hence sits as the first map in the above diagram. Now we are left to construct: [Y /\ Z, loops X /\ loops X] -> [Y /\ Z, loops X] Note that the functor [Y /\ Z, - ] can give this map if we give it a map loops X /\ loops X -> loops X. Now how do we construct a map loops X /\ loops X -> loops X? Well classically, the smash product is just a quotient, so we would use a function on the representatives of the equivalence classes and show that coming from the same class lands you in the same element. In HoTT we basically do something similar, the difference being that the smash product is a HIT. There are at least two equivalent definitions of the smash product in HoTT but we will ignore both of them and instead use an recursion principle you should be able to derive, no matter which definition you choose. This principle says: If you want to construct a map A /\ B -> C, then give me a map P : A x B -> C, such that we have the following: - pleft : forall a, P a pt = 1 - pright : forall b, P pt b = 1 - pleft pt = 1 - prigh pt = 1 Here 1 is the identity path or trivial loop. pt is just the base point of A or B. We are asking that our map essentially be pointed in each argument, and furthermore the proofs that they are pointed to be trivial. Now coming back to Whitehead, we see that to give a map: loops X /\ loops X -> loops X We need to give a map loops X x loops X -> loops X. So we just give the commutator map! It is an easy exercise to see that the commutator map satisfies the conditions we need for our recursion principle! So finally you can set-truncate this entire thing to get the whitehead product between given homotopy groups. This isn't the first time the Whitehead product has been defined in HoTT. Notably in his thesis, Guillaume Brunerie defined and used the Whitehead product, together with the James construction, to show that Pi_4(S^3) has a non-trivial generator of order n. (And is in fact generated by the bracket!) Guillaume uses joins of spheres and the 3x3 lemma which I think is far too complicated to describe what is in fact a very simple operation. The 3x3 lemma is a very non-trivial thing to prove. I mentioned earlier that S^n /\ S^m ~= S^(n+m) which isn't so trivial to show, but I wouldn't like to leave anybody hanging so I will give a quick proof here: When I write '=' I mean equivalence (which is a terrible abuse of notation). Start with the following three lemmas: Lemma 1. S^0 /\ X = X Lemma 2. S^1 /\ X = Susp X Lemma 3. X /\ (Y /\ Z) = (X /\ Y) /\ Z We want to show S^n /\ S^m = S^n+m, start by induction on n. For the base case we need to show that S^0 /\ S^m, apply lemma 1. Now our induction hypothesis is that S^n /\ S^m = S^n+m, and we wish to show S^n+1 /\ S^m = S^n+m+1. Since we define the spheres to be an iterated suspension, observe that: S^n+1 = Susp S^n = S^1 /\ S^n by lemma 2. Now using lemma 3, observe that S^n+1 /\ S^m = (S^1 /\ S^n) /\ S^m = S^1 /\ (S^n /\ S^ m), hence by lemma 2 and our induction hypothesis S^n+1 /\ S^m = Susp (S^n+m) = S^n+m+1, and we are done. I didn't really get a feel for the Whitehead product until Jacob mentioned that it was a commutator map in his talk. I thought that this would be a simpler and more enlightening construction than the ones I have come across. Whitehead products are important in homotopy theory because in some appropriate sense, every homotopy operation comes from Whitehead products and another simple operation. And as Guillaume showed, they can be used to construct non-trivial elements of higher homotopy groups. Hopefully this has been an interesting read. Please feel free to reply and ask questions. Happy thinking! Ali Caglayan -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DiL5O4-aQ-7YsPHOzo3MbnGHNgxXuYMW7ZPcxCWtQGAqg%40mail.gmail.com. --000000000000693020059752c2a0 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hello HoTT lis= t!

I have recently been thinking about Whitehead products and how we= can talk about
them in homotopy type theory. I have always thought that= their construction was
slightly convoluted, and I failed to see why the= y were interesting operations to
think about.

Recently, Jacob Lur= ie gave a really nice talk about Lie algebras and homotopy
theory:
https://www.youtube.com/watch?v=3DLeaiPHAh0X0

I will give a q= uick and dirty summary of the start of his talk. If you don't care to
hear it you can scroll past it to the section heading.=

The Whitehead product= is a binary operation on homotopy groups of spheres.
Explicitly, for a = pointed space X this is a group homomorphism:

=C2=A0 =C2=A0 Pi_{n + = 1} (X) x Pi_{m + 1} (X) --> Pi_{n + m + 1} (X)

Now at first glanc= e this seems to be an ugly operation. The indexing, for
example, doesn&#= 39;t quite line up, so it doesn't quite become what some people
woul= d consider to be a graded map.

This is simply because this is the wr= ong way to look at it. What the Whitehead
product really is is the follo= wing:

=C2=A0 =C2=A0 Pi_n (loops X) x Pi_m (loops X) --> Pi_{n+m} = (loops X)

This is much better.
But still the question arises, why= do we care about such a map?

To understand the picture, we take a f= ew step backs and look at Lie theory.
You don't need to know anythin= g about Lie theory to understand this story
however.

Classically = given a group G, we are often interested in the behavior of the
commutat= or map:

=C2=A0 =C2=A0 G x G =C2=A0--> =C2=A0 G
=C2=A0 =C2=A0 (= g, h) |-> g h g^-1 h^-1

This map gives us a measure of how commut= ative our group operation is.

Now often we have some extra structure= on a group G, which lets us understand
our commutator map better.
Suppose G was also a smooth manifold in a compatible way with our groupoperation. We call such a group, a Lie group. Notably our group operation= is now
a smooth map, which means we can differentiate it as many times = as we wish. It
isn't too difficult to also show that our commutator = map is also smooth.

So using the tools at our disposal we can differ= entiate our commutator map
(at the identity of G). Doing so we get the f= ollowing bilinear map:

=C2=A0 =C2=A0 TG x TG -> TG

Which w= e will call our Lie bracket [-,-]. This bracket satisfies some extra
ide= ntities which aren't so important for now:

=C2=A0 =C2=A0 - Skew-= symmetry [x, y] + [y, x] =3D 0
=C2=A0 =C2=A0 - Jacobi identity [x, [y, z= ]] + [y, [z, x]] + [z, [x, y]] =3D 0

Together an Abelian group with= its Lie bracket operation satisfying the above
identities is called a L= ie algebra.

As a quick example, consider the group SU(2) of unitary = 2x2 matrices with
determinant 1, or equivalently pairs of complex number= s (alpha, beta) such that
|alpha|^2 + |beta|^2 =3D 1, or equivalently th= e group of unit quarternions.

Now take my word for it, and note that= the tangent space of SU(2) at the
identity is essentially the vector sp= ace R^3. So the commutator operation we
defined on SU(2) becomes a bilin= ear map R^3 x R^3 -> R^3.

What is this map exactly? Well its just= the cross product on R^3!

Now it turns out in Lie theory, that no i= nformation was lost when
differentiating this commutator map. By this I = mean every Lie group has an
associated Lie algebra and every Lie algebra= has an associated Lie group. This
correspondence let's you study th= ese two worlds with the help of each other.

We can develop the follo= wing heuristic: commutator maps in group-like objects
can shed light on = the structure of said object.


How does this rel= ate to homotopy theory?

Well in homotopy theory, we have some= thing that kind of looks like a group. The
loop space of a pointed space= X. If you are familiar with homotopy theory or
homotopy type theory you= will know that we have a concatenation map:

=C2=A0 =C2=A0 loops X x= loops X -> loops X

Which takes a loop p and a loop q, and sends = it to the loop pq. In classical
homotopy theory loops are points in X pa= rameterized by the interval.
Concatenation is constructed by going twice= as fast round p, then twice as fast
round q, leaving you a loop pq. In = homotopy type theory we can define the
concatenation by path induction (= see Ch2 of the HoTT book).

Now we can also take inverses p^ of a pat= h p in classical homotopy theory and
HoTT. In classical homotopy theory = you just go backwards along your
paramterization. In HoTT you can define= the inverse by path induction. With both
you can show that inverse and = identity laws kind of hold but with a catch:
=C2=A0 =C2=A0 =C2=A0 =C2=A0= =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0
=C2=A0 =C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 They = only hold up to homotopy.

When you look at homotopy classes of such = loops when taking the fundamental
group, this is fine because it ends up= being associative "on the nose". In HoTT
we define the fundam= ental group as the set-truncation of the loop space, which
lets us show = that any two "associativity proofs" are in fact the same.

= Observe that we can create a "commutator" map for loop spaces als= o:

=C2=A0 =C2=A0 loops X x loops X --> =C2=A0loops X
=C2=A0 = =C2=A0 =C2=A0 =C2=A0 ( p , q ) =C2=A0 =C2=A0 |-> =C2=A0p q p^ q^
=C2= =A0 =C2=A0
However as mentioned before, loop spaces aren't really g= roups, but groups up to
homotopy (or H-groups). However when looking at = the fundamental group of X, we
see that our "commutator" becom= es the actual commutator on the fundamental group.

Now just as we di= d in Lie theory, we can exploit this "extra structure" that wehave to study our "commutator" map. We do this by looking at the= higher homotopy
groups of our space, and see how it interacts with the = commutator map.

This is the story that Jacob Lurie told in his talk,= which I was following up
until he wrote the following:

=C2=A0 = =C2=A0 Pi_a (loops X) x Pi_b (loops X) --> Pi_{a + b} (loops X)

a= nd said that this was the Whitehead product. Now I didn't quite follow = this
step, and since I was watching the talk online, I couldn't put = my hand up and
ask a question. Since this wasn't really relevent to = the pointed Jacob was
trying to make, he didn't talk so much about i= t.

Instead I devised my own explanation:

What we really want = to do is construct the following map:

=C2=A0 =C2=A0 [Y, loops X] x [= Z, loops X] --> [Y /\ Z , loops X]

you can see if we plug in Y := =3D S^a, Z :=3D S^b we get

=C2=A0 =C2=A0 [S^a, loops X] x [S^b, loop= s X] --> [S^a /\ S^b, loops X]

Now a property of the smash produc= t is that we have S^a /\ S^b being equivalent
to S^(a+b) (which I will c= ome back to since this isn't so obvious). And since
higher homotopy = groups are just the set of pointed maps from the spheres to a
space, we = can see that in classical homotopy theory and HoTT that we have a map:
<= br>=C2=A0 =C2=A0 Pi_a (loops X) x Pi_b (loops X) --> Pi_{a+b} (loops X)<= br>
Or in order words, we have as a special case, the Whitehead product.= So the
question becomes, how do we create this "generalized Whiteh= ead product"?

What we will see is that it is a pretty natural t= hing to consider. In fact it is
just the composition of two maps:
[Y, loops X] x [Z, loops X] -> [Y /\ Z, loops X /\ loops X] -> [Y /\= Z, loops X]

Here by [-,-] I really mean the space of pointed maps, = not the set as before.
And all our arrows are also pointed. Mapping spac= es are pointed spaces by taking
the 'constant map at the basepoint&#= 39; as the basepoint.

Now the first map is just the bifunctoriality = of the smash product. i.e. given
two pointed maps Y -> loops X and Z = -> loops X, we have a third pointed map
Y /\ Z -> loops X /\ loops= X. Furthermore, this construction of the pointed map
is pointed itself = hence sits as the first map in the above diagram.

Now we are left to= construct:

=C2=A0 =C2=A0 =C2=A0[Y /\ Z, loops X /\ loops X] -> [= Y /\ Z, loops X]

Note that the functor [Y /\ Z, - ] can give this ma= p if we give it a map
=C2=A0 =C2=A0
=C2=A0 =C2=A0 =C2=A0 =C2=A0 loop= s X /\ loops X -> loops X.

Now how do we construct a map loops X = /\ loops X -> loops X? Well classically,
the smash product is just a = quotient, so we would use a function on the
representatives of the equiv= alence classes and show that coming from the same
class lands you in the= same element.

In HoTT we basically do something similar, the differ= ence being that the smash
product is a HIT. There are at least two equiv= alent definitions of the smash
product in HoTT but we will ignore both o= f them and instead use an recursion
principle you should be able to deri= ve, no matter which definition you choose.

This principle says:
<= br>If you want to construct a map A /\ B -> C, then give me a map P : A = x B -> C,
such that we have the following:
=C2=A0 =C2=A0 - pleft := forall a, P a pt =3D 1
=C2=A0 =C2=A0 - pright : forall b, P pt b =3D 1<= br>=C2=A0 =C2=A0 - pleft pt =3D 1
=C2=A0 =C2=A0 - prigh pt =3D 1

= Here 1 is the identity path or trivial loop. pt is just the base point of A= or
B. We are asking that our map essentially be pointed in each argumen= t, and
furthermore the proofs that they are pointed to be trivial.
Now coming back to Whitehead, we see that to give a map:

=C2=A0 = =C2=A0 loops X /\ loops X -> loops X

We need to give a map
=C2=A0 =C2=A0 loops X x loops X -> loops X.

So we just give the = commutator map!

It is an easy exercise to see that the commutator ma= p satisfies the conditions
we need for our recursion principle!

S= o finally you can set-truncate this entire thing to get the whitehead produ= ct
between given homotopy groups.

This isn't the first time t= he Whitehead product has been defined in HoTT.
Notably in his thesis, Gu= illaume Brunerie defined and used the Whitehead
product, together with t= he James construction, to show that Pi_4(S^3) has a
non-trivial generato= r of order n. (And is in fact generated by the bracket!)

Guillaume u= ses joins of spheres and the 3x3 lemma which I think is far too
complica= ted to describe what is in fact a very simple operation. The 3x3 lemma
i= s a very non-trivial thing to prove.

I mentioned earlier that S^n /\= S^m ~=3D S^(n+m) which isn't so trivial to show,
but I wouldn't= like to leave anybody hanging so I will give a quick proof here:

Wh= en I write '=3D' I mean equivalence (which is a terrible abuse of n= otation).

Start with the following three lemmas:

Lemma 1. S^0= /\ X =3D X
Lemma 2. S^1 /\ X =3D Susp X
Lemma 3. X /\ (Y /\ Z) =3D (= X /\ Y) /\ Z

We want to show S^n /\ S^m =3D S^n+m, start by inductio= n on n. For the base case
we need to show that S^0 /\ S^m, apply lemma 1= . Now our induction hypothesis is
that S^n /\ S^m =3D S^n+m, and we wish= to show S^n+1 /\ S^m =3D S^n+m+1. Since we
define the spheres to be an = iterated suspension, observe that:
S^n+1 =3D Susp S^n =3D S^1 /\ S^n by = lemma 2. Now using lemma 3, observe that
S^n+1 /\ S^m =C2=A0=3D (S^1 /\ = S^n) /\ S^m =3D S^1 /\ (S^n /\ S^ m), hence by lemma 2
and our induction= hypothesis S^n+1 /\ S^m =3D Susp (S^n+m) =3D S^n+m+1, and we are
done.<= br>
I didn't really get a feel for the Whitehead product until Jacob= mentioned that
it was a commutator map in his talk. I thought that this= would be a simpler and
more enlightening construction than the ones I h= ave come across.

Whitehead products are important in homotopy theory= because in some appropriate
sense, every homotopy operation comes from = Whitehead products and another
simple operation. And as Guillaume showed= , they can be used to construct
non-trivial elements of higher homotopy = groups.

Hopefully this has been an interesting read. Please feel fre= e to reply and ask
questions.

Happy thinking!

Ali Caglaya= n

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DiL5O4-aQ-7YsPHOzo3MbnG= HNgxXuYMW7ZPcxCWtQGAqg%40mail.gmail.com.
--000000000000693020059752c2a0--