module Algebra.Group.Homotopy where

Homotopy groupsπŸ”—

Given a pointed type we refer to the type as the loop space of , and refer to it in short as Since we always have is itself a pointed type, the construction can be iterated, a process which we denote

Ωⁿ : Nat β†’ Typeβˆ™ β„“ β†’ Typeβˆ™ β„“
Ωⁿ zero A    = A
Ωⁿ (suc n) (A , x) with Ωⁿ n (A , x)
... | (T , x) = Path T x x , refl

For positive we can give a Group structure, obtained by truncating the higher groupoid structure that is equipped with. We call the sequence the homotopy groups of but remark that the indexing used by Ο€β‚™β‚Šβ‚ is off by 1: Ο€β‚™β‚Šβ‚ 0 A is the fundamental group

Ο€β‚™β‚Šβ‚ : 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 is commutative, independent of

Ωⁿ⁺²-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 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 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 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 _ _))