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 (β-invl x i) omega .make-group.idl = β₯-β₯β-elim (Ξ» _ β is-propβis-set (squash _ _)) Ξ» x i β inc (β-idl 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 β β-idr x k) p β ap (Ξ» x β β-idl x k) q β‘ ap (Ξ» x β β-idl x k) q β ap (Ξ» x β β-idr 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 β-idr
on p j
and
β-idl
on q j
. Note
that β-idr refl
and β-idl 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 (β-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 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-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 3) Deloop-elim (quote Deloop) Deloop-elim-prop : β {β'} (P : Deloop β Type β') β (β x β is-prop (P x)) β P base β β x β P x unquoteDef Deloop-elim-prop = make-elim-with (default-elim-visible into 1) 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)
. First, to
define Code
, we perform induction on
Deloop
:
Code : Deloop β Set β Code = Deloop-elim _ (Ξ» _ β hlevel 3) (G .fst) (Ξ» x β n-ua (act 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 Set
s: 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
act : G β G β‘ G
for the path
constructor;
The constructor path-sq
then
requires that act
be a homomorphism from
to
.
where act : β x β β G β β β G β act 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 act, 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 (act x) β ua (act y) β‘ ua (act (x β y)) lemma x y = ua (act x) β ua (act y) β‘β¨ sym uaβ β©β‘ ua (act x βe act y) β‘β¨ ap ua (Ξ£-prop-path is-equiv-is-prop (funext Ξ» z β sym (Group-on.associative (G .snd)))) β©β‘ ua (act (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)))