Small ∞-groups

Content created by Egbert Rijke.

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

module higher-group-theory.small-higher-groups where
open import foundation.0-connected-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.identity-types
open import foundation.images
open import foundation.locally-small-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.replacement
open import foundation.small-types
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.unit-type
open import foundation.universe-levels

open import higher-group-theory.equivalences-higher-groups
open import higher-group-theory.higher-groups

open import structured-types.pointed-equivalences
open import structured-types.pointed-types
open import structured-types.small-pointed-types


An ∞-group G is said to be small with respect to a universe 𝒰 if its underlying type is 𝒰-small. By the type theoretic replacement principle it follows that G is small if and only if its classifying type BG is small. This observation implies that an ∞-group G is small if and only if it is structurally small in the sense that it comes equipped with an element of type

  Σ (H : ∞-Group), G ≃ H,

where the type G ≃ H is the type of equivalences of ∞-groups.

Finally, we also introduce the notion of pointed small ∞-group. An ∞-group G is said to be pointed small if its classifying pointed type BG is pointed small.


The predicate of being a small ∞-group

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

  is-small-prop-∞-Group : Prop (l1  lsuc l2)
  is-small-prop-∞-Group = is-small-Prop l2 (type-∞-Group G)

  is-small-∞-Group : UU (l1  lsuc l2)
  is-small-∞-Group = is-small l2 (type-∞-Group G)

  is-prop-is-small-∞-Group : is-prop is-small-∞-Group
  is-prop-is-small-∞-Group = is-prop-is-small l2 (type-∞-Group G)

The predicate of being a structurally small ∞-group

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

  is-structurally-small-∞-Group : UU (l1  lsuc l2)
  is-structurally-small-∞-Group =
    Σ (∞-Group l2) (equiv-∞-Group G)

    is-prop-is-structurally-small-∞-Group :
      is-prop is-structurally-small-∞-Group
    is-prop-is-structurally-small-∞-Group =
        ( equiv-right-swap-Σ)
        ( is-prop-Σ
          ( is-prop-is-pointed-small-Pointed-Type
            ( classifying-pointed-type-∞-Group G))
          ( λ H  is-prop-is-0-connected _))

  is-structurally-small-prop-∞-Group : Prop (l1  lsuc l2)
  pr1 is-structurally-small-prop-∞-Group = is-structurally-small-∞-Group
  pr2 is-structurally-small-prop-∞-Group = is-prop-is-structurally-small-∞-Group

module _
  {l1 l2 : Level} (G : ∞-Group l1) (H : is-structurally-small-∞-Group l2 G)

  ∞-group-is-structurally-small-∞-Group : ∞-Group l2
  ∞-group-is-structurally-small-∞-Group = pr1 H

  type-∞-group-is-structurally-small-∞-Group : UU l2
  type-∞-group-is-structurally-small-∞-Group =
    type-∞-Group ∞-group-is-structurally-small-∞-Group

  equiv-∞-group-is-structurally-small-∞-Group :
    equiv-∞-Group G ∞-group-is-structurally-small-∞-Group
  equiv-∞-group-is-structurally-small-∞-Group = pr2 H

  equiv-is-structurally-small-∞-Group :
    type-∞-Group G  type-∞-group-is-structurally-small-∞-Group
  equiv-is-structurally-small-∞-Group =
    equiv-equiv-∞-Group G
      ( ∞-group-is-structurally-small-∞-Group)
      ( equiv-∞-group-is-structurally-small-∞-Group)

The predicate of being a pointed small ∞-group

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

  is-pointed-small-prop-∞-Group : Prop (l1  lsuc l2)
  is-pointed-small-prop-∞-Group =
    is-pointed-small-prop-Pointed-Type l2 (classifying-pointed-type-∞-Group G)

  is-pointed-small-∞-Group : UU (l1  lsuc l2)
  is-pointed-small-∞-Group =
    is-pointed-small-Pointed-Type l2 (classifying-pointed-type-∞-Group G)

  is-prop-is-pointed-small-∞-Group : is-prop is-pointed-small-∞-Group
  is-prop-is-pointed-small-∞-Group =
    is-prop-is-pointed-small-Pointed-Type (classifying-pointed-type-∞-Group G)


The classifying type of any small ∞-group is locally small

module _
  {l1 l2 : Level} (G : ∞-Group l1) (H : is-small-∞-Group l2 G)

    is-locally-small-classifying-type-is-small-∞-Group' :
      (x y : classifying-type-∞-Group G) 
      shape-∞-Group G  x  shape-∞-Group G  y 
      is-small l2 (x  y)
    is-locally-small-classifying-type-is-small-∞-Group' ._ ._ refl refl = H

    is-locally-small-classifying-type-is-small-∞-Group :
      is-locally-small l2 (classifying-type-∞-Group G)
    is-locally-small-classifying-type-is-small-∞-Group x y =
        ( mere-eq-classifying-type-∞-Group G (shape-∞-Group G) x)
        ( mere-eq-classifying-type-∞-Group G (shape-∞-Group G) y)
        ( is-small-Prop l2 (x  y))
        ( is-locally-small-classifying-type-is-small-∞-Group' x y)

An ∞-group is small if and only if its classifying type is small

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

    is-small-classifying-type-is-small-∞-Group :
      is-small-∞-Group l2 G  is-small l2 (classifying-type-∞-Group G)
    is-small-classifying-type-is-small-∞-Group H =
        ( im (point-∞-Group G))
        ( compute-im-point-∞-Group G)
        ( replacement
          ( point-∞-Group G)
          ( is-small-unit)
          ( is-locally-small-classifying-type-is-small-∞-Group G H))

    is-small-is-small-classifying-type-∞-Group :
      is-small l2 (classifying-type-∞-Group G)  is-small-∞-Group l2 G
    is-small-is-small-classifying-type-∞-Group H =
      is-locally-small-is-small H (shape-∞-Group G) (shape-∞-Group G)

An ∞-group is small if and only if it is pointed small

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

    is-pointed-small-is-small-∞-Group :
      is-small-∞-Group l2 G  is-pointed-small-∞-Group l2 G
    is-pointed-small-is-small-∞-Group H =
        ( classifying-pointed-type-∞-Group G)
        ( is-small-classifying-type-is-small-∞-Group G H)

An ∞-group is small if and only if it is structurally small

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

  classifying-pointed-type-is-small-∞-Group :
    is-small-∞-Group l2 G  Pointed-Type l2
  classifying-pointed-type-is-small-∞-Group H =
      ( classifying-pointed-type-∞-Group G)
      ( is-pointed-small-is-small-∞-Group G H)

  classifying-type-is-small-∞-Group : is-small-∞-Group l2 G  UU l2
  classifying-type-is-small-∞-Group H =
      ( classifying-pointed-type-∞-Group G)
      ( is-pointed-small-is-small-∞-Group G H)

    is-0-connected-classifying-type-is-small-∞-Group :
      (H : is-small-∞-Group l2 G) 
      is-0-connected (classifying-type-is-small-∞-Group H)
    is-0-connected-classifying-type-is-small-∞-Group H =
        ( equiv-is-pointed-small-Pointed-Type
          ( classifying-pointed-type-∞-Group G)
          ( is-pointed-small-is-small-∞-Group G H))
        ( is-0-connected-classifying-type-∞-Group G)

  ∞-group-is-small-∞-Group : is-small-∞-Group l2 G  ∞-Group l2
  pr1 (∞-group-is-small-∞-Group H) =
    classifying-pointed-type-is-small-∞-Group H
  pr2 (∞-group-is-small-∞-Group H) =
    is-0-connected-classifying-type-is-small-∞-Group H

  pointed-type-∞-group-is-small-∞-Group :
    is-small-∞-Group l2 G  Pointed-Type l2
  pointed-type-∞-group-is-small-∞-Group H =
    pointed-type-∞-Group (∞-group-is-small-∞-Group H)

  type-∞-group-is-small-∞-Group :
    is-small-∞-Group l2 G  UU l2
  type-∞-group-is-small-∞-Group H =
    type-∞-Group (∞-group-is-small-∞-Group H)

  equiv-∞-group-is-small-∞-Group :
    (H : is-small-∞-Group l2 G)  equiv-∞-Group G (∞-group-is-small-∞-Group H)
  equiv-∞-group-is-small-∞-Group H =
      ( classifying-pointed-type-∞-Group G)
      ( is-pointed-small-is-small-∞-Group G H)

  pointed-equiv-equiv-∞-group-is-small-∞-Group :
    (H : is-small-∞-Group l2 G) 
    pointed-type-∞-Group G ≃∗ pointed-type-∞-group-is-small-∞-Group H
  pointed-equiv-equiv-∞-group-is-small-∞-Group H =
    pointed-equiv-equiv-∞-Group G
      ( ∞-group-is-small-∞-Group H)
      ( equiv-∞-group-is-small-∞-Group H)

  equiv-equiv-∞-group-is-small-∞-Group :
    (H : is-small-∞-Group l2 G) 
    type-∞-Group G  type-∞-group-is-small-∞-Group H
  equiv-equiv-∞-group-is-small-∞-Group H =
    equiv-equiv-∞-Group G
      ( ∞-group-is-small-∞-Group H)
      ( equiv-∞-group-is-small-∞-Group H)

    is-structurally-small-is-small-∞-Group :
      is-small-∞-Group l2 G  is-structurally-small-∞-Group l2 G
    pr1 (is-structurally-small-is-small-∞-Group H) =
      ∞-group-is-small-∞-Group H
    pr2 (is-structurally-small-is-small-∞-Group H) =
      equiv-∞-group-is-small-∞-Group H

    is-small-is-structurally-small-∞-Group :
      is-structurally-small-∞-Group l2 G  is-small-∞-Group l2 G
    pr1 (is-small-is-structurally-small-∞-Group H) =
      type-∞-group-is-structurally-small-∞-Group G H
    pr2 (is-small-is-structurally-small-∞-Group H) =
      equiv-is-structurally-small-∞-Group G H

    is-small-∞-group-is-small-∞-Group :
      (H : is-small-∞-Group l2 G) 
      is-small-∞-Group l1 (∞-group-is-small-∞-Group H)
    pr1 (is-small-∞-group-is-small-∞-Group H) = type-∞-Group G
    pr2 (is-small-∞-group-is-small-∞-Group H) =
      inv-equiv (equiv-equiv-∞-group-is-small-∞-Group H)

Recent changes