(Joint Center)Library MathComp.alt

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype tuple.
Require Import tuple bigop prime finset fingroup morphism perm automorphism.
Require Import quotient action cyclic pgroup gseries sylow primitive_action.

Definitions of the symmetric and alternate groups, and some properties. 'Sym_T == The symmetric group over type T (which must have a finType structure). := [set: {perm T} ] 'Alt_T == The alternating group over type T.

Set Implicit Arguments.

Import GroupScope.

Definition bool_groupMixin := FinGroup.Mixin addbA addFb addbb.
Canonical bool_baseGroup := Eval hnf in BaseFinGroupType bool bool_groupMixin.
Canonical boolGroup := Eval hnf in FinGroupType addbb.

Section SymAltDef.

Variable T : finType.
Implicit Types (s : {perm T}) (x y z : T).

Definitions of the alternate groups and some Properties *
Definition Sym of phant T : {set {perm T}} := setT.

Canonical Sym_group phT := Eval hnf in [group of Sym phT].

Notation Local "'Sym_T" := (Sym (Phant T)) (at level 0).

Canonical sign_morph := @Morphism _ _ 'Sym_T _ (in2W (@odd_permM _)).

Definition Alt of phant T := 'ker (@odd_perm T).

Canonical Alt_group phT := Eval hnf in [group of Alt phT].

Notation Local "'Alt_T" := (Alt (Phant T)) (at level 0).

Lemma Alt_even p : (p \in 'Alt_T) = ~~ p.

Lemma Alt_subset : 'Alt_T \subset 'Sym_T.

Lemma Alt_normal : 'Alt_T <| 'Sym_T.

Lemma Alt_norm : 'Sym_T \subset 'N('Alt_T).

Let n := #|T|.

Lemma Alt_index : 1 < n#|'Sym_T : 'Alt_T| = 2.

Lemma card_Sym : #|'Sym_T| = n`!.

Lemma card_Alt : 1 < n → (2 × #|'Alt_T|)%N = n`!.

Lemma Sym_trans : [transitive^n 'Sym_T, on setT | 'P].

Lemma Alt_trans : [transitive^n.-2 'Alt_T, on setT | 'P].

Lemma aperm_faithful (A : {group {perm T}}) : [faithful A, on setT | 'P].

End SymAltDef.

Notation "''Sym_' T" := (Sym (Phant T))
  (at level 8, T at level 2, format "''Sym_' T") : group_scope.
Notation "''Sym_' T" := (Sym_group (Phant T)) : Group_scope.

Notation "''Alt_' T" := (Alt (Phant T))
  (at level 8, T at level 2, format "''Alt_' T") : group_scope.
Notation "''Alt_' T" := (Alt_group (Phant T)) : Group_scope.

Lemma trivial_Alt_2 (T : finType) : #|T| 2 → 'Alt_T = 1.

Lemma simple_Alt_3 (T : finType) : #|T| = 3 → simple 'Alt_T.

Lemma not_simple_Alt_4 (T : finType) : #|T| = 4 → ~~ simple 'Alt_T.

Lemma simple_Alt5_base (T : finType) : #|T| = 5 → simple 'Alt_T.

Section Restrict.

Variables (T : finType) (x : T).
Notation T' := {y | y != x}.

Lemma rfd_funP (p : {perm T}) (u : T') :
  let p1 := if p x == x then p else 1 in p1 (val u) != x.

Definition rfd_fun p := [fun u Sub ((_ : {perm T}) _) (rfd_funP p u) : T'].

Lemma rfdP p : injective (rfd_fun p).

Definition rfd p := perm (@rfdP p).

Hypothesis card_T : 2 < #|T|.

Lemma rfd_morph : {in 'C_('Sym_T)[x | 'P] &, {morph rfd : y z / y × z}}.

Canonical rfd_morphism := Morphism rfd_morph.

Definition rgd_fun (p : {perm T'}) :=
  [fun x1 if insub x1 is Some u then sval (p u) else x].

Lemma rgdP p : injective (rgd_fun p).

Definition rgd p := perm (@rgdP p).

Lemma rfd_odd (p : {perm T}) : p x = xrfd p = p :> bool.

Lemma rfd_iso : 'C_('Alt_T)[x | 'P] \isog 'Alt_T'.

End Restrict.

Lemma simple_Alt5 (T : finType) : #|T| 5 → simple 'Alt_T.