module Algebra.Group.Homotopy where
Homotopy Groupsπ
Given a pointed type we refer to the type as the loop space of , and refer to it in short as . Since we always have , is itself a pointed type, the construction can be iterated, a process which we denote .
Ξ©βΏ : Nat β Typeβ β β Typeβ β Ξ©βΏ zero A = A Ξ©βΏ (suc n) (A , x) with Ξ©βΏ n (A , x) ... | (T , x) = Path T x x , refl
For positive
,
we can give
a Group structure, obtained by truncating the higher groupoid
structure that
is equipped with. We call the sequence
the homotopy groups of
,
but remark that the indexing used by Οβ
is off by 1: Οβ 0 A
is
the fundamental group
.
Οβββ : Nat β Typeβ β β Group β Οβββ n t = to-group omega where omega : make-group β₯ Ξ©βΏ (suc n) t .fst β₯β omega .make-group.group-is-set = 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 (β-inv-l x i) omega .make-group.idl = β₯-β₯β-elim (Ξ» _ β is-propβis-set (squash _ _)) Ξ» x i β inc (β-id-l x i)
A direct cubical transcription of the Eckmann-Hilton argument tells us that path concatenation is commutative for is commutative, independent of .
Ξ©βΏβΊΒ²-is-abelian-group : β {β} {A : Typeβ β} (n : Nat) (p q : Ξ©βΏ (2 + n) A .fst) β p β q β‘ q β p Ξ©βΏβΊΒ²-is-abelian-group n p q = transport (Ξ» k β ap (Ξ» x β β-id-r x k) p β ap (Ξ» x β β-id-l x k) q β‘ ap (Ξ» x β β-id-l x k) q β ap (Ξ» x β β-id-r 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
.
The outer rectangle shows p β q β‘ q β p
, which is filled by
transporting the two inner squares using β-id-r
on p j
and β-id-l
on q j
. Note that β-id-r refl
and
β-id-l 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 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))
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 , we construct a type with . We call the delooping of .
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) instance 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
.
We then have the βinterestingβ higher constructors: path lets us turn any element of
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
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 (β-id-r _) β©β‘ path unit β β refl β β‘Λβ¨ apΒ‘ (β-inv-r _) β©β‘Λ 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) β‘β¨ β-inv-r _ β©β‘ 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.
Deloop-elim : β {β'} (P : Deloop β Type β') β (β x β is-hlevel (P x) 3) β (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 Deloop-elim P grpd pp ploop psq base = pp Deloop-elim P grpd pp ploop psq (path x i) = ploop x i Deloop-elim P grpd pp ploop psq (path-sq x y i j) = psq x y i j Deloop-elim P grpd pp ploop psq (squash a b p q r s i j k) = is-hlevelβis-hlevel-dep 2 grpd (g a) (g b) (Ξ» i β g (p i)) (Ξ» i β g (q i)) (Ξ» i j β g (r i j)) (Ξ» i j β g (s i j)) (squash a b p q r s) i j k where g = Deloop-elim P grpd pp ploop psq Deloop-elim-prop : β {β'} (P : Deloop β Type β') β (β x β is-prop (P x)) β P base β β x β P x Deloop-elim-prop P pprop p = Deloop-elim P (Ξ» x β is-propβis-hlevel-suc {n = 2} (pprop x)) p (Ξ» x β is-propβpathp (Ξ» i β pprop (path x i)) p p) (Ξ» x y β is-propβsquarep (Ξ» i j β pprop (path-sq x y i j)) _ _ _ _)
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 (map 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
-types
is a
-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
map : G β G β‘ G
for the path constructor; The
constructor path-sq then requires that
map
be a homomorphism from
to
.
where map : β x β β G β β β G β map 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 as the definition of the map, which is an automorphism of since it is invertible by , and it preserves composition by associativity of , as is shown in the lemma below.
lemma : β x y β ua (map x) β ua (map y) β‘ ua (map (x β y)) lemma x y = ua (map x) β ua (map y) β‘β¨ sym uaβ β©β‘ ua (map x βe map y) β‘β¨ ap ua (Ξ£-prop-path is-equiv-is-prop (funext Ξ» z β sym (Group-on.associative (G .snd)))) β©β‘ ua (map (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.
path (Ξ» 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) 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 .
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 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)))