Symmetric groups

module group-theory.symmetric-groups where
Imports
open import foundation.automorphisms
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.functions
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import group-theory.concrete-groups
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.homomorphisms-semigroups
open import group-theory.isomorphisms-groups
open import group-theory.monoids
open import group-theory.opposite-groups
open import group-theory.semigroups
open import group-theory.symmetric-concrete-groups

Definitions

set-symmetric-Group : {l : Level} (X : Set l)  Set l
set-symmetric-Group X = Aut-Set X

type-symmetric-Group : {l : Level} (X : Set l)  UU l
type-symmetric-Group X = type-Set (set-symmetric-Group X)

is-set-type-symmetric-Group :
  {l : Level} (X : Set l)  is-set (type-symmetric-Group X)
is-set-type-symmetric-Group X = is-set-type-Set (set-symmetric-Group X)

has-associative-mul-aut-Set :
  {l : Level} (X : Set l)  has-associative-mul-Set (Aut-Set X)
pr1 (has-associative-mul-aut-Set X) f e = f ∘e e
pr2 (has-associative-mul-aut-Set X) e f g = associative-comp-equiv g f e

symmetric-Semigroup :
  {l : Level} (X : Set l)  Semigroup l
pr1 (symmetric-Semigroup X) = set-symmetric-Group X
pr2 (symmetric-Semigroup X) = has-associative-mul-aut-Set X

is-unital-Semigroup-symmetric-Semigroup :
  {l : Level} (X : Set l)  is-unital-Semigroup (symmetric-Semigroup X)
pr1 (is-unital-Semigroup-symmetric-Semigroup X) = id-equiv
pr1 (pr2 (is-unital-Semigroup-symmetric-Semigroup X)) = left-unit-law-equiv
pr2 (pr2 (is-unital-Semigroup-symmetric-Semigroup X)) = right-unit-law-equiv

is-group-symmetric-Semigroup' :
  {l : Level} (X : Set l) 
  is-group' (symmetric-Semigroup X) (is-unital-Semigroup-symmetric-Semigroup X)
pr1 (is-group-symmetric-Semigroup' X) = inv-equiv
pr1 (pr2 (is-group-symmetric-Semigroup' X)) = left-inverse-law-equiv
pr2 (pr2 (is-group-symmetric-Semigroup' X)) = right-inverse-law-equiv

symmetric-Group :
  {l : Level}  Set l  Group l
pr1 (symmetric-Group X) = symmetric-Semigroup X
pr1 (pr2 (symmetric-Group X)) = is-unital-Semigroup-symmetric-Semigroup X
pr2 (pr2 (symmetric-Group X)) = is-group-symmetric-Semigroup' X

Properties

If two sets are equivalent, then their symmetric groups are isomorphic

module _
  {l1 l2 : Level} (X : Set l1) (Y : Set l2) (e : type-Set X  type-Set Y)
  where

  hom-symmetric-group-equiv-Set :
    type-hom-Group (symmetric-Group X) (symmetric-Group Y)
  pr1 hom-symmetric-group-equiv-Set f = e ∘e (f ∘e inv-equiv e)
  pr2 hom-symmetric-group-equiv-Set f g =
    ( eq-equiv-eq-map-equiv refl) 
      ( ( ap
        ( λ h  e ∘e (( f ∘e (h ∘e g)) ∘e inv-equiv e))
        ( inv (left-inverse-law-equiv e))) 
        ( eq-equiv-eq-map-equiv refl))

  hom-inv-symmetric-group-equiv-Set :
    type-hom-Group (symmetric-Group Y) (symmetric-Group X)
  pr1 hom-inv-symmetric-group-equiv-Set f = inv-equiv e ∘e (f ∘e e)
  pr2 hom-inv-symmetric-group-equiv-Set f g =
    ( eq-equiv-eq-map-equiv refl) 
      ( ( ap
        ( λ h  inv-equiv e ∘e (( f ∘e (h ∘e g)) ∘e e))
        ( inv (right-inverse-law-equiv e))) 
        ( eq-equiv-eq-map-equiv refl))

  is-sec-hom-inv-symmetric-group-equiv-Set :
    Id
      ( comp-hom-Group
        ( symmetric-Group Y)
        ( symmetric-Group X)
        ( symmetric-Group Y)
        ( hom-symmetric-group-equiv-Set)
        ( hom-inv-symmetric-group-equiv-Set))
      ( id-hom-Group (symmetric-Group Y))
  is-sec-hom-inv-symmetric-group-equiv-Set =
    eq-pair-Σ
      ( eq-htpy
        ( λ f 
          ( eq-equiv-eq-map-equiv refl) 
            ( ( ap  h  h ∘e (f ∘e h)) (right-inverse-law-equiv e)) 
              ( eq-equiv-eq-map-equiv refl))))
      ( eq-is-prop
        ( is-prop-preserves-mul-Semigroup
          ( semigroup-Group (symmetric-Group Y))
          ( semigroup-Group (symmetric-Group Y))
          ( id)))

  is-retr-hom-inv-symmetric-group-equiv-Set :
    Id
      ( comp-hom-Group
        ( symmetric-Group X)
        ( symmetric-Group Y)
        ( symmetric-Group X)
        ( hom-inv-symmetric-group-equiv-Set)
        ( hom-symmetric-group-equiv-Set))
      ( id-hom-Group (symmetric-Group X))
  is-retr-hom-inv-symmetric-group-equiv-Set =
    eq-pair-Σ
      ( eq-htpy
        ( λ f 
          ( eq-equiv-eq-map-equiv refl) 
            ( ( ap  h  h ∘e (f ∘e h)) (left-inverse-law-equiv e)) 
              ( eq-equiv-eq-map-equiv refl))))
      ( eq-is-prop
        ( is-prop-preserves-mul-Semigroup
          ( semigroup-Group (symmetric-Group X))
          ( semigroup-Group (symmetric-Group X))
          ( id)))

  iso-symmetric-group-equiv-Set :
    type-iso-Group (symmetric-Group X) (symmetric-Group Y)
  pr1 iso-symmetric-group-equiv-Set = hom-symmetric-group-equiv-Set
  pr1 (pr2 iso-symmetric-group-equiv-Set) = hom-inv-symmetric-group-equiv-Set
  pr1 (pr2 (pr2 iso-symmetric-group-equiv-Set)) =
    is-sec-hom-inv-symmetric-group-equiv-Set
  pr2 (pr2 (pr2 iso-symmetric-group-equiv-Set)) =
    is-retr-hom-inv-symmetric-group-equiv-Set

The symmetric group and the abstract automorphism group of a set are isomorphic

module _
  {l1 : Level} (A : Set l1)
  where

  equiv-compute-symmetric-Concrete-Group :
    type-Concrete-Group (symmetric-Concrete-Group A)  type-symmetric-Group A
  equiv-compute-symmetric-Concrete-Group =
    extensionality-classifying-type-symmetric-Concrete-Group A
      ( shape-symmetric-Concrete-Group A)
      ( shape-symmetric-Concrete-Group A)

  map-compute-symmetric-Concrete-Group :
    type-Concrete-Group (symmetric-Concrete-Group A)  type-symmetric-Group A
  map-compute-symmetric-Concrete-Group =
    equiv-eq-classifying-type-symmetric-Concrete-Group A
      ( shape-symmetric-Concrete-Group A)
      ( shape-symmetric-Concrete-Group A)

  preserves-mul-compute-symmetric-Concrete-Group :
    preserves-mul-Group
      ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A))
      ( symmetric-Group A)
      ( map-compute-symmetric-Concrete-Group)
  preserves-mul-compute-symmetric-Concrete-Group =
    preserves-mul-equiv-eq-classifying-type-symmetric-Concrete-Group A
      ( shape-symmetric-Concrete-Group A)
      ( shape-symmetric-Concrete-Group A)
      ( shape-symmetric-Concrete-Group A)

  equiv-group-compute-symmetric-Concrete-Group :
    equiv-Group
      ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A))
      ( symmetric-Group A)
  pr1 equiv-group-compute-symmetric-Concrete-Group =
    equiv-compute-symmetric-Concrete-Group
  pr2 equiv-group-compute-symmetric-Concrete-Group =
    preserves-mul-compute-symmetric-Concrete-Group

  compute-symmetric-Concrete-Group' :
    type-iso-Group
      ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A))
      ( symmetric-Group A)
  compute-symmetric-Concrete-Group' =
    iso-equiv-Group
      ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A))
      ( symmetric-Group A)
      ( equiv-group-compute-symmetric-Concrete-Group)

  compute-symmetric-Concrete-Group :
    type-iso-Group
      ( abstract-group-Concrete-Group (symmetric-Concrete-Group A))
      ( symmetric-Group A)
  compute-symmetric-Concrete-Group =
    comp-iso-Group
      ( abstract-group-Concrete-Group (symmetric-Concrete-Group A))
      ( op-abstract-group-Concrete-Group (symmetric-Concrete-Group A))
      ( symmetric-Group A)
      ( compute-symmetric-Concrete-Group')
      ( iso-inv-Group
        ( abstract-group-Concrete-Group (symmetric-Concrete-Group A)))