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 fingroup.
From mathcomp Require Import morphism perm automorphism quotient action cyclic.
From mathcomp Require Import pgroup gseries sylow primitive_action.
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 fingroup.
From mathcomp Require Import morphism perm automorphism quotient action cyclic.
From mathcomp Require Import 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.
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.
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.