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

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:

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 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 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 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:

=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

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.

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 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:

=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.

=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--