module Homotopy.HSpace where

H-Spaces🔗

An H-space structure on a pointed type consists of a binary operation equipped with paths and witnessing left- and right- unitality of respectively, together with a coherence datum connecting

record HSpace {} (A* : Type∙ ) : Type  where
  open Σ A* renaming (fst to A ; snd to a₀)
  field
    μ : A  A  A

    idl    :  x  μ a₀ x  x
    idr    :  x  μ x a₀  x
    id-coh : idl a₀  idr a₀

Here, we’re interested in the case where each and is an equivalence, so we’re really discussing invertible H-spaces. We note that if is connected then any of its H-space structures is automatically both left- and right-invertible. This is because, since “being an equivalence” is a proposition, it would suffice to check invertibility when is the basepoint, but in this case is the identity.

    μ-invl :  y  is-equiv (μ y)
    μ-invr :  y  is-equiv (flip μ y)

Using either unit law (we choose we can show that extends to a secondary “composition” operation on the loop space This operation is also unital on both the left and the right, with the side we didn’t choose having a slightly more complicated argument that involves the coherence

  _⊗_ : a₀  a₀  a₀  a₀  a₀  a₀
  p  q = conj (idl a₀) (ap₂ μ p q)

  ⊗-idl :  p  refl  p  p
  ⊗-idl p = square→conj (ap  e  ap e p) (funext idl))

  ⊗-idr :  p  p  refl  p
  ⊗-idr p =
    conj (idl a₀) (ap₂ μ p refl) ≡⟨ ap  e  conj e (ap₂ μ p refl)) id-coh 
    conj (idr a₀) (ap₂ μ p refl) ≡⟨ square→conj (ap  e  ap e p) (funext idr)) 
    p                            

Moreover, this new operation satisfies an “interchange” law, in that it preserves path composition in both variables. By an incoherent version of the Eckmann-Hilton argument, this means that composition of loops in is commutative. This implies that the only connected groupoids with H-space structures are the deloopings of abelian groups.

  ⊗-interchange :  a b c d  (a  b)  (c  d)  (a  c)  (b  d)
  ⊗-interchange a b c d =
    conj (idl a₀) (ap₂ μ (a  b) (c  d))
      ≡⟨ ap (conj (idl a₀)) (ap₂-∙ μ a b c d) 
    conj (idl a₀) (ap₂ μ a c  ap₂ μ b d)
      ≡⟨ conj-of-∙ (idl a₀) _ _ 
    (a  c)  (b  d)
      
We omit the proof here because it’s the same algebra as in the case for set-level magmas.
  private
    ∙-is-flip-⊗ : (p q : a₀  a₀)  p  q  q  p
    ∙-is-flip-⊗ p q =
      p  q                   ≡˘⟨ ap₂ _∙_ (⊗-idl p) (⊗-idr q) ≡˘
      (refl  p)  (q  refl) ≡⟨ sym (⊗-interchange refl q p refl) 
      (refl  q)  (p  refl) ≡⟨ ap₂ _⊗_ (∙-idl q) (∙-idr p) 
      q  p                   

    ∙-is-⊗ : (p q : a₀  a₀)  p  q  p  q
    ∙-is-⊗ p q =
      p  q                   ≡˘⟨ ap₂ _∙_ (⊗-idr p) (⊗-idl q) ≡˘
      (p  refl)  (refl  q) ≡⟨ sym (⊗-interchange p refl refl q) 
      (p  refl)  (refl  q) ≡⟨ ap₂ _⊗_ (∙-idr p) (∙-idl q) 
      (p  q)                 

  ∙-comm : (p q : a₀  a₀)  p  q  q  p
  ∙-comm p q = ∙-is-flip-⊗ p q  sym (∙-is-⊗ q p)

H-Space structures on deloopings🔗

We can define an H-space structure on the delooping of an abelian group by recursion. First, we fix an element and define the “path” case, by elimination into sets — so it suffices to turn a into a and to show that this is commutative.

    mul₀ : (g :  G ) (y : Deloop G)  y  y
    mul₀ g = Deloop-elim-set G _  d  hlevel 2)
      (path g)
       z  commutes→square (Deloop-ab.∙-comm G ab _ _))

Now we extend this to when is an arbitrary element of At the basepoint, we can simply return the other operand; this ensures identity on the left is definitional. For the generating paths, we can use the helper defined above. To show that this respects multiplication, we can lift the generating triangle pathᵀ to mul₀ by elimination into propositions. The truncation case is handled automatically.

    coh : (x y :  G ) (z : Deloop G)  Square refl (mul₀ x z) (mul₀ (x  y) z) (mul₀ y z)
    coh x y = Deloop-elim-prop G _  _  hlevel 1) λ i j  pathᵀ x y i j

    mul : Deloop G  Deloop G  Deloop G
    mul base            x = x
    mul (path x i)      y = mul₀ x y i
    mul (pathᵀ x y i j) z = coh x y z i j
    mul (squash x y p q α β i j k) z = squash (mul x z) (mul y z)
       i  mul (p i) z)  i  mul (q i) z)
       i j  mul (α i j) z)
       i j  mul (β i j) z) i j k

By elimination into sets we can prove that mul is also unital on the right. For the base case this is once again definitional, and for the path case we’re left with filling a degenerate square which is path in one direction.

    mul-idr :  x  mul x base  x
    mul-idr = Deloop-elim-set G _  _  hlevel 2) refl  z i j  path z i)

Finally, for invertibility, it suffices to check mul is an equivalence at the basepoint, in which case our proof above reduces this to showing the identity function is an equivalence.

  HSpace-BG : HSpace (Deloop∙ G)
  HSpace-BG .μ      = mul
  HSpace-BG .idl x  = refl
  HSpace-BG .idr    = mul-idr
  HSpace-BG .id-coh = refl
  HSpace-BG .μ-invl = Deloop-elim-prop _ _  _  hlevel 1)
    id-equiv
  HSpace-BG .μ-invr = Deloop-elim-prop _ _  _  hlevel 1)
    (subst is-equiv (ext (sym  mul-idr)) id-equiv)

On the circle🔗

We can specialise the discussion above to the circle, in which case we already have many of the components we need. Note that always-loop gives us, for every point a loop at but loops are nothing but maps from so we get a “multiplication” on the circle. We also define the “inverse” map on 1

mulS¹ :     
mulS¹ base     y = y
mulS¹ (loop i) y = always-loop y i

invS¹ :   
invS¹ base     = base
invS¹ (loop i) = loop (~ i)
mulS¹-idr :  x  mulS¹ x base  x
mulS¹-idr = S¹-elim refl  i j  loop i)

mulS¹-comm :  x y  mulS¹ x y  mulS¹ y x
mulS¹-comm = S¹-elim  y  sym (mulS¹-idr y)) (funextP (S¹-elim  i j  loop i) prop!))

mulS¹-invl :  x  mulS¹ (invS¹ x) x  base
mulS¹-invl = S¹-elim refl λ i j  hcomp {A = } ( i   j) λ where
  k (k = i0)  base
  k (i = i0)  base
  k (i = i1)  base
  k (j = i0)  hfill ( i) k  { k (k = i0)  base ; k (i = i0)  loop (~ i  k) ; k (i = i1)  loop (~ i  k) })
  k (j = i1)  base

mulS¹-invr :  x  mulS¹ x (invS¹ x)  base
mulS¹-invr x = mulS¹-comm x (invS¹ x)  mulS¹-invl x

mulS¹-assoc :  x y z  mulS¹ x (mulS¹ y z)  mulS¹ (mulS¹ x y) z
mulS¹-assoc = S¹-elim  y z  refl) (funextP (S¹-elim (funextP (S¹-elim  i j  loop i) prop!)) prop!))

HSpace-S¹ : HSpace ( , base)
HSpace-S¹ .μ      = mulS¹
HSpace-S¹ .idl x  = refl
HSpace-S¹ .idr    = mulS¹-idr
HSpace-S¹ .id-coh = refl
HSpace-S¹ .μ-invr x =
  is-iso→is-equiv λ where
    .is-iso.from y  mulS¹ (invS¹ x) y
    .is-iso.rinv y  ap₂ mulS¹ (mulS¹-comm (invS¹ x) y) refl  sym (mulS¹-assoc y (invS¹ x) x)  ap (mulS¹ y) (mulS¹-invl x)  mulS¹-idr y
    .is-iso.linv y  ap (mulS¹ (invS¹ x)) (mulS¹-comm y x)  mulS¹-assoc (invS¹ x) x y  ap (flip mulS¹ y) (mulS¹-invl x)
HSpace-S¹ .μ-invl x = is-iso→is-equiv λ where
  .is-iso.from y  mulS¹ (invS¹ x) y
  .is-iso.rinv y  mulS¹-assoc x (invS¹ x) y  ap (flip mulS¹ y) (mulS¹-invr x)
  .is-iso.linv y  mulS¹-assoc (invS¹ x) x y  ap (flip mulS¹ y) (mulS¹-invl x)

  1. If one thinks of the circle as the set of unit complex numbers with base point it is useful to think of mulS¹ as complex multiplication and of invS¹ as complex conjugation.↩︎