- -

Library mathcomp.solvable.alt

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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 ].
- -
- -
-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 ].
- -
- -
-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 = x → rfd 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.
-