Deloopable groups

Content created by Egbert Rijke.

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

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

open import group-theory.groups

open import higher-group-theory.deloopable-h-spaces

Idea

A delooping of a group G is a delooping of the underlying H-space of G. In other words, a delooping of a group G consists of a higher group H, which is defined to be a pointed connected type, equipped with an equivalence of H-spaces G ≃ h-space-∞-Group H from G to the underlying H-space of H.

Definitions

Deloopings of groups of a given universe level

module _
  {l1 : Level} (l2 : Level) (G : Group l1)
  where

  delooping-Group-Level : UU (l1 ⊔ lsuc l2)
  delooping-Group-Level = delooping-H-Space-Level l2 (h-space-Group G)

Deloopings of groups

module _
  {l1 : Level} (G : Group l1)
  where

  delooping-Group : UU (lsuc l1)
  delooping-Group = delooping-Group-Level l1 G

See also

Recent changes