Equivalences of concrete group actions

module group-theory.equivalences-concrete-group-actions where
Imports
open import foundation.1-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equality-dependent-function-types
open import foundation.equivalences
open import foundation.functoriality-dependent-function-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.concrete-group-actions
open import group-theory.concrete-groups
open import group-theory.homomorphisms-concrete-group-actions

Idea

An equivalence of concrete group actions from X to Y is a family of equivalences from X u to Y u indexed by u : BG.

Definition

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

  equiv-action-Concrete-Group :
    {l3 : Level} (Y : action-Concrete-Group l3 G)  UU (l1  l2  l3)
  equiv-action-Concrete-Group Y =
    (u : classifying-type-Concrete-Group G)  type-equiv-Set (X u) (Y u)

  id-equiv-action-Concrete-Group : equiv-action-Concrete-Group X
  id-equiv-action-Concrete-Group u = id-equiv

  extensionality-action-Concrete-Group :
    (Y : action-Concrete-Group l2 G)  (X  Y)  equiv-action-Concrete-Group Y
  extensionality-action-Concrete-Group =
    extensionality-Π X
      ( λ u  type-equiv-Set (X u))
      ( λ u  extensionality-Set (X u))

  equiv-eq-action-Concrete-Group :
    (Y : action-Concrete-Group l2 G)  (X  Y)  equiv-action-Concrete-Group Y
  equiv-eq-action-Concrete-Group Y =
    map-equiv (extensionality-action-Concrete-Group Y)

  eq-equiv-action-Concrete-Group :
    (Y : action-Concrete-Group l2 G)  equiv-action-Concrete-Group Y  (X  Y)
  eq-equiv-action-Concrete-Group Y =
    map-inv-equiv (extensionality-action-Concrete-Group Y)

  is-contr-total-equiv-action-Concrete-Group :
    is-contr (Σ (action-Concrete-Group l2 G) equiv-action-Concrete-Group)
  is-contr-total-equiv-action-Concrete-Group =
    is-contr-total-Eq-Π
      ( λ u  type-equiv-Set (X u))
      ( λ u  is-contr-total-equiv-Set (X u))

module _
  {l1 l2 l3 : Level} (G : Concrete-Group l1) (X : action-Concrete-Group l2 G)
  (Y : action-Concrete-Group l3 G)
  where

  emb-hom-equiv-action-Concrete-Group :
    equiv-action-Concrete-Group G X Y  hom-action-Concrete-Group G X Y
  emb-hom-equiv-action-Concrete-Group = emb-Π  u  emb-map-equiv)

  hom-equiv-action-Concrete-Group :
    equiv-action-Concrete-Group G X Y  hom-action-Concrete-Group G X Y
  hom-equiv-action-Concrete-Group = map-emb emb-hom-equiv-action-Concrete-Group

  is-emb-hom-equiv-action-Concrete-Group :
    is-emb hom-equiv-action-Concrete-Group
  is-emb-hom-equiv-action-Concrete-Group =
    is-emb-map-emb emb-hom-equiv-action-Concrete-Group

  map-equiv-action-Concrete-Group :
    equiv-action-Concrete-Group G X Y 
    type-action-Concrete-Group G X  type-action-Concrete-Group G Y
  map-equiv-action-Concrete-Group e =
    map-hom-action-Concrete-Group G X Y (hom-equiv-action-Concrete-Group e)

  preserves-mul-equiv-action-Concrete-Group :
    (e : equiv-action-Concrete-Group G X Y) (g : type-Concrete-Group G)
    (x : type-action-Concrete-Group G X) 
    ( map-equiv-action-Concrete-Group e (mul-action-Concrete-Group G X g x)) 
    ( mul-action-Concrete-Group G Y g (map-equiv-action-Concrete-Group e x))
  preserves-mul-equiv-action-Concrete-Group e =
    preserves-mul-hom-action-Concrete-Group G X Y
      ( hom-equiv-action-Concrete-Group e)

  htpy-equiv-action-Concrete-Group :
    (e f : equiv-action-Concrete-Group G X Y)  UU (l2  l3)
  htpy-equiv-action-Concrete-Group e f =
    htpy-hom-action-Concrete-Group G X Y
      ( hom-equiv-action-Concrete-Group e)
      ( hom-equiv-action-Concrete-Group f)

  extensionality-equiv-action-Concrete-Group :
    (e f : equiv-action-Concrete-Group G X Y) 
    (e  f)  htpy-equiv-action-Concrete-Group e f
  extensionality-equiv-action-Concrete-Group e f =
    ( extensionality-hom-action-Concrete-Group G X Y
      ( hom-equiv-action-Concrete-Group e)
      ( hom-equiv-action-Concrete-Group f)) ∘e
    ( equiv-ap-emb emb-hom-equiv-action-Concrete-Group)

  eq-htpy-equiv-action-Concrete-Group :
    (e f : equiv-action-Concrete-Group G X Y) 
    htpy-equiv-action-Concrete-Group e f  (e  f)
  eq-htpy-equiv-action-Concrete-Group e f =
    map-inv-equiv (extensionality-equiv-action-Concrete-Group e f)

Properties

The type of equivalences between concrete group actions is a set

module _
  {l1 l2 l3 : Level} (G : Concrete-Group l1) (X : action-Concrete-Group l2 G)
  (Y : action-Concrete-Group l3 G)
  where

  is-prop-htpy-equiv-action-Concrete-Group :
    (e f : equiv-action-Concrete-Group G X Y) 
    is-prop (htpy-equiv-action-Concrete-Group G X Y e f)
  is-prop-htpy-equiv-action-Concrete-Group e f =
    is-prop-htpy-hom-action-Concrete-Group G X Y
      ( hom-equiv-action-Concrete-Group G X Y e)
      ( hom-equiv-action-Concrete-Group G X Y f)

  htpy-equiv-action-Concrete-Group-Prop :
    (e f : equiv-action-Concrete-Group G X Y)  Prop (l2  l3)
  pr1 (htpy-equiv-action-Concrete-Group-Prop e f) =
    htpy-equiv-action-Concrete-Group G X Y e f
  pr2 (htpy-equiv-action-Concrete-Group-Prop e f) =
    is-prop-htpy-equiv-action-Concrete-Group e f

  is-set-equiv-action-Concrete-Group :
    is-set (equiv-action-Concrete-Group G X Y)
  is-set-equiv-action-Concrete-Group e f =
    is-prop-equiv
      ( extensionality-equiv-action-Concrete-Group G X Y e f)
      ( is-prop-htpy-equiv-action-Concrete-Group e f)

The type of concrete group actions is a 1-type

is-1-type-action-Concrete-Group :
  {l1 l2 : Level} (G : Concrete-Group l1) 
  is-1-type (action-Concrete-Group l2 G)
is-1-type-action-Concrete-Group G X Y =
  is-set-equiv
    ( equiv-action-Concrete-Group G X Y)
    ( extensionality-action-Concrete-Group G X Y)
    ( is-set-equiv-action-Concrete-Group G X Y)