nLab
Whitehead theorem

Context

Homotopy theory

(∞,1)-Topos theory

(∞,1)-topos theory

Background

Definitions

Characterization

Morphisms

Extra stuff, structure and property

Models

Constructions

structures in a cohesive (∞,1)-topos

Foundations

Contents

Classical case

The classical Whitehead theorem asserts that

Theorem (Whitehead)

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 general (,1)(\infty,1)-toposes

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 (,1)(\infty,1)-topos Top is presented by the model structure on simplicial presheaves on the point, namely the model structure on simplicial sets.

In homotopy type theory

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 nn; this is provable in homotopy type theory by induction on nn.

References

The (,1)(\infty,1)-topos version is in section 6.5 of

A formalization in homotopy type theory written in Agda is in

Revised on July 24, 2014 22:21:13 by Urs Schreiber (89.204.139.218)