module Algebra.Group.Homotopy.BAut where

Deloopings of automorphism groups🔗

Recall that any set XX generates a group Sym(X)\mathrm{Sym}(X), given by the automorphisms XXX \simeq X. We also have a generic construction of deloopings: special spaces K(G,1)K(G,1) (for a group GG), where the fundamental group π1(K(G,1))\pi_1(K(G,1)) recovers GG. For the specific case of deloping automorphism groups, we can give an alternative construction: The type of small types merely equivalent to XX has a fundamental group of Sym(X)\mathrm{Sym}(X).

module _ {} (T : Type ℓ) where
  BAut : Type (lsuc ℓ)
  BAut = Σ[ B ∈ Type ℓ ] ∥ T ≃ B ∥

  base : BAut
  base = T , inc (id , id-equiv)

The first thing we note is that BAut is a connected type, meaning that it only has “a single point”, or, more precisely, that all of its interesting information is in its (higher) path spaces:

  connected : (x : BAut)  ∥ x ≡ base ∥
  connected (b , x) =
    ∥-∥-elim {P = λ x (b , x) ≡ base ∥}  _  squash)  e  inc (p _ _)) x
    where
      p :  b e  (b , inc e) ≡ base
      p _ = EquivJ  B e  (B , inc e) ≡ base) refl

We now turn to proving that π1(B(X))(XX)\pi_1(\operatorname*{\mathbf{B}}(X)) \simeq (X \simeq X). We will define a type family Code(b)\mathrm{Code}(b), where a value p:Code(x)p : \mathrm{Code}(x) codes for an identification pbasep \equiv \mathrm{base}. Correspondingly, there are functions to and from these types: The core of the proof is showing that these functions, encode and decode, are inverses.

  Code : BAut  Type ℓ
  Code b = T ≃ b .fst

  encode :  b  base ≡ b  Code b
  encode x p = path→equiv (ap fst p)

  decode :  b  Code b  base ≡ b
  decode (b , eqv) rot = Σ-pathp (ua rot) (is-prop→pathp  _  squash) _ _)

Recall that base\mathrm{base} is the type TT itself, equipped with the identity equivalence. Hence, to code for an identification base(X,e)\mathrm{base} \equiv (X, e), it suffices to record ee — which by univalence corresponds to a path ua(e):TX\mathrm{ua}(e) : T \equiv X. We can not directly extract the equivalence from a given point (X,e):B(X)(X, e) : \operatorname*{\mathbf{B}}(X): it is “hidden away” under a truncation. But, given an identification p:bbasep : b \equiv \mathrm{base}, we can recover the equivalence by seeing how pp identifies XTX \equiv T.

  decode∘encode :  b (p : base ≡ b)  decode b (encode b p) ≡ p
  decode∘encode b =
    J  b p  decode b (encode b p) ≡ p)
      (Σ-prop-square  _  squash) sq)
    where
      sq : ua (encode base refl) ≡ refl
      sq = ap ua path→equiv-refl ∙ ua-id-equiv

Encode and decode are inverses by a direct application of univalence.

  encode∘decode :  b (p : Code b)  encode b (decode b p) ≡ p
  encode∘decode b p = ua.η _

We now have the core result: Specialising encode and decode to the basepoint, we conclude that loop space basebase\mathrm{base} \equiv \mathrm{base} is equivalent to Sym(X)\mathrm{Sym}(X).

  Ω¹BAut : (base ≡ base)(T ≃ T)
  Ω¹BAut = Iso→Equiv
    (encode base , iso (decode base) (encode∘decode base) (decode∘encode base))

We can also characterise the h-level of these connected components. Intuitively the h-level should be one more than that of the type we’re delooping, because BAut “only has one point” (it’s connected), and as we established right above, the space of loops of that point is the automorphism group we delooped. The trouble here is that BAut has many points, and while we can pick paths between any two of them, we can not do so continuously (otherwise BAut would be a proposition).

This turns out not to matter! Since “being of h-level nn” is a proposition, our discontinuous (i.e.: truncated) method of picking paths is just excellent. In the case when TT is contractible, we can directly get at the underlying equivalences, but for the higher h-levels, we proceed exactly by using connectedness.

  BAut-is-hlevel :  n  is-hlevel T n  is-hlevel BAut (1 + n)
  BAut-is-hlevel zero hl (x , f) (y , g) =
    Σ-prop-path  _  squash) (sym (ua f') ∙ ua g')
    where
      extract :  {X}  is-prop (T ≃ X)
      extract f g = Σ-prop-path is-equiv-is-prop $ funext λ x 
        ap fst (is-contr→is-prop ((f e⁻¹) .snd .is-eqv (hl .centre))
          (f .fst x , is-contr→is-prop hl _ _)
          (g .fst x , is-contr→is-prop hl _ _))

      f' = ∥-∥-rec extract  x  x) f
      g' = ∥-∥-rec extract  x  x) g
  BAut-is-hlevel (suc n) hl x y =
    ∥-∥-elim₂ {P = λ _ _  is-hlevel (x ≡ y) (1 + n)}
       _ _  is-hlevel-is-prop _)
       p q  transport (ap₂  a b  is-hlevel (a ≡ b) (1 + n)) (sym p) (sym q))
        (is-hlevel≃ (1 + n) Ω¹BAut (≃-is-hlevel (1 + n) hl hl)))
      (connected x) (connected y)