open import 1Lab.Prelude open import Algebra.Group open import Data.Set.Truncation 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 : β b β β₯ b β‘ 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 . 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) 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
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 (Ξ» _ β 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)