Deloopable H-spaces

Content created by Egbert Rijke.

Created on 2024-03-23.
Last modified on 2024-03-23.

module higher-group-theory.deloopable-h-spaces where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import higher-group-theory.higher-groups

open import structured-types.equivalences-h-spaces
open import structured-types.h-spaces

Idea

Consider an H-space with underlying pointed type (X , *) and with multiplication μ satisfying

   left-unit-law : (x : X) → μ * x ＝ x
  right-unit-law : (x : X) → μ x * ＝ x
    coh-unit-law : left-unit-law * ＝ right-unit-law *.

A delooping of the H-space X consists of an ∞-group G and an equivalence of H-spaces

  X ≃ h-space-∞-Group G.

Definitions

Deloopings of H-spaces of a given universe level

module _
  {l1 : Level} (l2 : Level) (A : H-Space l1)
  where

  delooping-H-Space-Level : UU (l1 ⊔ lsuc l2)
  delooping-H-Space-Level =
    Σ (∞-Group l2) (λ G → equiv-H-Space A (h-space-∞-Group G))

Deloopings of H-spaces

module _
  {l1 : Level} (A : H-Space l1)
  where

  delooping-H-Space : UU (lsuc l1)
  delooping-H-Space = delooping-H-Space-Level l1 A

See also

Recent changes