module Algebra.Group.Homotopy where

Homotopy groups🔗

Given a pointed type $(A, a)$ we refer to the type $a = a$ as the loop space of $A$ , and refer to it in short as $\Omega A$ . Since we always have $\mathrm{refl} : a = a$ , $\Omega A$ is itself a pointed type, the construction can be iterated, a process which we denote $\Omega^n A$ .

Ωⁿ : Nat → Type∙ ℓ → Type∙ ℓ
Ωⁿ zero A    = A
Ωⁿ (suc n) (A , x) with Ωⁿ n (A , x)
... | (T , x) = Path T x x , refl

For positive $n$ , we can give $\Omega^n A$ a Group structure, obtained by truncating the higher groupoid structure that $A$ is equipped with. We call the sequence $\pi_n(A)$ the homotopy groups of $A$ , but remark that the indexing used by πₙ₊₁ is off by 1: πₙ₊₁ 0 A is the fundamental group $\pi_1(A)$ .

πₙ₊₁ : Nat → Type∙ ℓ → Group ℓ
πₙ₊₁ n t = to-group omega where
  omega : make-group ∥ Ωⁿ (suc n) t .fst ∥₀
  omega .make-group.group-is-set = squash
  omega .make-group.unit = inc refl
  omega .make-group.mul = ∥-∥₀-map₂ _∙_
  omega .make-group.inv = ∥-∥₀-map sym

As mentioned above, the group structure is given entirely by the groupoid structure of types: The neutral element is refl, the group operation is path concatenation, and the inverses are given by inverting paths.

  omega .make-group.assoc =
    ∥-∥₀-elim₃ (λ _ _ _ → is-prop→is-set (squash _ _))
      λ x y z i → inc (∙-assoc x y z i)
  omega .make-group.invl =
    ∥-∥₀-elim (λ _ → is-prop→is-set (squash _ _)) λ x i → inc (∙-invl x i)
  omega .make-group.idl =
    ∥-∥₀-elim (λ _ → is-prop→is-set (squash _ _)) λ x i → inc (∙-idl x i)

A direct cubical transcription of the Eckmann-Hilton argument tells us that path concatenation for $\Omega^{n + 2} A$ is commutative, independent of $A$ .

Ωⁿ⁺²-is-abelian-group
  : ∀ {ℓ} {A : Type∙ ℓ} (n : Nat) (p q : Ωⁿ (2 + n) A .fst)
  → p ∙ q ≡ q ∙ p
Ωⁿ⁺²-is-abelian-group n p q =
  transport
    (λ k → ap (λ x → ∙-idr x k) p ∙ ap (λ x → ∙-idl x k) q
         ≡ ap (λ x → ∙-idl x k) q ∙ ap (λ x → ∙-idr x k) p)
    (λ i → (λ j → p (j ∧ ~ i) ∙ q (j ∧ i))
         ∙ (λ j → p (~ i ∨ j) ∙ q (i ∨ j)))

The proof can be visualized with the following diagram, where the vertices are in $\Omega^{n + 1} A$ . The outer rectangle shows p ∙ q ≡ q ∙ p, which is filled by transporting the two inner squares using ∙-idr on p j and ∙-idl on q j. Note that ∙-idr refl and ∙-idl refl are definitionally equal. In the two inner squares, p j and q j are on different sides of the path composition, so we can use the De Morgan structure on the interval to have p and q slip by each other.

Lifting this result through the set truncation establishes that $\pi_{n+2}$ is an Abelian group:

πₙ₊₂-is-abelian-group : ∀ {ℓ} {A : Type∙ ℓ} (n : Nat)
                      → Group-on-is-abelian (πₙ₊₁ (1 + n) A .snd)
πₙ₊₂-is-abelian-group {A = A} n =
  ∥-∥₀-elim₂ (λ x y → is-prop→is-set (squash _ _))
             (λ x y i → inc (Ωⁿ⁺²-is-abelian-group n x y i))

We can give an alternative construction of the fundamental group $\pi_1$ for types that are known to be groupoids: in that case, we can avoid using a set truncation since the loop space is already a set.

module π₁Groupoid {ℓ} ((T , t) : Type∙ ℓ) (grpd : is-groupoid T) where
  private
    mk : make-group (t ≡ t)
    mk .make-group.group-is-set = grpd t t
    mk .make-group.unit         = refl
    mk .make-group.mul          = _∙_
    mk .make-group.inv          = sym
    mk .make-group.assoc        = ∙-assoc
    mk .make-group.invl         = ∙-invl
    mk .make-group.idl          = ∙-idl

  on-Ω : Group-on (t ≡ t)
  on-Ω = to-group-on mk

  π₁ : Group ℓ
  π₁ = to-group mk

  π₁≡π₀₊₁ : π₁ ≡ πₙ₊₁ 0 (T , t)
  π₁≡π₀₊₁ = ∫-Path Groups-equational
    (total-hom inc (record { pres-⋆ = λ _ _ → refl }))
    (∥-∥₀-idempotent (grpd _ _))