Library mathcomp.solvable.alt
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
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 = 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 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 = 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.