Blakers–Massey theorem

From testwiki
Revision as of 05:20, 13 May 2023 by imported>DanGrayson (Description of the result: fix some grammar)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigation Jump to search

Template:Short description In mathematics, the first Blakers–Massey theorem, named after Albert Blakers and William S. Massey,[1][2][3] gave vanishing conditions for certain triad homotopy groups of spaces.

Description of the result

This connectivity result may be expressed more precisely, as follows. Suppose X is a topological space which is the pushout of the diagram

A f C g B,

where f is an m-connected map and g is n-connected. Then the map of pairs

(A,C)(X,B)

induces an isomorphism in relative homotopy groups in degrees k(m+n1) and a surjection in the next degree.

However the third paper of Blakers and Massey in this area[4] determines the critical, i.e., first non-zero, triad homotopy group as a tensor product, under a number of assumptions, including some simple connectivity. This condition and some dimension conditions were relaxed in work of Ronald Brown and Jean-Louis Loday.[5] The algebraic result implies the connectivity result, since a tensor product is zero if one of the factors is zero. In the non simply connected case, one has to use the nonabelian tensor product of Brown and Loday.[5]

The triad connectivity result can be expressed in a number of other ways, for example, it says that the pushout square above behaves like a homotopy pullback up to dimension m+n.

Generalization to higher toposes

The generalization of the connectivity part of the theorem from traditional homotopy theory to any other infinity-topos with an infinity-site of definition was given by Charles Rezk in 2010.[6]

Fully formal proof

In 2013 a fairly short, fully formal proof using homotopy type theory as a mathematical foundation and an Agda variant as a proof assistant was announced by Peter LeFanu Lumsdaine;[7] this became Theorem 8.10.2 of Homotopy Type Theory – Univalent Foundations of Mathematics.[8] This induces an internal proof for any infinity-topos (i.e. without reference to a site of definition); in particular, it gives a new proof of the original result.

References

Template:Reflist