Subgroups of higher groups

module higher-group-theory.subgroups-higher-groups where
Imports 
open import foundation.0-connected-types
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.functions
open import foundation.sets
open import foundation.universe-levels

open import higher-group-theory.higher-groups

open import structured-types.pointed-types

Idea

A subgroup of a higher group is a pointed set bundle over its classifying type with connected total space.

Definition

subgroup-action-∞-Group :
  {l1 : Level} (l2 : Level) (G : ∞-Group l1) →
  classifying-type-∞-Group G → UU (l1 ⊔ lsuc l2)
subgroup-action-∞-Group l2 G u =
  Σ ( classifying-type-∞-Group G → Set l2)
    ( λ X →
      ( type-Set (X u)) ×
      ( is-0-connected (Σ (classifying-type-∞-Group G) (type-Set ∘ X))))

subgroup-∞-Group :
  {l1 : Level} (l2 : Level) (G : ∞-Group l1) → UU (l1 ⊔ lsuc l2)
subgroup-∞-Group l2 G = subgroup-action-∞-Group l2 G (shape-∞-Group G)

module _
  {l1 l2 : Level} (G : ∞-Group l1) (H : subgroup-∞-Group l2 G)
  where

  set-action-subgroup-∞-Group :
    classifying-type-∞-Group G → Set l2
  set-action-subgroup-∞-Group = pr1 H

  action-subgroup-∞-Group : classifying-type-∞-Group G → UU l2
  action-subgroup-∞-Group = type-Set ∘ set-action-subgroup-∞-Group

  classifying-type-subgroup-∞-Group : UU (l1 ⊔ l2)
  classifying-type-subgroup-∞-Group =
    Σ (classifying-type-∞-Group G) action-subgroup-∞-Group

  shape-subgroup-∞-Group : classifying-type-subgroup-∞-Group
  pr1 shape-subgroup-∞-Group = shape-∞-Group G
  pr2 shape-subgroup-∞-Group = pr1 (pr2 H)

  classifying-pointed-type-subgroup-∞-Group : Pointed-Type (l1 ⊔ l2)
  pr1 classifying-pointed-type-subgroup-∞-Group =
    classifying-type-subgroup-∞-Group
  pr2 classifying-pointed-type-subgroup-∞-Group =
    shape-subgroup-∞-Group

  is-connected-classifying-type-subgroup-∞-Group :
    is-0-connected classifying-type-subgroup-∞-Group
  is-connected-classifying-type-subgroup-∞-Group = pr2 (pr2 H)

  ∞-group-subgroup-∞-Group : ∞-Group (l1 ⊔ l2)
  pr1 ∞-group-subgroup-∞-Group = classifying-pointed-type-subgroup-∞-Group
  pr2 ∞-group-subgroup-∞-Group = is-connected-classifying-type-subgroup-∞-Group