Library HoTT.Homotopy.HomotopyGroup

The type that the nth homotopy group will have.

We construct the wildcat structure on HomotopyGroup_type in the obvious way.

We first define Pi 1 X, and use this to define Pi n X. The reason is to make it easier for Coq to see that Pi (n.+1) X is definitionally equal to Pi 1 (iterated_loops n X)

Operation

Unit

Inverse

IsHSet

Associativity

Left identity

Right identity

Left inverse

Right inverse

Definition of the nth homotopy group

See pi_loops below for an alternate unfolding.

When n >= 2 we have that the nth homotopy group is an abelian group. Note that we don't actually define it as an abelian group but merely show that it is one. This would cause lots of complications with the typechecker.

For the same reason as above, we make Pi1 a functor before making Pi a functor.

Note: we don't have to be careful about which paths we choose here since we are trying to inhabit a proposition.

The conditions for Pi1 to be a 1-functor only involve equalities of maps between groups, which reduce to equalities of maps between types. Type inference shows that Tr 0 o loops is a 1-functor, and so it follows that Pi1 is a 1-functor.

Sometimes it is convenient to regard Pi n as landing in pointed types. On objects, this is handled by the coercion HomotopyGroup_type_ptype, but on morphisms it doesn't seem possible to define a coercion. So we explicitly name the composite functor.

pPi is equal to a more explicit map. These are definitional for n = 0 and n a successor; it would be nice to make them definitional for generic n.

Here is the associated object-wise equivalence, which is the identity map for 0 and successors.

These equivalences are natural. Put another way, we can compute fmap Pi in terms of the composite functor, up to the equivalences above. For n = 0 or n a successor, we can omit the equivalences; for n = 0, the induced maps are definitionally equal as pointed maps; for n a successfor the underlying unpointed maps are definitionally equal, but the pointedness proofs are not, and this is handled by phomotopy_homotopy_hset.

Pi n.+1 sends equivalences to group isomorphisms.

The homotopy groups of a loop space are those of the space shifted.

Except in the lowest case, this can be expressed as an isomorphism of groups.

Naturality of pi_loops.

Homotopy groups preserve products. This is a direct proof, but below we give a second proof whose underlying map is the natural one.

The pointed map from left-to-right below, coming from functoriality, is an equivalence.

For positive n, this equivalence is an isomorphism of groups.

Homotopy groups of truncations An n-connected map induces an equivalence on the nth homotopy group. We first state this for pTr 0 o iterated_loops n, since the proof works for general n, and then we deduce the result for pPi n afterwards.

The same holds for pPi n.

For positive n, it is a group isomorphism.

As a consequence, the truncation map ptr : X → pTr n X induces an equivalence on Pi n. We don't make this an instance, since it is found by typeclass search.

For positive n, it is a group isomorphism.

An n-connected map induces a surjection on n+1-fold loop spaces and Pi (n+1).

Pointed sections induce embeddings on homotopy groups.