Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / Atom feed
* [HoTT] Whitehead products in HoTT
@ 2019-11-14 18:36 Ali Caglayan
  0 siblings, 0 replies; only message in thread
From: Ali Caglayan @ 2019-11-14 18:36 UTC (permalink / raw)
  To: Homotopy Type Theory

[-- Attachment #1: Type: text/plain, Size: 11416 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 13064 bytes --]

<div dir="ltr"><div class="gmail_quote"><div dir="ltr">Hello HoTT list!<br><br>I have recently been thinking about Whitehead products and how we can talk about<br>them in homotopy type theory. I have always thought that their construction was<br>slightly convoluted, and I failed to see why they were interesting operations to<br>think about.<br><br>Recently, Jacob Lurie gave a really nice talk about Lie algebras and homotopy<br>theory:<br><br><a href="https://www.youtube.com/watch?v=LeaiPHAh0X0" target="_blank">https://www.youtube.com/watch?v=LeaiPHAh0X0</a><br><br>I will give a quick and dirty summary of the start of his talk. If you don&#39;t care to</div><div dir="ltr">hear it you can scroll past it to the section heading.<br></div><div dir="ltr"><br></div><div dir="ltr">The Whitehead product is a binary operation on homotopy groups of spheres.<br>Explicitly, for a pointed space X this is a group homomorphism:<br><br>    Pi_{n + 1} (X) x Pi_{m + 1} (X) --&gt; Pi_{n + m + 1} (X)<br><br>Now at first glance this seems to be an ugly operation. The indexing, for<br>example, doesn&#39;t quite line up, so it doesn&#39;t quite become what some people<br>would consider to be a graded map.<br><br>This is simply because this is the wrong way to look at it. What the Whitehead<br>product really is is the following:<br><br>    Pi_n (loops X) x Pi_m (loops X) --&gt; Pi_{n+m} (loops X)<br><br>This is much better.<br>But still the question arises, why do we care about such a map?<br><br>To understand the picture, we take a few step backs and look at Lie theory.<br>You don&#39;t need to know anything about Lie theory to understand this story<br>however.<br><br>Classically given a group G, we are often interested in the behavior of the<br>commutator map:<br><br>    G x G  --&gt;   G<br>    (g, h) |-&gt; g h g^-1 h^-1<br><br>This map gives us a measure of how commutative our group operation is.<br><br>Now often we have some extra structure on a group G, which lets us understand<br>our commutator map better.<br><br>Suppose G was also a smooth manifold in a compatible way with our group<br>operation. We call such a group, a Lie group. Notably our group operation is now<br>a smooth map, which means we can differentiate it as many times as we wish. It<br>isn&#39;t too difficult to also show that our commutator map is also smooth.<br><br>So using the tools at our disposal we can differentiate our commutator map<br>(at the identity of G). Doing so we get the following bilinear map:<br><br>    TG x TG -&gt; TG<br><br>Which we will call our Lie bracket [-,-]. This bracket satisfies some extra<br>identities which aren&#39;t so important for now:<br><br>    - Skew-symmetry [x, y] + [y, x] = 0<br>    - Jacobi identity [x, [y, z]] + [y, [z, x]] + [z, [x, y]] = 0 <br><br>Together an Abelian group with its Lie bracket operation satisfying the above<br>identities is called a Lie algebra.<br><br>As a quick example, consider the group SU(2) of unitary 2x2 matrices with<br>determinant 1, or equivalently pairs of complex numbers (alpha, beta) such that<br>|alpha|^2 + |beta|^2 = 1, or equivalently the group of unit quarternions.<br><br>Now take my word for it, and note that the tangent space of SU(2) at the<br>identity is essentially the vector space R^3. So the commutator operation we<br>defined on SU(2) becomes a bilinear map R^3 x R^3 -&gt; R^3.<br><br>What is this map exactly? Well its just the cross product on R^3!<br><br>Now it turns out in Lie theory, that no information was lost when<br>differentiating this commutator map. By this I mean every Lie group has an<br>associated Lie algebra and every Lie algebra has an associated Lie group. This<br>correspondence let&#39;s you study these two worlds with the help of each other.<br><br>We can develop the following heuristic: commutator maps in group-like objects<br>can shed light on the structure of said object.<br><br><br><font size="4">How does this relate to homotopy theory?</font><br><br>Well in homotopy theory, we have something that kind of looks like a group. The<br>loop space of a pointed space X. If you are familiar with homotopy theory or<br>homotopy type theory you will know that we have a concatenation map:<br><br>    loops X x loops X -&gt; loops X<br><br>Which takes a loop p and a loop q, and sends it to the loop pq. In classical<br>homotopy theory loops are points in X parameterized by the interval.<br>Concatenation is constructed by going twice as fast round p, then twice as fast<br>round q, leaving you a loop pq. In homotopy type theory we can define the<br>concatenation by path induction (see Ch2 of the HoTT book).<br><br>Now we can also take inverses p^ of a path p in classical homotopy theory and<br>HoTT. In classical homotopy theory you just go backwards along your<br>paramterization. In HoTT you can define the inverse by path induction. With both<br>you can show that inverse and identity laws kind of hold but with a catch:<br>                        <br>                        They only hold up to homotopy.<br><br>When you look at homotopy classes of such loops when taking the fundamental<br>group, this is fine because it ends up being associative &quot;on the nose&quot;. In HoTT<br>we define the fundamental group as the set-truncation of the loop space, which<br>lets us show that any two &quot;associativity proofs&quot; are in fact the same.<br><br>Observe that we can create a &quot;commutator&quot; map for loop spaces also:<br><br>    loops X x loops X --&gt;  loops X<br>        ( p , q )     |-&gt;  p q p^ q^<br>    <br>However as mentioned before, loop spaces aren&#39;t really groups, but groups up to<br>homotopy (or H-groups). However when looking at the fundamental group of X, we<br>see that our &quot;commutator&quot; becomes the actual commutator on the fundamental group.<br><br>Now just as we did in Lie theory, we can exploit this &quot;extra structure&quot; that we<br>have to study our &quot;commutator&quot; map. We do this by looking at the higher homotopy<br>groups of our space, and see how it interacts with the commutator map.<br><br>This is the story that Jacob Lurie told in his talk, which I was following up<br>until he wrote the following:<br><br>    Pi_a (loops X) x Pi_b (loops X) --&gt; Pi_{a + b} (loops X)<br><br>and said that this was the Whitehead product. Now I didn&#39;t quite follow this<br>step, and since I was watching the talk online, I couldn&#39;t put my hand up and<br>ask a question. Since this wasn&#39;t really relevent to the pointed Jacob was<br>trying to make, he didn&#39;t talk so much about it.<br><br>Instead I devised my own explanation:<br><br>What we really want to do is construct the following map:<br><br>    [Y, loops X] x [Z, loops X] --&gt; [Y /\ Z , loops X]<br><br>you can see if we plug in Y := S^a, Z := S^b we get<br><br>    [S^a, loops X] x [S^b, loops X] --&gt; [S^a /\ S^b, loops X]<br><br>Now a property of the smash product is that we have S^a /\ S^b being equivalent<br>to S^(a+b) (which I will come back to since this isn&#39;t so obvious). And since<br>higher homotopy groups are just the set of pointed maps from the spheres to a<br>space, we can see that in classical homotopy theory and HoTT that we have a map:<br><br>    Pi_a (loops X) x Pi_b (loops X) --&gt; Pi_{a+b} (loops X)<br><br>Or in order words, we have as a special case, the Whitehead product. So the<br>question becomes, how do we create this &quot;generalized Whitehead product&quot;?<br><br>What we will see is that it is a pretty natural thing to consider. In fact it is<br>just the composition of two maps:<br><br>[Y, loops X] x [Z, loops X] -&gt; [Y /\ Z, loops X /\ loops X] -&gt; [Y /\ Z, loops X]<br><br>Here by [-,-] I really mean the space of pointed maps, not the set as before.<br>And all our arrows are also pointed. Mapping spaces are pointed spaces by taking<br>the &#39;constant map at the basepoint&#39; as the basepoint.<br><br>Now the first map is just the bifunctoriality of the smash product. i.e. given<br>two pointed maps Y -&gt; loops X and Z -&gt; loops X, we have a third pointed map<br>Y /\ Z -&gt; loops X /\ loops X. Furthermore, this construction of the pointed map<br>is pointed itself hence sits as the first map in the above diagram.<br><br>Now we are left to construct:<br><br>     [Y /\ Z, loops X /\ loops X] -&gt; [Y /\ Z, loops X]<br><br>Note that the functor [Y /\ Z, - ] can give this map if we give it a map<br>    <br>        loops X /\ loops X -&gt; loops X.<br><br>Now how do we construct a map loops X /\ loops X -&gt; loops X? Well classically,<br>the smash product is just a quotient, so we would use a function on the<br>representatives of the equivalence classes and show that coming from the same<br>class lands you in the same element.<br><br>In HoTT we basically do something similar, the difference being that the smash<br>product is a HIT. There are at least two equivalent definitions of the smash<br>product in HoTT but we will ignore both of them and instead use an recursion<br>principle you should be able to derive, no matter which definition you choose.<br><br>This principle says:<br><br>If you want to construct a map A /\ B -&gt; C, then give me a map P : A x B -&gt; C,<br>such that we have the following:<br>    - pleft : forall a, P a pt = 1<br>    - pright : forall b, P pt b = 1<br>    - pleft pt = 1<br>    - prigh pt = 1<br><br>Here 1 is the identity path or trivial loop. pt is just the base point of A or<br>B. We are asking that our map essentially be pointed in each argument, and<br>furthermore the proofs that they are pointed to be trivial.<br><br>Now coming back to Whitehead, we see that to give a map:<br><br>    loops X /\ loops X -&gt; loops X<br><br>We need to give a map<br><br>    loops X x loops X -&gt; loops X.<br><br>So we just give the commutator map!<br><br>It is an easy exercise to see that the commutator map satisfies the conditions<br>we need for our recursion principle!<br><br>So finally you can set-truncate this entire thing to get the whitehead product<br>between given homotopy groups.<br><br>This isn&#39;t the first time the Whitehead product has been defined in HoTT.<br>Notably in his thesis, Guillaume Brunerie defined and used the Whitehead<br>product, together with the James construction, to show that Pi_4(S^3) has a<br>non-trivial generator of order n. (And is in fact generated by the bracket!)<br><br>Guillaume uses joins of spheres and the 3x3 lemma which I think is far too<br>complicated to describe what is in fact a very simple operation. The 3x3 lemma<br>is a very non-trivial thing to prove.<br><br>I mentioned earlier that S^n /\ S^m ~= S^(n+m) which isn&#39;t so trivial to show,<br>but I wouldn&#39;t like to leave anybody hanging so I will give a quick proof here:<br><br>When I write &#39;=&#39; I mean equivalence (which is a terrible abuse of notation).<br><br>Start with the following three lemmas:<br><br>Lemma 1. S^0 /\ X = X<br>Lemma 2. S^1 /\ X = Susp X<br>Lemma 3. X /\ (Y /\ Z) = (X /\ Y) /\ Z<br><br>We want to show S^n /\ S^m = S^n+m, start by induction on n. For the base case<br>we need to show that S^0 /\ S^m, apply lemma 1. Now our induction hypothesis is<br>that S^n /\ S^m = S^n+m, and we wish to show S^n+1 /\ S^m = S^n+m+1. Since we<br>define the spheres to be an iterated suspension, observe that:<br>S^n+1 = Susp S^n = S^1 /\ S^n by lemma 2. Now using lemma 3, observe that<br>S^n+1 /\ S^m  = (S^1 /\ S^n) /\ S^m = S^1 /\ (S^n /\ S^ m), hence by lemma 2<br>and our induction hypothesis S^n+1 /\ S^m = Susp (S^n+m) = S^n+m+1, and we are<br>done.<br><br>I didn&#39;t really get a feel for the Whitehead product until Jacob mentioned that<br>it was a commutator map in his talk. I thought that this would be a simpler and<br>more enlightening construction than the ones I have come across.<br><br>Whitehead products are important in homotopy theory because in some appropriate<br>sense, every homotopy operation comes from Whitehead products and another<br>simple operation. And as Guillaume showed, they can be used to construct<br>non-trivial elements of higher homotopy groups.<br><br>Hopefully this has been an interesting read. Please feel free to reply and ask<br>questions. <br><br>Happy thinking!<br><br>Ali Caglayan<br></div>
</div></div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &quot;Homotopy Type Theory&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an email to <a href="mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com">HomotopyTypeTheory+unsubscribe@googlegroups.com</a>.<br />
To view this discussion on the web visit <a href="https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DiL5O4-aQ-7YsPHOzo3MbnGHNgxXuYMW7ZPcxCWtQGAqg%40mail.gmail.com?utm_medium=email&utm_source=footer">https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DiL5O4-aQ-7YsPHOzo3MbnGHNgxXuYMW7ZPcxCWtQGAqg%40mail.gmail.com</a>.<br />

^ permalink raw reply	[flat|nested] only message in thread

only message in thread, back to index

Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-11-14 18:36 [HoTT] Whitehead products in HoTT Ali Caglayan

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Example config snippet for mirrors

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git