A homotopy -type is a view of a space where we consider its properties only up to the nd homotopy group . To make this precise, we look at maps that ‘see’ invariants in dimensions 0,1, and 2. These are the 2-equivalences:
A continuous map is a homotopy -equivalence if it induces isomorphisms on for at each basepoint. Two spaces share the same homotopy -type if they are linked by a zig-zag chain of homotopy -equivalences.
For any ‘nice’ space , you can kill its homotopy groups in higher dimensions by attaching cells, thus constructing a new space so that the inclusion of into is a homotopy -equivalence; up to (weak) homotopy equivalence, the result is the same for any space with the same homotopy -type. Accordingly, a homotopy -type may alternatively be defined as a space with trivial for , or as the unique (weak) homotopy type of such a space, or as its fundamental -groupoid (which will be a -groupoid).
See the general discussion in homotopy n-type.
Homotopy -types can be classified by various different types of algebraic data.
\delta: C_2 \to C_1
of groupoids with object set such that is totally disconnected, i.e. is a family of groups . Further the groupoid operates on this family of groups so that (using right operations) if in and then ; and the usual rules for an operation are satisfied, namely , , when these are defined. Further the two basic crossed module rules hold:
for all when the rules make sense.
Such a crossed module may be extended to a crossed complex by adding trivial elements in dimensions higher than 2. Hence there is a simplicial nerve which in dimension is
Crs(\Pi (\Delta^n_*), sk^2 C).
The geometric realisation of this is the classifying space . Its first and second homotopy groups at are the cokernel and kernel of . It components are those of the groupoid . All other homotopy groups are trivial.
If is a CW-complex then there is a bijection of homotopy classes
[X,BC] \cong [\Pi X_*, sk^2 C],
and hence there is a map inducing isomorphisms of homotopy groups in dimensions 1 and 2.
Here the cotruncation of a general crossed complex agree with up to dimension , is in dimension , and is trivial in higher dimensions.
It is in this sense that crossed modules of groupoids classify weak homotopy -types.
Crs^2(C \otimes D, E) \cong Crs^2(C, CRS^2(D,E))
and with a unit interval object so that (left) homotopies are determined as morphisms or as elements of .
As a crossed module give rise to an internal groupoid in the category of groups (or groupoids), we can take the nerve of that structure and get a simplicial group (or simplicially enriched groupoid). From a simplicial group(oid), , one can define a simplicial set called the classifying space of the simplicial group, , for which construction see simplicial group. We thus can start with a crossed module form a simplicial group and then take of that to get another model of .
|homotopy level||n-truncation||homotopy theory||higher category theory||higher topos theory||homotopy type theory|
|h-level 0||(-2)-truncated||contractible space||(-2)-groupoid||true/unit type/contractible type|
|h-level 1||(-1)-truncated||(-1)-groupoid/truth value||h-proposition|
|h-level 2||0-truncated||discrete space||0-groupoid/set||sheaf||h-set|
|h-level 3||1-truncated||homotopy 1-type||1-groupoid/groupoid||(2,1)-sheaf/stack||h-groupoid|
|h-level 4||2-truncated||homotopy 2-type||2-groupoid||h-2-groupoid|
|h-level 5||3-truncated||homotopy 3-type||3-groupoid||h-3-groupoid|