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
$Ξ©A.$
Since we always have
$refl:a=a,$
$Ξ©A$
is *itself* a pointed type, the construction can be iterated, a
process which we denote
$Ξ©_{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
$Ξ©_{n}A$
a `Group`

structure, obtained by truncating the higher
groupoid structure that
$A$
is equipped with. We call the sequence
$Ο_{n}(A)$
the **homotopy groups** of
$A,$
but remark that the indexing used by `Οβββ`

is off by 1:
`Οβββ 0 A`

is the **fundamental group**
$Ο_{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! Ξ» x y z i β inc (β-assoc x y z i) omega .make-group.invl = elim! Ξ» x i β inc (β-invl x i) omega .make-group.idl = elim! Ξ» x i β inc (β-idl x i)

A direct cubical transcription of the Eckmann-Hilton argument tells us that path concatenation for $Ξ©_{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
$Ξ©_{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 $Ο_{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 i β inc (Ξ©βΏβΊΒ²-is-abelian-group n x y i)

We can give an alternative construction of the fundamental group $Ο_{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 (total-hom inc (record { pres-β = Ξ» _ _ β refl })) (β₯-β₯β-idempotent (grpd _ _))