Library mathcomp.solvable.alt
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import div fintype tuple tuple bigop prime finset ssralg.
From mathcomp Require Import zmodp fingroup morphism perm automorphism quotient.
From mathcomp Require Import action cyclic pgroup gseries sylow.
From mathcomp Require Import primitive_action nilpotent maximal.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
From mathcomp Require Import div fintype tuple tuple bigop prime finset ssralg.
From mathcomp Require Import zmodp fingroup morphism perm automorphism quotient.
From mathcomp Require Import action cyclic pgroup gseries sylow.
From mathcomp Require Import primitive_action nilpotent maximal.
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 GRing.
Section SymAltDef.
Variable T : finType.
Implicit Types (s : {perm T}) (x y z : T).
Definitions of the alternate groups and some Properties *
Definition Sym : {set {perm T}} := setT.
Canonical Sym_group := Eval hnf in [group of Sym].
Local Notation "'Sym_T" := Sym (at level 0).
Canonical sign_morph := @Morphism _ _ 'Sym_T _ (in2W (@odd_permM _)).
Definition Alt := 'ker (@odd_perm T).
Canonical Alt_group := Eval hnf in [group of Alt].
Local Notation "'Alt_T" := Alt (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.
Arguments Sym T%_type.
Arguments Sym_group T%_type.
Arguments Alt T%_type.
Arguments Alt_group T%_type.
Notation "''Sym_' T" := (Sym T)
(at level 8, T at level 2, format "''Sym_' T") : group_scope.
Notation "''Sym_' T" := (Sym_group T) : Group_scope.
Notation "''Alt_' T" := (Alt T)
(at level 8, T at level 2, format "''Alt_' T") : group_scope.
Notation "''Alt_' T" := (Alt_group 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.
Lemma gen_tperm_circular_shift (X : finType) x y c : prime #|X| →
x != y → #[c]%g = #|X| →
<<[set tperm x y; c]>>%g = ('Sym_X)%g.
Section Perm_solvable.
Local Open Scope nat_scope.
Variable T : finType.
Lemma solvable_AltF : 4 < #|T| → solvable 'Alt_T = false.
Lemma solvable_SymF : 4 < #|T| → solvable 'Sym_T = false.
End Perm_solvable.
Canonical Sym_group := Eval hnf in [group of Sym].
Local Notation "'Sym_T" := Sym (at level 0).
Canonical sign_morph := @Morphism _ _ 'Sym_T _ (in2W (@odd_permM _)).
Definition Alt := 'ker (@odd_perm T).
Canonical Alt_group := Eval hnf in [group of Alt].
Local Notation "'Alt_T" := Alt (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.
Arguments Sym T%_type.
Arguments Sym_group T%_type.
Arguments Alt T%_type.
Arguments Alt_group T%_type.
Notation "''Sym_' T" := (Sym T)
(at level 8, T at level 2, format "''Sym_' T") : group_scope.
Notation "''Sym_' T" := (Sym_group T) : Group_scope.
Notation "''Alt_' T" := (Alt T)
(at level 8, T at level 2, format "''Alt_' T") : group_scope.
Notation "''Alt_' T" := (Alt_group 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.
Lemma gen_tperm_circular_shift (X : finType) x y c : prime #|X| →
x != y → #[c]%g = #|X| →
<<[set tperm x y; c]>>%g = ('Sym_X)%g.
Section Perm_solvable.
Local Open Scope nat_scope.
Variable T : finType.
Lemma solvable_AltF : 4 < #|T| → solvable 'Alt_T = false.
Lemma solvable_SymF : 4 < #|T| → solvable 'Sym_T = false.
End Perm_solvable.