# Symmetric groups

Content created by Egbert Rijke, Fredrik Bakke, Eléonore Mangel, Jonathan Prieto-Cubides, Elisabeth Stenholm and favonia.

Created on 2022-03-17.

module group-theory.symmetric-groups where

Imports
open import foundation.action-on-identifications-functions
open import foundation.automorphisms
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.sets
open import foundation.subtypes
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-is-unital-Semigroup
( 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 :
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 :
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-section-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-section-hom-inv-symmetric-group-equiv-Set =
eq-type-subtype
( preserves-mul-prop-Semigroup
( semigroup-Group (symmetric-Group Y))
( semigroup-Group (symmetric-Group Y)))
( 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)))

is-retraction-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-retraction-hom-inv-symmetric-group-equiv-Set =
eq-type-subtype
( preserves-mul-prop-Semigroup
( semigroup-Group (symmetric-Group X))
( semigroup-Group (symmetric-Group X)))
( 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)))

iso-symmetric-group-equiv-Set :
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-section-hom-inv-symmetric-group-equiv-Set
pr2 (pr2 (pr2 iso-symmetric-group-equiv-Set)) =
is-retraction-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-group-Concrete-Group (symmetric-Concrete-Group A))
( symmetric-Group A)
( map-compute-symmetric-Concrete-Group)
preserves-mul-compute-symmetric-Concrete-Group {x} {y} =
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)
( x)
( y)

equiv-group-compute-symmetric-Concrete-Group :
equiv-Group
( op-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 {x} {y} =
preserves-mul-compute-symmetric-Concrete-Group {x} {y}

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

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