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\mathrm{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 equipped 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 = to-group omega where
  omega : make-group βˆ₯ Ωⁿ (suc n) t .fst βˆ₯β‚€
  omega = 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 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 =
    (Ξ» 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+1A\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 Ο€n+2\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))


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 BG\mathbf{B} G with Ο€1(BG)≑G\pi_1(\mathbf{B} G) \equiv G. We call BG\mathbf{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 ⌟ β†’ base ≑ base
    path-sq : (x y : ⌞ G ⌟) β†’ 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(BG)≑G\pi_1(\mathbf{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 (βˆ™-idr _) βŸ©β‰‘
      path unit βˆ™ ⌜ refl ⌝                    β‰‘Λ˜βŸ¨ apΒ‘ (βˆ™-invr _)  βŸ©β‰‘Λ˜
      path unit βˆ™ path unit βˆ™ sym (path unit) β‰‘βŸ¨ βˆ™-assoc _ _ _ βˆ™ apβ‚‚ _βˆ™_ (sym (path-βˆ™ _ _)) refl βŸ©β‰‘
      path ⌜ unit ⋆ unit ⌝ βˆ™ sym (path unit)  β‰‘βŸ¨ ap! G.idr βŸ©β‰‘
      path unit βˆ™ sym (path unit)             β‰‘βŸ¨ βˆ™-invr _  βŸ©β‰‘
      refl                                    ∎

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-groupoid (P x))
    β†’ (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
  unquoteDef Deloop-elim = make-elim-with (default-elim-visible into 3)
    Deloop-elim (quote Deloop)

    : βˆ€ {β„“'} (P : Deloop β†’ Type β„“')
    β†’ (βˆ€ x β†’ is-prop (P x))
    β†’ P base
    β†’ βˆ€ x β†’ P x
  unquoteDef Deloop-elim-prop = make-elim-with (default-elim-visible into 1)
    Deloop-elim-prop (quote Deloop)

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)
      (Ξ» x β†’ n-ua (act x))
      Ξ» x y β†’ n-Type-square (transport (sym Square≑double-composite-path) (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 act : G β†’ G ≑ G for the path constructor; The constructor path-sq then requires that act be a homomorphism from GG to Aut(G)\mathrm{Aut}(G).

      act : βˆ€ x β†’ ⌞ G ⌟ ≃ ⌞ G ⌟
      act 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 y↦y⋆xy \mapsto y \star x as the definition of the act, which is an automorphism of GG since it is invertible by y↦y⋆xβˆ’1y \mapsto y \star x^{-1}, and it preserves composition by associativity of ⋆\star, as is shown in the lemma below.

      lemma : βˆ€ x y β†’ ua (act x) βˆ™ ua (act y) ≑ ua (act (x ⋆ y))
      lemma x y =
        ua (act x) βˆ™ ua (act y) β‰‘βŸ¨ sym uaβˆ™ βŸ©β‰‘
        ua (act x βˆ™e act y)     β‰‘βŸ¨ ap ua (Ξ£-prop-path is-equiv-is-prop (funext Ξ» z β†’ sym (Group-on.associative (G .snd)))) βŸ©β‰‘
        ua (act (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 1⋆1=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 ⌟ ≃ (base ≑ base)
  G≃ΩB = Isoβ†’Equiv (path , iso (encode base) encodeβ†’decode (decodeβ†’encode base))

  G≑π₁B : G ≑ Ο€β‚™β‚Šβ‚ 0 (Deloop , base)
  G≑π₁B = ∫-Path Groups-equational
    (total-hom (Ξ» x β†’ inc (path x)) (record { pres-⋆ = Ξ» x y β†’ ap βˆ₯_βˆ₯β‚€.inc (path-βˆ™ _ _) }))
    (βˆ™-is-equiv (G≃ΩB .snd) (βˆ₯-βˆ₯β‚€-idempotent (squash base base)))