open import 1Lab.Prelude

open import Algebra.Group.Cat.Base
open import Algebra.Semigroup
open import Algebra.Monoid
open import Algebra.Group
open import Algebra.Magma

open import Data.Set.Truncation

module Algebra.Group.Homotopy where


# Homotopy Groupsπ

Given a pointed type $(A, a)$ we refer to the type $a = a$ as the loop space of $A$, and refer to it in short as $\Omega A$. Since we always have ${\mathrm{refl}} : a = a$, $\Omega A$ is itself a pointed type, the construction can be iterated, a process which we denote $\Omega^n A$.

Ξ©βΏ : Nat β Typeβ β β Typeβ β
Ξ©βΏ zero A    = A
Ξ©βΏ (suc n) (A , x) with Ξ©βΏ n (A , x)
... | (T , x) = Path T x x , refl


For positive $n$, we can give $\Omega^n A$ a Group structure, obtained by truncating the higher groupoid structure that $A$ is equipped with. We call the sequence $\pi_n(A)$ the homotopy groups of $A$, but remark that the indexing used by Οβ is off by 1: Οβ 0 A is the fundamental group $\pi_1(A)$.

Οβββ : 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.invr =
β₯-β₯β-elim (Ξ» _ β is-propβis-set (squash _ _)) Ξ» x i β inc (β-inv-r 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 $\Omega^{n + 2} A$ is commutative, independent of $A$.

Ξ©βΏβΊΒ²-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 $\Omega^{n + 1} A$. 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 $\pi_{n+2}$ is an Abelian group:

Οβββ-is-abelian-group : β {β} {A : Typeβ β} (n : Nat)
β is-abelian-group (Οβββ (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 $G$, we construct a type $B(G)$ with $\pi_1(B(G)) \equiv G$. We call $B(G)$ the delooping of $G$.

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 $\pi_1(B(G)) \equiv G$. We then have the βinterestingβ higher constructors: path lets us turn any element of $G$ 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 $n$-types is a $(n+1)$-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 $G$ to ${\mathrm{Aut}}(G)$.

    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 $y \mapsto y \star x$ as the definition of the map, which is an automorphism of $G$ since it is invertible by $y \mapsto y \star x^{-1}$, and it preserves composition by associativity of $\star$, 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 $1 \star 1 = 1$.

  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)))