From Ssreflect Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
From MathComp Require Import path tuple finfun bigop finset binomial fingroup perm.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GroupScope.
(** The set of all permutation of %\lstinline!'I_3!% forms a %\lstinline!finGroupType!%. *)
Goal 'S_3 = {perm 'I_3}. reflexivity. Abort.
Check [finGroupType of 'S_3].
(** We define the basic transpositions. *)
Definition p01 : 'S_3 := tperm ord0 (@Ordinal 3 1 erefl).
Definition p02 : 'S_3 := tperm ord0 (@Ordinal 3 2 erefl).
Definition p12 : 'S_3 := tperm (@Ordinal 3 1 erefl) (@Ordinal 3 2 erefl).
(** We define the permutation $(021)$. ($0 \to 2$, $2 \to 1$.) *)
Definition p021 := p01 * p02.
Goal p021 ord0 = @Ordinal 3 1 erefl.
rewrite !permE /= /p02 /p01 !permE //.
Abort.
Goal p021 (@Ordinal 3 1 erefl) = @Ordinal 3 2 erefl.
rewrite !permE /= /p02 /p01 !permE //.
Abort.
Goal p021 (@Ordinal 3 2 erefl) = ord0.
rewrite !permE /= /p02 /p01 !permE //.
Abort.
(** We define the permutation $(012)$. *)
Definition p012 := p02 * p01.
Ltac same_perm :=
let x := fresh in
apply/permP => /= x;
let x0 := fresh in
case: (boolP (x == ord0)) => [/eqP -> | x0];
[by do ! rewrite !permE /= |
let x1 := fresh in
case: (boolP (x == @Ordinal 3 1 erefl)) => [/eqP -> | x1];
[by do ! rewrite !permE /= |
let x2 := fresh in
case: (boolP (x == @Ordinal 3 2 erefl)) => [/eqP -> | x2];
[by do ! rewrite !permE /= |
(suff : False by done) ;
case: x x0 x1 x2; case=> //; case=> //; by case]]].
(** We build the multiplication and inverse tables for permutations of 3 elements. *)
Lemma p01_p01 : p01 * p01 = 1.
Proof. same_perm. Qed.
Lemma p01_p02 : p01 * p02 = p021.
Proof. same_perm. Qed.
Lemma p01_p012 : p01 * p012 = p12.
Proof. same_perm. Qed.
Lemma p01_p12 : p01 * p12 = p012.
Proof. same_perm. Qed.
Lemma p01_p021 : p01 * p021 = p02.
Proof.
rewrite /p021.
rewrite tpermKg.
done.
Qed.
Lemma p02_p01 : p02 * p01 = p012.
Proof. same_perm. Qed.
Lemma p02_p12 : p02 * p12 = p021.
Proof. same_perm. Qed.
Lemma p02_p012 : p02 * p012 = p01.
Proof. same_perm. Qed.
Lemma p02_p021 : p02 * p021 = p12.
Proof. same_perm. Qed.
Lemma p12_p01 : p12 * p01 = p021.
Proof. same_perm. Qed.
Lemma p12_p02 : p12 * p02 = p012.
Proof. same_perm. Qed.
Lemma p12_p12 : p12 * p12 = 1.
Proof. same_perm. Qed.
Lemma p12_p012 : p12 * p012 = p02.
Proof. same_perm. Qed.
Lemma p12_p021 : p12 * p021 = p01.
Proof. same_perm. Qed.
Lemma p012_p01 : p012 * p01 = p02.
Proof. same_perm. Qed.
Lemma p012_p02 : p012 * p02 = p12.
Proof. same_perm. Qed.
Lemma p012_p12 : p012 * p12 = p01.
Proof. same_perm. Qed.
Lemma p012_p012 : p012 * p012 = p021.
Proof. same_perm. Qed.
Lemma p012_p022 : p012 * p021 = 1.
Proof. same_perm. Qed.
Lemma p021_p01 : p021 * p01 = p12.
Proof. same_perm. Qed.
Lemma p021_p02 : p021 * p02 = p01.
Proof. same_perm. Qed.
Lemma p021_p12 : p021 * p12 = p02.
Proof. same_perm. Qed.
Lemma p021_p012 : p021 * p012 = 1.
Proof. same_perm. Qed.
Lemma p021_p021 : p021 * p021 = p012.
Proof. same_perm. Qed.
Lemma p01_inv : p01 ^-1 = p01.
Proof.
rewrite /p01.
by rewrite tpermV.
Qed.
Lemma p02_inv : p02 ^-1 = p02.
Proof.
rewrite /p02.
by rewrite tpermV.
Qed.
Lemma p12_inv : p12 ^-1 = p12.
Proof.
rewrite /p12.
by rewrite tpermV.
Qed.
Lemma p012_inv : p012 ^-1 = p021.
Proof.
rewrite /p021.
rewrite invMg.
rewrite tpermV.
rewrite tpermV.
done.
Qed.
Lemma p021_inv : p021 ^-1 = p012.
Proof.
rewrite /p021.
rewrite invMg.
rewrite tpermV.
by rewrite tpermV.
Qed.
Lemma p01p12 : p01 != p12.
Proof.
apply/eqP.
move/permP.
move/(_ ord0).
rewrite /p01 /p12.
by rewrite !permE.
Qed.
Lemma p021_1 : p021 <> 1.
Proof.
move=> abs.
have : p021 ord0 = (1 : 'S_3) ord0.
rewrite abs.
by rewrite !permE.
by rewrite !permE /= /p02 /p01 !permE.
Qed.
Lemma p012_1 : p012 <> 1.
Proof.
move=> abs.
have : p012 ord0 = (1 : 'S_3) ord0.
rewrite abs.
by rewrite !permE.
by rewrite !permE /= /p02 /p01 !permE.
Qed.
Lemma p021_neq_p012 : p021 <> p012.
Proof.
move=> abs.
have : p021 ord0 = p012 ord0 by rewrite abs.
rewrite !permE /=.
rewrite /p01 /p02.
by rewrite !permE.
Qed.
Lemma p02_neq_p12 : p02 <> p12.
Proof.
move=> abs.
have : p02 ord0 = p12 ord0.
rewrite abs.
by rewrite !permE.
by rewrite !permE /=.
Qed.
(** We show that S_3 is not commutative. *)
Lemma S_3_not_commutative : ~ commute p01 p021.
Proof.
rewrite /commute.
rewrite p01_p021 p021_p01.
exact p02_neq_p12.
Qed.
(** $A_3$ is the group generated by $(021)$, $(012)$, and $1$. *)
Definition A_3 : {group 'S_3} := [group of << [set p021; p012; 1] >>].
Lemma group_set_A3 : group_set [set p021; p012; 1].
Proof.
apply/group_setP.
split.
by rewrite !inE eqxx orbT.
move=> /= r s Hr Hs.
rewrite !inE in Hr.
rewrite !inE in Hs.
case/orP : Hr.
case/orP.
move/eqP => Hr.
case/orP : Hs.
case/orP.
move/eqP=> Hs.
by rewrite Hr Hs p021_p021 !inE eqxx orbT.
move/eqP => Hs.
by rewrite Hr Hs -{1}p021_inv mulgV !inE eqxx orbT.
move/eqP => Hs.
by rewrite Hr Hs mulg1 !inE eqxx.
case/orP : Hs.
case/orP.
move/eqP=> Hs /eqP Hr.
by rewrite Hr Hs -{1}p021_inv mulVg !inE eqxx orbT.
move/eqP=> Hs /eqP Hr.
by rewrite Hr Hs p012_p012 !inE eqxx.
move/eqP => Hs /eqP Hr.
by rewrite Hr Hs mulg1 !inE eqxx orbT.
case/orP : Hs.
case/orP.
move/eqP=> Hs /eqP Hr.
by rewrite Hr Hs mul1g !inE eqxx.
move/eqP=> Hs /eqP Hr.
by rewrite Hr Hs mul1g !inE eqxx orbT.
move/eqP=> Hs /eqP Hr.
by rewrite Hr Hs mul1g !inE eqxx orbT.
Qed.
Lemma card_A_3 : #| A_3 | = 3.
Proof.
rewrite /A_3 /=.
transitivity (#|[set p021; p012; 1]|).
rewrite gen_set_id //.
exact group_set_A3.
rewrite cardsU.
rewrite cards1.
rewrite cards2.
set tmp2 := _ :&: _.
rewrite (_ : tmp2 = set0); last first.
rewrite /tmp2.
apply/eqP/set0Pn.
case => q /=.
rewrite !inE.
rewrite andb_orl.
case/orP.
case/andP.
move/eqP => ->.
move/eqP.
by apply p021_1.
case/andP => /eqP ->.
move/eqP.
by apply p012_1.
rewrite cards0.
suff -> : p021 != p012.
done.
apply/eqP.
by apply p021_neq_p012.
Qed.
Lemma card_S_3 : #|[group of << [set x in 'S_3]>>]| = 6.
Proof.
rewrite /=.
transitivity (#|[set x in 'S_3]|).
have : group_set [set x in 'S_3] by apply/group_setT.
by move/(gen_set_id) => ->.
rewrite cardsE.
transitivity (#|perm_on [set x in 'I_3]|).
apply eq_card => /= p.
rewrite inE.
apply/esym.
destruct p.
rewrite /perm_on.
rewrite /mem.
rewrite /=.
rewrite /in_mem.
rewrite /=.
apply/subsetP => j /=.
by rewrite inE.
by rewrite card_perm cardsE card_ord.
Qed.
(** $A_3$ is normal in $S_3$. *)
Lemma A_3_S_3 : A_3 <| [group of << [set x in 'S_3] >>].
Proof.
apply index2_normal.
rewrite /=.
apply genS.
apply/subsetP => /= p.
by rewrite !inE.
move: (LagrangeI [group of <<[set x in 'S_3]>>] A_3).
rewrite card_S_3.
suff -> : #|[group of <<[set x in 'S_3]>>] :&: A_3| = 3.
rewrite (_ : 6 = 3 * 2)%nat //.
move/eqP.
rewrite eqn_mul2l /=.
by move/eqP.
set tmp := _ :&: _.
suff : tmp = A_3 by move=> ->; exact card_A_3.
rewrite {}/tmp.
apply/setIidPr.
apply sub_gen.
apply/subsetP => p Hp /=.
by rewrite inE.
Qed.