module Algebra.Group.Instances.Symmetric where

# Symmetric groupsπ

If
$X$
is a set, then the type of all bijections
$XβX$
is also a set, and it forms the carrier for a group: The *symmetric group*
on
$X.$

Sym : β {β} (X : Set β) β Group-on (β£ X β£ β β£ X β£) Sym X = to-group-on group-str where open make-group group-str : make-group (β£ X β£ β β£ X β£) group-str .mul g f = f βe g

The group operation is `composition of equivalences`

;
The identity element is `the identity equivalence`

.

group-str .unit = id , id-equiv

This type is a set because
$XβX$
is a set (because
$X$
is a set by assumption), and `being an equivalence is a proposition`

.

group-str .group-is-set = hlevel 2

The associativity and identity laws hold definitionally.

group-str .assoc _ _ _ = trivial! group-str .idl _ = trivial!

The inverse is given by `the inverse equivalence`

,
and the inverse equations hold by the fact that the inverse of an
equivalence is both a section and a retraction.

group-str .inv = _eβ»ΒΉ group-str .invl (f , eqv) = ext (equivβunit eqv)

We write $S_{n}$ for the symmetric group on the standard finite set with $n$ elements.

S : Nat β Group lzero S n = el! (Fin n β Fin n) , Sym (el! (Fin n))