module Algebra.Group.Homotopy.BAut where
Deloopings of automorphism groups🔗
Recall that any set generates a group given by the automorphisms We also have a generic construction of deloopings: special spaces (for a group where the fundamental group recovers For the specific case of deloping automorphism groups, we can give an alternative construction: The type of small types merely equivalent to has a fundamental group of
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 = elim! λ b e → inc (p b e) where p : ∀ b e → (b , inc e) ≡ base p _ = EquivJ (λ B e → (B , inc e) ≡ base) refl
We now turn to proving that
We will define a type family
where a value
codes for an identification
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 is the type itself, equipped with the identity equivalence. Hence, to code for an identification it suffices to record — which by univalence corresponds to a path We can not directly extract the equivalence from a given point it is “hidden away” under a truncation. But, given an identification we can recover the equivalence by seeing how identifies
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) (ua.ε refl))
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
is equivalent to
Ω¹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 ” is a proposition, our discontinuous (i.e.: truncated) method of picking paths is just excellent. In the case when 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! (sym (ua f') ∙ ua g') where extract : ∀ {X} → is-prop (T ≃ X) extract f g = ext λ 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)) (Equiv→is-hlevel (1 + n) Ω¹BAut (≃-is-hlevel (1 + n) hl hl))) (connected x) (connected y)