Library alt

  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.                           


Import GroupScope.

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

Section SymAltDef.

Variable T : finType.

Implicit Type s : {perm T}.
Implicit Types x y z : T.

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

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

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

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

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

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

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

Lemma Alt_even : forall 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).


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 : forall 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)) : subgroup_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)) : subgroup_scope.

Lemma trivial_Alt_2 : forall T : finType, #|T| <= 2 -> 'Alt_T = 1.

Lemma simple_Alt_3 : forall T : finType, #|T| = 3 -> simple 'Alt_T.

Lemma not_simple_Alt_4 : forall T : finType, #|T| = 4 -> ~~ simple 'Alt_T.

Module Alt_CP_1. End Alt_CP_1.

Lemma simple_Alt5_base : forall T : finType, #|T| = 5 -> simple 'Alt_T.

Module Alt_CP_2. End Alt_CP_2.

Section Restrict.

Variable T : finType.
Variable x : T.
Notation T' := {y | y != x}.

Lemma rfd_funP : forall (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 : forall 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 Structure 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 : forall p, injective (rgd_fun p).

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

Lemma rfd_odd : forall p : {perm T}, p x = x -> rfd p = p :> bool.

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

End Restrict.

Module Alt_CP_3. End Alt_CP_3.

Lemma simple_Alt5 : forall T : finType, #|T| >= 5 -> simple 'Alt_T.