open import 1Lab.Prelude

open import Algebra.Semigroup
open import Algebra.Monoid
open import Algebra.Group
open import Algebra.Magma

open import Data.Set.Truncation

module Algebra.Group.Homotopy where

Homotopy Groups🔗

Given a pointed type (A,a)(A, a) we refer to the type a=aa = a as the loop space of AA, and refer to it in short as ΩA\Omega A. Since we always have refl:a=a\id{refl} : a = a, ΩA\Omega A is itself a pointed type, the construction can be iterated, a process which we denote ΩnA\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 nn, we can give ΩnA\Omega^n A a Group structure, obtained by truncating the higher groupoid structure that AA is equiped with. We call the sequence πn(A)\pi_n(A) the homotopy groups of AA, but remark that the indexing used by πₙ is off by 1: πₙ 0 A is the fundamental group π1(A)\pi_1(A).

πₙ₊₁ : Nat  Type∙   Group 
πₙ₊₁ n t .fst =  Ω^ (suc n) t .fst ∥₀
πₙ₊₁ n t .snd =
  make-group squash
    (inc refl)
    (∥-∥₀-map₂ _∙_)
    (∥-∥₀-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.

    (∥-∥₀-elim₃  _ _ _  is-prop→is-set (squash _ _))
      λ x y z i  inc (∙-assoc x y z (~ i)))
    (∥-∥₀-elim  _  is-prop→is-set (squash _ _))
      λ x i  inc (∙-inv-l x i))
    (∥-∥₀-elim  _  is-prop→is-set (squash _ _))
      λ x i  inc (∙-inv-r x i))
    (∥-∥₀-elim  _  is-prop→is-set (squash _ _))
      λ x i  inc (∙-id-l x i))

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

  :  {} {A : Type∙ } (n : Nat) (p q : Ω^ (2 + n) A .fst)
   p  q  q  p
Ωⁿ⁺²-is-abelian-group n p q =
     i  ap  x  ∙-id-r x i) p  ap  x  ∙-id-l x i) q
          ap  x  ∙-id-l x i) q  ap  x  ∙-id-r x i) p)
     i   j  p (j  ~ i)  q (j  i))
           j  p (~ i  j)  q (i  j)))

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

πₙ₊₂-is-abelian-group :  {} {A : Type∙ } (n : Nat)
                    is-abelian-group (πₙ₊₁ (1 + n) A)
πₙ₊₂-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))


A natural question to ask, given that all pointed types have a fundamental group, is whether every group arises as the fundamental group of some type. The answer to this question is “yes”, but in the annoying way that questions like these tend to be answered: Given any group GG, we construct a type B(G)B(G) with π1(B(G))G\pi_1(B(G)) \equiv G. We call B(G)B(G) the delooping of GG.

module _ {} (G : Group ) where
  module G = Group-on (G .snd)
  open G

  data Deloop : Type  where
    base    : Deloop
    squash  : is-groupoid Deloop
    path    : G .fst  base  base
    path-sq : (x y : G .fst)  Square refl (path x) (path (x  y)) (path y)

    H-Level-Deloop :  {n}  H-Level Deloop (3 + n)
    H-Level-Deloop = basic-instance 3 squash

The delooping is constructed as a higher inductive type. We have a generic base point, and a constructor expressing that Deloop is a groupoid; Since it is a groupoid, it has a set of loops point ≡ point: this is necessary, since otherwise we would not be able to prove that π1(B(G))G\pi_1(B(G)) \equiv G. We then have the “interesting” higher constructors: path lets us turn any element of GG to a path point ≡ point, and path-sq expresses that path is a group homomorphism. More specifically, path-sq fills the square below:

Using the uniqueness result for double composition, we derive that path is a homomorphism in the traditional sense:

    path-∙ :  x y  path (x  y)  path x  path y
    path-∙ x y i j =
      ··-unique refl (path x) (path y)
        (path (x  y)    , path-sq x y)
        (path x  path y , ∙-filler _ _)
        i .fst j
And the standard argument shows that path, being a group homomorphism, preserves the group identity.
    path-unit : path unit  refl
    path-unit =
      path unit                               ≡⟨ sym (∙-id-r _) 
      path unit  refl                        ≡⟨ ap₂ _∙_ refl (sym (∙-inv-r _))  
      path unit  path unit  sym (path unit) ≡⟨ ∙-assoc _ _ _  ap₂ _∙_ (sym (path-∙ _ _)) refl 
      path (unit  unit)  sym (path unit)    ≡⟨ ap₂ _∙_ (ap path G.idr) refl 
      path unit  sym (path unit)             ≡⟨ ∙-inv-r _  

We define an elimination principle for Deloop, which has a monstruous type since it works in full generality. We’ll also need an eliminator into propositions later, so we define that now.

    :  {ℓ'} (P : Deloop  Type ℓ')
     (∀ x  is-hlevel (P x) 3)
     (p : P base)
     (ploop :  x  PathP  i  P (path x i)) p p)
     (  x y
         SquareP  i j  P (path-sq x y i j))
                   _  p) (ploop x) (ploop (x  y)) (ploop y))
      x  P x
  Deloop-elim P grpd pp ploop psq base = pp
  Deloop-elim P grpd pp ploop psq (path x i) = ploop x i
  Deloop-elim P grpd pp ploop psq (path-sq x y i j) = psq x y i j
  Deloop-elim P grpd pp ploop psq (squash a b p q r s i j k) =
    is-hlevel→is-hlevel-dep 2 grpd
      (g a) (g b)  i  g (p i))  i  g (q i))
       i j  g (r i j))  i j  g (s i j)) (squash a b p q r s) i j k
      g = Deloop-elim P grpd pp ploop psq

    :  {ℓ'} (P : Deloop  Type ℓ')
     (∀ x  is-prop (P x))
     P base
      x  P x
  Deloop-elim-prop P pprop p =
    Deloop-elim P
       x  is-prop→is-hlevel-suc {n = 2} (pprop x)) p
       x  is-prop→pathp  i  pprop (path x i)) p p)
       x y  is-prop→squarep  i j  pprop (path-sq x y i j)) _ _ _ _)

We can then proceed to characterise the type point ≡ x by an encode-decode argument. We define a family Code, where the fibre over base is definitionally G; Then we exhibit inverse equivalences base ≡ x → Code x and Code x → base ≡ x, which fit together to establish G ≡ (base ≡ base). First, to define Code, we perform induction on Deloop:

  Code : Deloop  Set 
  Code =
    Deloop-elim _
       _  hlevel 3)
      (G .fst , Group-on.has-is-set (G .snd))
       x  n-ua (map x))
      λ x y  n-Type-square (transport (sym Square≡··) (lemma x y))

Since we must map into a type which is known to be a groupoid, we map to the type of Sets; Since the collection of nn-types is a (n+1)(n+1)-type, this is a groupoid. To arrange that the fibre over base is G, we give G as the argument for base in the elimination. This locks us into giving a family of automorphisms map : G → G ≡ G for the path constructor; The constructor path-sq then requires that map be a homomorphism from GG to Aut(G)\id{Aut}(G).

      map :  x  G .fst  G .fst
      map x = Iso→Equiv (_⋆ x , p) where
        open is-iso

        p : is-iso (_⋆ x)
        p .inv = _⋆ x ⁻¹
        p .rinv x = sym G.associative ·· ap₂ G._⋆_ refl G.inversel ·· G.idr
        p .linv x = sym G.associative ·· ap₂ G._⋆_ refl G.inverser ·· G.idr

We take yyxy \mapsto y \star x as the definition of the map, which is an automorphism of GG since it is invertible by yyx1y \mapsto y \star x^{-1}, and it preserves composition by associativity of \star, as is shown in the lemma below.

      lemma :  x y  ua (map x)  ua (map y)  ua (map (x  y))
      lemma x y =
        ua (map x)  ua (map y) ≡⟨ sym ua∙ 
        ua (map x ∙e map y)     ≡⟨ ap ua (Σ-prop-path is-equiv-is-prop (funext λ z  sym (Group-on.associative (G .snd)))) 
        ua (map (x  y))        

We then define the encoding and decoding functions. The encoding function encode is given by lifting a path from Deloop to Code. For decoding, we do induction on Deloop with Code x .fst → base ≡ x as the motive.

  encode :  x  base  x   Code x 
  encode x p = subst  x   Code x ) p unit

  decode :  x   Code x   base  x
  decode = Deloop-elim _
     _  hlevel 3)

With this motive, the type of what we must give for base reduces to G → base ≡ base, for which path suffices; The path case is handled by path-sq, and the path-sq case is automatic.

     x  ua→ λ a  path-sq _ _)
     x y  is-set→squarep  i j  hlevel 2) _ _ _ _)

Proving that these are inverses finishes the proof. For one direction, we use path induction to reduce to the case decode base (encode base refl) ≡ refl; A quick argument tells us that encode base refl is the group identity, and since path is a group homomorphism, we have path unit = refl, as required.

  encode→decode :  {x} (p : base  x)  decode x (encode x p)  p
  encode→decode p =
    J  y p  decode y (encode y p)  p)
      (ap path (transport-refl _)  path-unit)

In the other direction, we do induction on deloopings; Since the motive is a family of propositions, we can use Deloop-elim-prop instead of the full Deloop-elim, which reduces the goal to proving 11=11 \star 1 = 1.

  decode→encode :  x (c :  Code x )  encode x (decode x c)  c
  decode→encode =
       x  (c :  Code x )  encode x (decode x c)  c)
       x  Π-is-hlevel 1 λ _  Code x .is-tr _ _)
      λ c  transport-refl _  G.idl

This completes the proof, and lets us establish that the fundamental group of Deloop is G, which is what we wanted.

  G≃ΩB : G .fst  (base  base)
  G≃ΩB = Iso→Equiv (path , iso (encode base) encode→decode (decode→encode base))

  G≡π₁B : G  πₙ₊₁ 0 (Deloop , base)
  G≡π₁B = sip Group-univalent
    ( G≃ΩB ∙e (_ , ∥-∥₀-idempotent (squash base base))
    , record { pres-⋆ = λ x y i  inc (path-∙ x y i) })