Isomorphisms of group actions

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

Created on 2022-03-17.
Last modified on 2024-04-11.

module group-theory.isomorphisms-group-actions where
Imports 
open import category-theory.isomorphisms-in-large-precategories

open import foundation.commuting-squares-of-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.propositions
open import foundation.subtypes
open import foundation.torsorial-type-families
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.universe-levels

open import group-theory.equivalences-group-actions
open import group-theory.group-actions
open import group-theory.groups
open import group-theory.homomorphisms-group-actions
open import group-theory.precategory-of-group-actions

Definitions

The predicate of being an isomorphism of group actions

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

  is-iso-action-Group :
    (f : hom-action-Group G X Y) → UU (l1 ⊔ l2 ⊔ l3)
  is-iso-action-Group =
    is-iso-Large-Precategory (action-Group-Large-Precategory G) {X = X} {Y = Y}

module _
  {l1 l2 l3 : Level} (G : Group l1)
  (X : action-Group G l2) (Y : action-Group G l3)
  (f : hom-action-Group G X Y) (is-iso-f : is-iso-action-Group G X Y f)
  where

  hom-inv-is-iso-action-Group : hom-action-Group G Y X
  hom-inv-is-iso-action-Group =
    hom-inv-is-iso-Large-Precategory
      ( action-Group-Large-Precategory G) {X = X} {Y = Y} f is-iso-f

  map-hom-inv-is-iso-action-Group :
    type-action-Group G Y → type-action-Group G X
  map-hom-inv-is-iso-action-Group =
    map-hom-action-Group G Y X hom-inv-is-iso-action-Group

  is-section-hom-inv-is-iso-action-Group :
    ( comp-hom-action-Group G Y X Y f hom-inv-is-iso-action-Group) ＝
    ( id-hom-action-Group G Y)
  is-section-hom-inv-is-iso-action-Group =
    is-section-hom-inv-is-iso-Large-Precategory
      ( action-Group-Large-Precategory G) {X = X} {Y = Y} f is-iso-f

  is-retraction-hom-inv-is-iso-action-Group :
    ( comp-hom-action-Group G X Y X hom-inv-is-iso-action-Group f) ＝
    ( id-hom-action-Group G X)
  is-retraction-hom-inv-is-iso-action-Group =
    is-retraction-hom-inv-is-iso-Large-Precategory
      ( action-Group-Large-Precategory G) {X = X} {Y = Y} f is-iso-f

The type of isomorphisms of group actions

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

  iso-action-Group : UU (l1 ⊔ l2 ⊔ l3)
  iso-action-Group =
    iso-Large-Precategory (action-Group-Large-Precategory G) X Y

  hom-iso-action-Group :
    iso-action-Group → hom-action-Group G X Y
  hom-iso-action-Group =
    hom-iso-Large-Precategory (action-Group-Large-Precategory G) {X = X} {Y = Y}

  map-iso-action-Group :
    iso-action-Group →
    type-action-Group G X → type-action-Group G Y
  map-iso-action-Group f =
    map-hom-action-Group G X Y (hom-iso-action-Group f)

  preserves-action-iso-action-Group :
    (f : iso-action-Group) (g : type-Group G) →
    coherence-square-maps
      ( map-iso-action-Group f)
      ( mul-action-Group G X g)
      ( mul-action-Group G Y g)
      ( map-iso-action-Group f)
  preserves-action-iso-action-Group f =
    preserves-action-hom-action-Group G X Y (hom-iso-action-Group f)

  hom-inv-iso-action-Group :
    iso-action-Group → hom-action-Group G Y X
  hom-inv-iso-action-Group =
    hom-inv-iso-Large-Precategory
      ( action-Group-Large-Precategory G) {X = X} {Y = Y}

  map-hom-inv-iso-action-Group :
    iso-action-Group →
    type-action-Group G Y → type-action-Group G X
  map-hom-inv-iso-action-Group f =
    map-hom-action-Group G Y X (hom-inv-iso-action-Group f)

  is-section-hom-inv-iso-action-Group :
    (f : iso-action-Group) →
    ( comp-hom-action-Group G Y X Y
      ( hom-iso-action-Group f)
      ( hom-inv-iso-action-Group f)) ＝
    ( id-hom-action-Group G Y)
  is-section-hom-inv-iso-action-Group =
    is-section-hom-inv-iso-Large-Precategory
      ( action-Group-Large-Precategory G) {X = X} {Y = Y}

  is-retraction-hom-inv-iso-action-Group :
    (f : iso-action-Group) →
    ( comp-hom-action-Group G X Y X
      ( hom-inv-iso-action-Group f)
      ( hom-iso-action-Group f)) ＝
    ( id-hom-action-Group G X)
  is-retraction-hom-inv-iso-action-Group =
    is-retraction-hom-inv-iso-Large-Precategory
      ( action-Group-Large-Precategory G) {X = X} {Y = Y}

  is-iso-iso-action-Group :
    (f : iso-action-Group) → is-iso-action-Group G X Y (hom-iso-action-Group f)
  is-iso-iso-action-Group =
    is-iso-iso-Large-Precategory
      ( action-Group-Large-Precategory G) {X = X} {Y = Y}

Properties

Isomorphisms of group actions are equivalent to equivalences of group actions

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

  is-equiv-hom-is-iso-action-Group :
    is-iso-action-Group G X Y f → is-equiv-hom-action-Group G X Y f
  is-equiv-hom-is-iso-action-Group is-iso-f =
    is-equiv-is-invertible
      ( map-hom-inv-is-iso-action-Group G X Y f is-iso-f)
      ( htpy-eq-hom-action-Group G Y Y
        ( comp-hom-action-Group G Y X Y
          ( f)
          ( hom-inv-is-iso-action-Group G X Y f is-iso-f))
        ( id-hom-action-Group G Y)
        ( is-section-hom-inv-is-iso-action-Group G X Y f is-iso-f))
      ( htpy-eq-hom-action-Group G X X
        ( comp-hom-action-Group G X Y X
          ( hom-inv-is-iso-action-Group G X Y f is-iso-f)
          ( f))
        ( id-hom-action-Group G X)
        ( is-retraction-hom-inv-is-iso-action-Group G X Y f is-iso-f))

  is-iso-is-equiv-hom-action-Group :
    is-equiv-hom-action-Group G X Y f → is-iso-action-Group G X Y f
  pr1 (pr1 (is-iso-is-equiv-hom-action-Group is-equiv-f)) =
    map-inv-is-equiv is-equiv-f
  pr2 (pr1 (is-iso-is-equiv-hom-action-Group is-equiv-f)) =
    preserves-action-map-inv-is-equiv-hom-action-Group G X Y f is-equiv-f
  pr1 (pr2 (is-iso-is-equiv-hom-action-Group is-equiv-f)) =
    eq-type-subtype
      ( preserves-action-prop-Group G Y Y)
      ( eq-htpy (is-section-map-inv-is-equiv is-equiv-f))
  pr2 (pr2 (is-iso-is-equiv-hom-action-Group is-equiv-f)) =
    eq-type-subtype
      ( preserves-action-prop-Group G X X)
      ( eq-htpy (is-retraction-map-inv-is-equiv is-equiv-f))

  is-equiv-is-equiv-hom-is-iso-action-Group :
    is-equiv is-equiv-hom-is-iso-action-Group
  is-equiv-is-equiv-hom-is-iso-action-Group =
    is-equiv-has-converse-is-prop
      ( is-prop-is-iso-Large-Precategory
        ( action-Group-Large-Precategory G) {X = X} {Y = Y} f)
      ( is-property-is-equiv (map-hom-action-Group G X Y f))
      ( is-iso-is-equiv-hom-action-Group)

  is-equiv-is-iso-is-equiv-hom-action-Group :
    is-equiv is-iso-is-equiv-hom-action-Group
  is-equiv-is-iso-is-equiv-hom-action-Group =
    is-equiv-has-converse-is-prop
      ( is-property-is-equiv (map-hom-action-Group G X Y f))
      ( is-prop-is-iso-Large-Precategory
        ( action-Group-Large-Precategory G) {X = X} {Y = Y} f)
      ( is-equiv-hom-is-iso-action-Group)

  equiv-is-equiv-hom-is-iso-action-Group :
    is-iso-action-Group G X Y f ≃ is-equiv-hom-action-Group G X Y f
  pr1 equiv-is-equiv-hom-is-iso-action-Group =
    is-equiv-hom-is-iso-action-Group
  pr2 equiv-is-equiv-hom-is-iso-action-Group =
    is-equiv-is-equiv-hom-is-iso-action-Group

  equiv-is-iso-is-equiv-hom-action-Group :
    is-equiv-hom-action-Group G X Y f ≃ is-iso-action-Group G X Y f
  pr1 equiv-is-iso-is-equiv-hom-action-Group =
    is-iso-is-equiv-hom-action-Group
  pr2 equiv-is-iso-is-equiv-hom-action-Group =
    is-equiv-is-iso-is-equiv-hom-action-Group

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

  is-equiv-map-iso-action-Group : is-equiv (map-iso-action-Group G X Y f)
  is-equiv-map-iso-action-Group =
    is-equiv-hom-is-iso-action-Group G X Y
      ( hom-iso-action-Group G X Y f)
      ( is-iso-iso-action-Group G X Y f)

  equiv-iso-action-Group : equiv-action-Group G X Y
  pr1 (pr1 equiv-iso-action-Group) = map-iso-action-Group G X Y f
  pr2 (pr1 equiv-iso-action-Group) = is-equiv-map-iso-action-Group
  pr2 equiv-iso-action-Group = preserves-action-iso-action-Group G X Y f

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

  equiv-equiv-iso-action-Group :
    iso-action-Group G X Y ≃ equiv-action-Group G X Y
  equiv-equiv-iso-action-Group =
    equiv-right-swap-Σ ∘e
    equiv-tot (equiv-is-equiv-hom-is-iso-action-Group G X Y)

  equiv-iso-equiv-action-Group :
    equiv-action-Group G X Y ≃ iso-action-Group G X Y
  equiv-iso-equiv-action-Group =
    equiv-tot (equiv-is-iso-is-equiv-hom-action-Group G X Y) ∘e
    equiv-right-swap-Σ

Isomorphisms characterize equality of G-sets

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

  is-torsorial-iso-action-Group : is-torsorial (iso-action-Group {l3 = l2} G X)
  is-torsorial-iso-action-Group =
    is-contr-equiv
      ( Σ (action-Group G l2) (equiv-action-Group G X))
      ( equiv-tot (equiv-equiv-iso-action-Group G X))
      ( is-torsorial-equiv-action-Group G X)

Recent changes