Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Ali Caglayan <alizter@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] Whitehead products in HoTT
Date: Thu, 14 Nov 2019 18:36:19 +0000	[thread overview]
Message-ID: <CAB17i=iL5O4-aQ-7YsPHOzo3MbnGHNgxXuYMW7ZPcxCWtQGAqg@mail.gmail.com> (raw)

[-- 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 --]

                 reply	other threads:[~2019-11-14 18:36 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CAB17i=iL5O4-aQ-7YsPHOzo3MbnGHNgxXuYMW7ZPcxCWtQGAqg@mail.gmail.com' \
    --to=alizter@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).