8.3 of an n-connected space and
Let be a pointed type and . Recall from \autorefthm:homotopy-groups that if the set has a group structure, and if the group is abelian.
We can now say something about homotopy groups of -truncated and -connected types.
Lemma 8.3.1.
If is -truncated and , then for all .
Proof.
The loop space of an -type is an -type, hence is an -type, and we have so is a mere proposition. But is inhabited, so it is actually contractible and . ∎
Lemma 8.3.2.
If is -connected and , then for all .
Proof.
We have the following sequence of equalities:
The third equality uses the fact that in order to use that and the fourth equality uses the fact that is -connected. ∎
Corollary 8.3.3.
for .
Proof.
The sphere is -connected by \autorefcor:sn-connected, so we can apply \autoreflem:pik-nconnected. ∎
Title | 8.3 of an n-connected space and |
---|---|
\metatable |