Homotopy groups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2025-02-27.
Last modified on 2025-02-27.

module synthetic-homotopy-theory.homotopy-groups where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.connected-components
open import foundation.dependent-pair-types
open import foundation.set-truncations
open import foundation.sets
open import foundation.truncation-levels
open import foundation.truncations
open import foundation.universe-levels

open import group-theory.concrete-groups
open import group-theory.homotopy-automorphism-groups

open import structured-types.pointed-types

open import synthetic-homotopy-theory.iterated-loop-spaces

Idea

The (abstract) homotopy groups of a pointed type A are a sequence i ↦ πᵢ A of sets where

  • π₀ A is the set of connected components of A, and
  • πᵢ₊₁ A is the set πᵢ ΩA equipped with the group structure obtained from the [loop space](synthetic-homotopy theory.loop-spaces.md).

For i ≥ 2, the i-th homotopy group πᵢ A of A is abelian by the Eckmann-Hilton argument.

Alternatively, we can define the concrete homotopy groups of a pointed type A to be the sequence ℕ → Concrete-Group, given by

  i ↦ concrete-group-Pointed-Type (iterated-loop-space i A)

However, note that there is an Obi-wan error in this definition: The 0-th concrete homotopy group corresponds to the first abstract homotopy group.

Definitions

The underlying sets of the homotopy groups

module _
  {l : Level} (n : ℕ) (A : Pointed-Type l)
  where

  set-homotopy-group : Set l
  set-homotopy-group = trunc-Set (type-iterated-loop-space n A)

  type-homotopy-group : UU l
  type-homotopy-group = type-Set set-homotopy-group

  is-set-type-homotopy-group : is-set type-homotopy-group
  is-set-type-homotopy-group = is-set-type-Set set-homotopy-group

  point-homotopy-group : type-homotopy-group
  point-homotopy-group = unit-trunc-Set (point-iterated-loop-space n A)

  pointed-type-homotopy-group : Pointed-Type l
  pr1 pointed-type-homotopy-group = type-homotopy-group
  pr2 pointed-type-homotopy-group = point-homotopy-group

The concrete homotopy groups

module _
  {l : Level} (n : ℕ) (A : Pointed-Type l)
  where

  concrete-homotopy-group : Concrete-Group l
  concrete-homotopy-group =
    concrete-group-Pointed-Type (iterated-loop-space n A)

Recent changes