Free higher group actions

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-10.
Last modified on 2023-11-24.

module where
open import foundation.embeddings
open import foundation.identity-types
open import foundation.propositional-maps
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.regensburg-extension-fundamental-theorem-of-identity-types
open import foundation.sets
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.truncation-levels
open import foundation.universe-levels

open import higher-group-theory.higher-group-actions
open import higher-group-theory.higher-groups
open import higher-group-theory.orbits-higher-group-actions


Consider an ∞-group G and an ∞-group action of G on X. We say that X is free if its type of orbits is a set.

Equivalently, we say that X is abstractly free if for any element x : X (sh G) of the underlying type of X the action map

  g ↦ mul-action-∞-Group G X g x

is an embedding. The equivalence of these two conditions is established via the Regensburg extension of the fundamental theorem of identity types.


The predicate of being a free group action

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

  is-free-prop-action-∞-Group : Prop (l1  l2)
  is-free-prop-action-∞-Group = is-set-Prop (orbit-action-∞-Group G X)

  is-free-action-∞-Group : UU (l1  l2)
  is-free-action-∞-Group = type-Prop is-free-prop-action-∞-Group

  is-prop-is-free-action-∞-Group : is-prop is-free-action-∞-Group
  is-prop-is-free-action-∞-Group = is-prop-type-Prop is-free-prop-action-∞-Group

The predicate of being an abstractly free ∞-group action

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

  is-abstractly-free-prop-action-∞-Group : Prop (l1  l2)
  is-abstractly-free-prop-action-∞-Group =
      ( type-action-∞-Group G X)
      ( λ x  is-emb-Prop  g  mul-action-∞-Group G X g x))

  is-abstractly-free-action-∞-Group : UU (l1  l2)
  is-abstractly-free-action-∞-Group =
    type-Prop is-abstractly-free-prop-action-∞-Group

  is-prop-is-abstractly-free-action-∞-Group :
    is-prop is-abstractly-free-action-∞-Group
  is-prop-is-abstractly-free-action-∞-Group =
    is-prop-type-Prop is-abstractly-free-prop-action-∞-Group

Free group actions

free-action-∞-Group :
  {l1 : Level} (l2 : Level)  ∞-Group l1  UU (l1  lsuc l2)
free-action-∞-Group l2 G =
  type-subtype (is-free-prop-action-∞-Group {l2 = l2} G)


Any transport function of an abstractly free higher group action is an embedding

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

    is-emb-tr-is-abstractly-free-action-∞-Group :
      is-abstractly-free-action-∞-Group G X 
      (u : classifying-type-∞-Group G)
      (x : type-action-∞-Group G X) 
      is-emb  (p : shape-∞-Group G  u)  tr X p x)
    is-emb-tr-is-abstractly-free-action-∞-Group H u x =
        ( mere-eq-classifying-type-∞-Group G (shape-∞-Group G) u)
        ( is-emb-Prop _)
        ( λ where refl  H x)

A higher group action X is free if and only if it is abstractly free

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

    is-free-is-abstractly-free-action-∞-Group :
      is-abstractly-free-action-∞-Group G X 
      is-free-action-∞-Group G X
    is-free-is-abstractly-free-action-∞-Group H =
        ( neg-one-𝕋)
        ( shape-∞-Group G)
        ( is-0-connected-classifying-type-∞-Group G)
        ( λ f u 
            ( is-emb-htpy
              ( compute-map-out-of-identity-type f u)
              ( is-emb-tr-is-abstractly-free-action-∞-Group G X H u
                ( f (shape-∞-Group G) (unit-∞-Group G)))))

    is-abstractly-free-is-free-action-∞-Group :
      is-free-action-∞-Group G X 
      is-abstractly-free-action-∞-Group G X
    is-abstractly-free-is-free-action-∞-Group H x =
        ( backward-implication-extended-fundamental-theorem-id-truncated
          ( neg-one-𝕋)
          ( shape-∞-Group G)
          ( H)
          ( λ u p  tr X p x)
          ( shape-∞-Group G))

Recent changes