Library mathcomp.solvable.alt
+ +
+(* (c) Copyright 2006-2016 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).
+ +
+
+
++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.
+
++ +
+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.
+