homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
(2,1)-quasitopos?
structures in a cohesive (∞,1)-topos
basic constructions:
strong axioms
further
The classical Whitehead theorem asserts that
Every weak homotopy equivalence between CW-complexes is a homotopy equivalence.
(See also the discussion at m-cofibrant space).
Using the homotopy hypothesis-theorem this may be reformulated:
In the (∞,1)-category ∞Grpd every weak homotopy equivalence is a homotopy equivalence.
A simplicial map $f\colon X\to Y$ between Kan complexes is a simplicial homotopy equivalence if and only if for any $a$ and $b$ that make the following square commute
there is a diagonal arrow $d$ that makes the upper triangle commutative and the lower triangle commutative up to a homotopy $h\colon \Delta^1\times\Delta^n\to Y$ that is constant on the boundary $\Delta^1\times\partial\Delta^n$.
Of course, this statement can be reformulated using homotopy groups like the version for topological spaces, but the above statement is more practical.
In the above criterion, the boundary inclusion
can be replaced by any weakly equivalent cofibration.
If $X$ or $Y$ is not a Kan complex, one can formulate a similar criterion using barycentric subdivisions of $\partial\Delta^n$ and $\Delta^n$. A simplicial map $f\colon X\to Y$ between simplicial sets is a weak homotopy equivalence if and only if for any $k\ge0$ and for any $a$ and $b$ that make the following square commute
there is $l\ge k$ such that in the outer rectangle in the diagram
we can find a diagonal arrow
that makes the upper triangle in the diagram
commutative and the lower triangle commutative up to a homotopy
that is constant on the boundary $Sd^l(\Delta^1\times\partial\Delta^n)$.
In $G$-equivariant homotopy theory the statement is that $G$-homotopy equivalences between G-CW complexes are equivalent to maps that are weak homotopy equivalences on fixed point spaces $H^H$ for all closed subgroups $H \subset G$ (e.g. Greenlees-May 95, theorem 2.4). See at equivariant Whitehead theorem.
There is a notion of homotopy groups for objects in every ∞-stack (∞,1)-topos, as described at homotopy group (of an ∞-stack). Accordingly, there is a notion of weak homotopy equivalence in every ∞-stack (∞,1)-topos and hence an analog of the statement of Whiteheads theorem. One finds that
Warning Whitehead’s theorem fails for general (∞,1)-toposes and non-truncated objects.
The ∞-stack (∞,1)-toposes in which the Whitehead theorem does hold are the hypercomplete (∞,1)-toposes. These are precisely the ones that are presented by a local model structure on simplicial presheaves.
For instance the hypercomplete $(\infty,1)$-topos Top is presented by the model structure on simplicial presheaves on the point, namely the model structure on simplicial sets.
Since homotopy type theory admits models in (∞,1)-toposes (and in particular in non-hypercomplete ones), Whitehead’s theorem is not provable when regarded as a statement about types in homotopy type theory. From this perspective, the truth of Whitehead’s theorem is a foundational axiom that may be regarded as a “classicality” property, akin to excluded middle or the axiom of choice — we call it Whitehead’s principle (not to be confused with Whitehead's problem?, another statement that is independent of the usual axioms of set theory).
Whitehead’s principle does hold, however, for maps between homotopy n-types for any finite $n$; this is provable in homotopy type theory by induction on $n$.
Originally proved by J. H. C. Whitehead:
J. H. C. Whitehead, Combinatorial homotopy. I, Bulletin of the American Mathematical Society 55:3 (1949), 213–246. doi.
Anthony Elmendorf, Igor Kriz, Peter May, section 1 of Modern foundations for stable homotopy theory, in Ioan Mackenzie James (ed.), Handbook of Algebraic Topology, 1995 Amsterdam: North-Holland, pp. 213–253, (pdf)
Discussion for equivariant homotopy theory includes
The $(\infty,1)$-topos version is in section 6.5 of
A formalization in homotopy type theory written in Agda is in