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! λ x y z i → inc (∙-assoc x y z i) omega .make-group.invl = elim! λ x i → inc (∙-invl x i) omega .make-group.idl = elim! λ x i → inc (∙-idl x i)
A direct cubical transcription of the Eckmann-Hilton argument tells us that path concatenation 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 i → inc (Ωⁿ⁺²-is-abelian-group n x y i)
We can give an alternative construction of the fundamental group for types that are known to be groupoids: in that case, we can avoid using a set truncation since the loop space is already a set.
module π₁Groupoid {ℓ} ((T , t) : Type∙ ℓ) (grpd : is-groupoid T) where private mk : make-group (t ≡ t) mk .make-group.group-is-set = grpd t t mk .make-group.unit = refl mk .make-group.mul = _∙_ mk .make-group.inv = sym mk .make-group.assoc = ∙-assoc mk .make-group.invl = ∙-invl mk .make-group.idl = ∙-idl on-Ω : Group-on (t ≡ t) on-Ω = to-group-on mk π₁ : Group ℓ π₁ = to-group mk π₁≡π₀₊₁ : π₁ ≡ πₙ₊₁ 0 (T , t) π₁≡π₀₊₁ = ∫-Path (total-hom inc (record { pres-⋆ = λ _ _ → refl })) (∥-∥₀-idempotent (grpd _ _))