open import 1Lab.Reflection.Induction
open import 1Lab.Prelude

open import Algebra.Group.Cat.Base
open import Algebra.Group.Homotopy
open import Algebra.Group.Ab
open import Algebra.Group

open import Cat.Base

open import Data.Set.Truncation

open import Homotopy.Connectedness
open import Homotopy.Conjugation

module Homotopy.Space.Delooping where

Deloopings🔗

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 $G\text{,}$ we construct a type $\mathbf{B}G$ with ${\pi }_1(\mathbf{B}G)\equiv G\text{.}$ We call $\mathbf{B}G$ the delooping of $G\text{.}$

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

  data Deloop : Type ℓ where
    base    : Deloop
    path    : ⌞ G ⌟ → base ≡ base
    path-sq : (x y : ⌞ G ⌟) → Square refl (path x) (path (x ⋆ y)) (path y)
    squash  : is-groupoid Deloop

  Deloop∙ : Type∙ ℓ
  Deloop∙ = Deloop , base

  private instance
    H-Level-Deloop : ∀ {n} → H-Level Deloop ( + n)
    H-Level-Deloop = basic-instance  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 ${\pi }_1(\mathbf{B}G)\equiv G\text{.}$ We then have the “interesting” higher constructors: path lets us turn any element of $G$ 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:

  abstract
    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

    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 the following monstruous type since it works for mapping into arbitrary groupoids. As usual, if we’re mapping into a family of types that’s more truncated (i.e. a family of sets or propositions), some of the higher cases become automatic.

  Deloop-elim
    : ∀ {ℓ'} (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 )
    Deloop-elim (quote Deloop)

  unquoteDecl Deloop-elim-set = make-elim-with (default-elim-visible into )
    Deloop-elim-set (quote Deloop)

  unquoteDecl Deloop-elim-prop = make-elim-with (default-elim-visible into )
    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).

We’ll want to define the family Code by induction on Deloop. First, since we have to map into a groupoid, we’ll map into the type $\mathrm{Set}\text{,}$ rather than $\mathrm{Type}\text{.}$ This takes care of the truncation constructor (which is hidden from the page since it is entirely formulaic): let’s tackle the rest in order. We can also handle the base case, since Code base = G was already a part of our specification.

  Code : Deloop → Set ℓ
  Code = go module Code where
    open is-iso

    base-case : Set ℓ
    ∣ base-case ∣    = ⌞ G ⌟
    base-case .is-tr = hlevel 

To handle the path case, we’ll have to produce, given an element $x:G\text{,}$ an equivalence $G\simeq G\text{:}$ by univalence, we can then lift this equivalence to a path $G\equiv G\text{,}$ which we can use as the path-case. While there might be many maps $G\to (G\simeq G)\text{,}$ one is canonical: the Yoneda embedding map, sending $x$ to $y\mapsto xy\text{.}$

    path-case : ⌞ G ⌟ → base-case ≡ base-case
    path-case x = n-ua eqv module path-case where
      rem₁ : is-iso (_⋆ x)
      rem₁ .inv = _⋆ x ⁻¹
      rem₁ .rinv x = cancelr inversel
      rem₁ .linv x = cancelr inverser

      eqv : ⌞ G ⌟ ≃ ⌞ G ⌟
      eqv .fst = _
      eqv .snd = is-iso→is-equiv rem₁

    open path-case

Finally, we can satisfy the coherence case path-sq by an algebraic calculation on paths:

    coh : ∀ x y → Square refl (path-case x) (path-case (x ⋆ y)) (path-case y)
    coh x y = n-Type-square $ transport (sym Square≡double-composite-path) $
      ua (eqv x) ∙ ua (eqv y) ≡˘⟨ ua∙ ⟩≡˘
      ua (eqv x ∙e eqv y)     ≡⟨ ap ua (Σ-prop-path! (funext λ _ → sym associative)) ⟩≡
      ua (eqv (x ⋆ y))        ∎

    go : Deloop → Set ℓ
    go base = base-case
    go (path x i) = path-case x i
    go (path-sq x y i j) = coh x y i j
    go (squash x y p q α β i j k) =
      n-Type-is-hlevel  (Code x) (Code y)
        (λ i → Code (p i))     (λ i → Code (q i))
        (λ i j → Code (α i j)) (λ i j → Code (β i j))
        i j k

We can 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.

  opaque
    encode : ∀ x → base ≡ x → Code ʻ x
    encode x p = subst (Code ʻ_) p unit

  decode : ∀ x → Code ʻ x → base ≡ x
  decode = go where
    coh : ∀ x → PathP (λ i → Code ʻ path x i → base ≡ path x i) path path
    coh x i c j = hcomp (∂ i ∨ ∂ j) λ where
      k (k = i0) → path (ua-unglue (Code.path-case.eqv x) i c) j
      k (i = i0) → path-sq c x (~ k) j
      k (i = i1) → path c j
      k (j = i0) → base
      k (j = i1) → path x (i ∨ ~ k)

    go : ∀ x → Code ʻ x → base ≡ x
    go base c = path c
    go (path x i) c = coh x i c
    go (path-sq x y i j) = is-set→squarep
      (λ i j → fun-is-hlevel {A = Code ʻ path-sq x y i j}  (Deloop.squash base (path-sq x y i j)) )
      (λ i → path) (coh x) (coh (x ⋆ y)) (coh y) i j
    go (squash x y p q α β i j k) =
      is-hlevel→is-hlevel-dep {B = λ x → Code ʻ x → base ≡ x}  (λ x → hlevel )
        (go x) (go y) (λ i → go (p i)) (λ i → go (q i))
        (λ i j → go (α i j)) (λ i j → go (β i j)) (squash x y p q α β) i j k

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.

  opaque
    unfolding encode

    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)
        p

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\star 1=1\text{.}$

    decode→encode : ∀ x (c : Code ʻ x) → encode x (decode x c) ≡ c
    decode→encode =
      Deloop-elim-prop
        (λ x → (c : Code ʻ x) → encode x (decode x c) ≡ c)
        (λ x → Π-is-hlevel  λ _ → 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 (decode base , iso (encode base) encode→decode (decode→encode base))

  G≡π₁B : G ≡ πₙ₊₁  (Deloop , base)
  G≡π₁B = ∫-Path
    (total-hom (λ x → inc (path x))
      record { pres-⋆ = λ x y → ap ∥_∥₀.inc (path-∙ _ _) })
    (∙-is-equiv (G≃ΩB .snd) (∥-∥₀-idempotent (squash base base)))

Since Deloop is a groupoid, each of its loop spaces is automatically a set, so we do not necessarily need the truncation when taking its fundamental group. This alternative construction is worth mentioning since it allows us to trade a proof that encode preserves multiplication for proofs that it also preserves the identity, inverses, differences, etc.

  encode-is-group-hom
    : is-group-hom (π₁Groupoid.on-Ω Deloop∙ squash) (G .snd) (encode base)
  encode-is-group-hom .is-group-hom.pres-⋆ x y = eqv.injective₂ (eqv.ε _) $
    path (encode base x ⋆ encode base y)          ≡⟨ path-∙ (encode base x) (encode base y) ⟩≡
    path (encode base x) ∙ path (encode base y)   ≡⟨ ap₂ _∙_ (eqv.ε _) (eqv.ε _) ⟩≡
    x ∙ y                                         ∎
    where module eqv = Equiv G≃ΩB

  module encode where
    open is-group-hom encode-is-group-hom public
    open Equiv (Equiv.inverse G≃ΩB) public

instance
  H-Level-Deloop : ∀ {n} {ℓ} {G : Group ℓ} → H-Level (Deloop G) ( + n)
  H-Level-Deloop {n} = basic-instance  squash

For abelian groups🔗

module _ {ℓ} (G : Group ℓ) (ab : is-commutative-group G) where
  open Group-on (G .snd)
  open is-group-hom

  opaque

If $G$ is an abelian group, then we can characterise the loop spaces of $\mathbf{B}G$ based at totally arbitrary points, rather than the above characterisation which only applies for the loop space at base. Our proof starts with the following immediate observation: multiplication in ${\pi }_1(\mathbf{B}G)$ is commutative as well.

    ∙-comm : (p q : Path (Deloop G) base base) → p ∙ q ≡ q ∙ p
    ∙-comm p q = encode.injective G
      (encode.pres-⋆ G _ _ ·· ab _ _ ·· sym (encode.pres-⋆ G _ _))

We’ll construct a function that computes the “winding number” of a loop with arbitrary base.

  winding : {x : Deloop G} → x ≡ x → ⌞ G ⌟
  winding {x = x} = go x module windingⁱ where

    hl : (x : Deloop G) → is-set (x ≡ x → ⌞ G ⌟)
    hl _ = hlevel 

    interleaved mutual
      go   : (x : Deloop G) → x ≡ x → ⌞ G ⌟

      coherence : Type _ [ i1 ↦ (λ ._ → (x : ⌞ G ⌟) → PathP (λ i → path {G = G} x i ≡ path x i → ⌞ G ⌟) (encode G base) (encode G base)) ]
      coh : outS coherence

      deg : base ≡ base → ⌞ G ⌟
      deg = encode G base

      go base loop = deg loop

If the loop is indeed based at the basepoint constructor, then we can appeal to the existing construction; We’ll abbreviate it as deg for this construction.

Since our codomain is a set, the higher cases are both handled mechanically; We omit them from the page in the interest of parsimony. We’re left with tackling the path case, which means constructing a term exhibiting the coherence below:

      coherence = inS ( ∀ b →
        PathP (λ i → path b i ≡ path b i → ⌞ G ⌟) deg deg)

This condition is a bit funky, since at first glance it looks like all we must do is equate deg with itself. However, we’re doing this over a non-trivial identification in the domain. By extensionality for dependent functions, the above is equivalent to showing that deg produces identical results given an element $b:G$ and loops $x_0\text{,}$ $x_1$ fiting into a commutative square

Since commutativity of the diagram above says precisely that $x_1$ is the conjugate of $x_0$ by $\mathrm{path}(b)\text{,}$ we can reason about conjugation instead; And since we’ve shown that $x_0\mathrm{path}(b)=\mathrm{path}(b)x_0\text{,}$ this conjugation is just $x_1$ again. That finishes the construction:

      abstract
        coh b = funext-dep λ {x₀} {x₁} p → ap deg $ sym $
          x₁               ≡˘⟨ pathp→conj p ⟩≡˘
          conj (path b) x₀ ≡⟨ conj-commutative (∙-comm x₀ (path b)) ⟩≡
          x₀               ∎

      go (path x i) loop = coh x i loop

      go (path-sq x y i j) = is-set→squarep (λ i j → hl (path-sq x y i j))
        (λ j → encode G base) (coh x) (coh (x ⋆ y)) (coh y)
        i j
      go (squash x y p q α β i j k) =
        is-hlevel→is-hlevel-dep  (λ x → is-hlevel-suc  (hl x))
          (go x) (go y) (λ i → go (p i)) (λ j → go (q j))
          (λ i j → go (α i j)) (λ i j → go (β i j))
          (squash x y p q α β) i j k

  {-# DISPLAY windingⁱ.go _ p = winding p #-}

We could go on to define the inverse to winding similar to how we constructed decode, but there’s a trick: since being an equivalence is a proposition, if we want to show ${\mathrm{winding}}_x$ is an equivalence for arbitrary $x\text{,}$ it suffices to do so for ${\mathrm{winding}}_{\mathrm{base}}=\mathrm{encode}\text{;}$ but we’ve already shown that’s an equivalence! A similar remark allows us to conclude that ${\mathrm{winding}}_x$ is a group homomorphism $\Omega (\mathbf{B}G,x)\to G\text{.}$

  opaque
    winding-is-equiv : ∀ x → is-equiv (winding {x})
    winding-is-equiv = Deloop-elim-prop G _ (λ _ → hlevel ) $
      Equiv.inverse (G≃ΩB G) .snd

    winding-is-group-hom : ∀ x →
      is-group-hom (π₁Groupoid.on-Ω (Deloop G , x) (hlevel ))
        (G .snd) (winding {x})
    winding-is-group-hom = Deloop-elim-prop G _ (λ x → hlevel ) λ where
      .pres-⋆ x y → encode.pres-⋆ G x y

We can then obtain a nice interface for working with winding.

  module winding {x} where
    open Equiv (winding , winding-is-equiv x) public
    open is-group-hom (winding-is-group-hom x) public

  pathᵇ : (x : Deloop G) → ⌞ G ⌟ → x ≡ x
  pathᵇ _ = winding.from

  -- Want: pathᵇ base ≡ path, definitionally
  -- Have: pathᵇ base is a projection from some opaque record
  -- Soln: Evil hack!
  opaque
    unfolding winding-is-equiv

    winding-is-equiv-base : winding-is-equiv base ≡ Equiv.inverse (G≃ΩB G) .snd
    winding-is-equiv-base = prop!

  {-# REWRITE winding-is-equiv-base #-}

  _ : pathᵇ base ≡ path
  _ = refl -- MUST check!

  pathᵇ-sq : ∀ (x : Deloop G) g h → Square refl (pathᵇ x g) (pathᵇ x (g ⋆ h)) (pathᵇ x h)
  pathᵇ-sq = Deloop-elim-prop G _ (λ x → hlevel ) λ g h → path-sq g h

Deloop-is-connected : ∀ {ℓ} {G : Group ℓ} → is-connected∙ (Deloop G , base)
Deloop-is-connected = Deloop-elim-prop _ _ (λ _ → hlevel ) (inc refl)