Library Exercise_3_2_1_7

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

Set Implicit Arguments.

Generalizable All Variables.


Section Exercise_3_2_1_7.


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.
    esplit; unfold monoid_obj; simpl;
    repeat intros [? [? ? ?]]; simpl in *;
    apply isomorphic_eq; expand; trivial.

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

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