Equivalences of concrete group actions

Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.

Created on 2022-07-10.
Last modified on 2024-01-31.

module group-theory.equivalences-concrete-group-actions where
Imports 
open import foundation.1-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.torsorial-type-families
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) → 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 → 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-torsorial-equiv-action-Concrete-Group :
    is-torsorial equiv-action-Concrete-Group
  is-torsorial-equiv-action-Concrete-Group =
    is-torsorial-Eq-Π (λ u → is-torsorial-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-prop-equiv-action-Concrete-Group :
    (e f : equiv-action-Concrete-Group G X Y) → Prop (l2 ⊔ l3)
  pr1 (htpy-prop-equiv-action-Concrete-Group e f) =
    htpy-equiv-action-Concrete-Group G X Y e f
  pr2 (htpy-prop-equiv-action-Concrete-Group 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)

Recent changes