# Library Exercise_3_2_1_7

Require Import Utf8.
Require Import FunctionalExtensionality.
Require Import Common Isomorphism Monoid Group.

Set Implicit Arguments.

Generalizable All Variables.

# Exercise 3.2.1.7

Section Exercise_3_2_1_7.

## Problem

Let S be a finite set. A permutation of S is an isomorphism f : S S
a.) Come up with an identity, and a multiplication formula, such that the set of permutations of S forms a monoid.
b.) Is it a group?

Variable S : Type.

Definition ComputationalMonoidOfAutomorphisms : ComputationalMonoid (S S)
:= {| id := isomorphic_reflexive S;
comp := (fun x y @isomorphic_transitive S S S y x) |}.

Instance Exercise_3_2_1_7_is_monoid : IsMonoid ComputationalMonoidOfAutomorphisms.
Proof.
esplit; unfold monoid_obj; simpl;
repeat intros [? [? ? ?]]; simpl in *;
apply isomorphic_eq; expand; trivial.
Qed.

Definition ComputationalGroupOfAutomorphisms : ComputationalGroup (S S)
:= {| group_monoid := ComputationalMonoidOfAutomorphisms;
group_inverse := @isomorphic_symmetric S S |}.

Instance Exercise_3_2_1_7_is_group : IsGroup ComputationalGroupOfAutomorphisms.
Proof.
repeat (intros [? [? ? ?]] || split);
unfold monoid_obj; simpl in *;
try apply isomorphic_eq;
try (apply functional_extensionality_dep; intro);
expand; trivial.
Qed.
End Exercise_3_2_1_7.