Library mathcomp.solvable.primitive_action
+ +
+(* (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.
+ +
+
+ n-transitive and primitive actions:
+ [primitive A, on S | to] <=>
+ A acts on S in a primitive manner, i.e., A is transitive on S and
+ A does not act on any nontrivial partition of S.
+ imprimitivity_system A to S Q <=>
+ Q is a non-trivial primitivity system for the action of A on S via
+ to, i.e., Q is a non-trivial partiiton of S on which A acts.
+ to * n == in the %act scope, the total action induced by the total
+ action to on n.-tuples. via n_act to n.
+ n.-dtuple S == the set of n-tuples with distinct values in S.
+ [transitive^n A, on S | to] <=>
+ A is n-transitive on S, i.e., A is transitive on n.-dtuple S
+ == the set of n-tuples with distinct values in S.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Section PrimitiveDef.
+ +
+Variables (aT : finGroupType) (sT : finType).
+Variables (A : {set aT}) (S : {set sT}) (to : {action aT &-> sT}).
+ +
+Definition imprimitivity_system Q :=
+ [&& partition Q S, [acts A, on Q | to^*] & 1 < #|Q| < #|S|].
+ +
+Definition primitive :=
+ [transitive A, on S | to] && ~~ [∃ Q, imprimitivity_system Q].
+ +
+End PrimitiveDef.
+ +
+ +
+Notation "[ 'primitive' A , 'on' S | to ]" := (primitive A S to)
+ (at level 0, format "[ 'primitive' A , 'on' S | to ]") : form_scope.
+ +
+ +
+Section Primitive.
+ +
+Variables (aT : finGroupType) (sT : finType).
+Variables (G : {group aT}) (to : {action aT &-> sT}) (S : {set sT}).
+ +
+Lemma trans_prim_astab x :
+ x \in S → [transitive G, on S | to] →
+ [primitive G, on S | to] = maximal_eq 'C_G[x | to] G.
+ +
+Lemma prim_trans_norm (H : {group aT}) :
+ [primitive G, on S | to] → H <| G →
+ H \subset 'C_G(S | to) ∨ [transitive H, on S | to].
+ +
+End Primitive.
+ +
+Section NactionDef.
+ +
+Variables (gT : finGroupType) (sT : finType).
+Variables (to : {action gT &-> sT}) (n : nat).
+ +
+Definition n_act (t : n.-tuple sT) a := [tuple of map (to^~ a) t].
+ +
+Fact n_act_is_action : is_action setT n_act.
+ +
+Canonical n_act_action := Action n_act_is_action.
+ +
+End NactionDef.
+ +
+Notation "to * n" := (n_act_action to n) : action_scope.
+ +
+Section NTransitive.
+ +
+Variables (gT : finGroupType) (sT : finType).
+Variables (n : nat) (A : {set gT}) (S : {set sT}) (to : {action gT &-> sT}).
+ +
+Definition dtuple_on := [set t : n.-tuple sT | uniq t & t \subset S].
+Definition ntransitive := [transitive A, on dtuple_on | to × n].
+ +
+Lemma dtuple_onP t :
+ reflect (injective (tnth t) ∧ ∀ i, tnth t i \in S) (t \in dtuple_on).
+ +
+Lemma n_act_dtuple t a :
+ a \in 'N(S | to) → t \in dtuple_on → n_act to t a \in dtuple_on.
+ +
+End NTransitive.
+ +
+ +
+Notation "n .-dtuple ( S )" := (dtuple_on n S)
+ (at level 8, format "n .-dtuple ( S )") : set_scope.
+ +
+Notation "[ 'transitive' ^ n A , 'on' S | to ]" := (ntransitive n A S to)
+ (at level 0, n at level 8,
+ format "[ 'transitive' ^ n A , 'on' S | to ]") : form_scope.
+ +
+Section NTransitveProp.
+ +
+Variables (gT : finGroupType) (sT : finType).
+Variables (to : {action gT &-> sT}) (G : {group gT}) (S : {set sT}).
+ +
+Lemma card_uniq_tuple n (t : n.-tuple sT) : uniq t → #|t| = n.
+ +
+Lemma n_act0 (t : 0.-tuple sT) a : n_act to t a = [tuple].
+ +
+Lemma dtuple_on_add n x (t : n.-tuple sT) :
+ ([tuple of x :: t] \in n.+1.-dtuple(S)) =
+ [&& x \in S, x \notin t & t \in n.-dtuple(S)].
+ +
+Lemma dtuple_on_add_D1 n x (t : n.-tuple sT) :
+ ([tuple of x :: t] \in n.+1.-dtuple(S))
+ = (x \in S) && (t \in n.-dtuple(S :\ x)).
+ +
+Lemma dtuple_on_subset n (S1 S2 : {set sT}) t :
+ S1 \subset S2 → t \in n.-dtuple(S1) → t \in n.-dtuple(S2).
+ +
+Lemma n_act_add n x (t : n.-tuple sT) a :
+ n_act to [tuple of x :: t] a = [tuple of to x a :: n_act to t a].
+ +
+Lemma ntransitive0 : [transitive^0 G, on S | to].
+ +
+Lemma ntransitive_weak k m :
+ k ≤ m → [transitive^m G, on S | to] → [transitive^k G, on S | to].
+ +
+Lemma ntransitive1 m :
+ 0 < m → [transitive^m G, on S | to] → [transitive G, on S | to].
+ +
+Lemma ntransitive_primitive m :
+ 1 < m → [transitive^m G, on S | to] → [primitive G, on S | to].
+ +
+End NTransitveProp.
+ +
+Section NTransitveProp1.
+ +
+Variables (gT : finGroupType) (sT : finType).
+Variables (to : {action gT &-> sT}) (G : {group gT}) (S : {set sT}).
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Section PrimitiveDef.
+ +
+Variables (aT : finGroupType) (sT : finType).
+Variables (A : {set aT}) (S : {set sT}) (to : {action aT &-> sT}).
+ +
+Definition imprimitivity_system Q :=
+ [&& partition Q S, [acts A, on Q | to^*] & 1 < #|Q| < #|S|].
+ +
+Definition primitive :=
+ [transitive A, on S | to] && ~~ [∃ Q, imprimitivity_system Q].
+ +
+End PrimitiveDef.
+ +
+ +
+Notation "[ 'primitive' A , 'on' S | to ]" := (primitive A S to)
+ (at level 0, format "[ 'primitive' A , 'on' S | to ]") : form_scope.
+ +
+ +
+Section Primitive.
+ +
+Variables (aT : finGroupType) (sT : finType).
+Variables (G : {group aT}) (to : {action aT &-> sT}) (S : {set sT}).
+ +
+Lemma trans_prim_astab x :
+ x \in S → [transitive G, on S | to] →
+ [primitive G, on S | to] = maximal_eq 'C_G[x | to] G.
+ +
+Lemma prim_trans_norm (H : {group aT}) :
+ [primitive G, on S | to] → H <| G →
+ H \subset 'C_G(S | to) ∨ [transitive H, on S | to].
+ +
+End Primitive.
+ +
+Section NactionDef.
+ +
+Variables (gT : finGroupType) (sT : finType).
+Variables (to : {action gT &-> sT}) (n : nat).
+ +
+Definition n_act (t : n.-tuple sT) a := [tuple of map (to^~ a) t].
+ +
+Fact n_act_is_action : is_action setT n_act.
+ +
+Canonical n_act_action := Action n_act_is_action.
+ +
+End NactionDef.
+ +
+Notation "to * n" := (n_act_action to n) : action_scope.
+ +
+Section NTransitive.
+ +
+Variables (gT : finGroupType) (sT : finType).
+Variables (n : nat) (A : {set gT}) (S : {set sT}) (to : {action gT &-> sT}).
+ +
+Definition dtuple_on := [set t : n.-tuple sT | uniq t & t \subset S].
+Definition ntransitive := [transitive A, on dtuple_on | to × n].
+ +
+Lemma dtuple_onP t :
+ reflect (injective (tnth t) ∧ ∀ i, tnth t i \in S) (t \in dtuple_on).
+ +
+Lemma n_act_dtuple t a :
+ a \in 'N(S | to) → t \in dtuple_on → n_act to t a \in dtuple_on.
+ +
+End NTransitive.
+ +
+ +
+Notation "n .-dtuple ( S )" := (dtuple_on n S)
+ (at level 8, format "n .-dtuple ( S )") : set_scope.
+ +
+Notation "[ 'transitive' ^ n A , 'on' S | to ]" := (ntransitive n A S to)
+ (at level 0, n at level 8,
+ format "[ 'transitive' ^ n A , 'on' S | to ]") : form_scope.
+ +
+Section NTransitveProp.
+ +
+Variables (gT : finGroupType) (sT : finType).
+Variables (to : {action gT &-> sT}) (G : {group gT}) (S : {set sT}).
+ +
+Lemma card_uniq_tuple n (t : n.-tuple sT) : uniq t → #|t| = n.
+ +
+Lemma n_act0 (t : 0.-tuple sT) a : n_act to t a = [tuple].
+ +
+Lemma dtuple_on_add n x (t : n.-tuple sT) :
+ ([tuple of x :: t] \in n.+1.-dtuple(S)) =
+ [&& x \in S, x \notin t & t \in n.-dtuple(S)].
+ +
+Lemma dtuple_on_add_D1 n x (t : n.-tuple sT) :
+ ([tuple of x :: t] \in n.+1.-dtuple(S))
+ = (x \in S) && (t \in n.-dtuple(S :\ x)).
+ +
+Lemma dtuple_on_subset n (S1 S2 : {set sT}) t :
+ S1 \subset S2 → t \in n.-dtuple(S1) → t \in n.-dtuple(S2).
+ +
+Lemma n_act_add n x (t : n.-tuple sT) a :
+ n_act to [tuple of x :: t] a = [tuple of to x a :: n_act to t a].
+ +
+Lemma ntransitive0 : [transitive^0 G, on S | to].
+ +
+Lemma ntransitive_weak k m :
+ k ≤ m → [transitive^m G, on S | to] → [transitive^k G, on S | to].
+ +
+Lemma ntransitive1 m :
+ 0 < m → [transitive^m G, on S | to] → [transitive G, on S | to].
+ +
+Lemma ntransitive_primitive m :
+ 1 < m → [transitive^m G, on S | to] → [primitive G, on S | to].
+ +
+End NTransitveProp.
+ +
+Section NTransitveProp1.
+ +
+Variables (gT : finGroupType) (sT : finType).
+Variables (to : {action gT &-> sT}) (G : {group gT}) (S : {set sT}).
+ +
+
+ This is the forward implication of Aschbacher (15.12).1
+
+
+Theorem stab_ntransitive m x :
+ 0 < m → x \in S → [transitive^m.+1 G, on S | to] →
+ [transitive^m 'C_G[x | to], on S :\ x | to].
+ +
+
+
++ 0 < m → x \in S → [transitive^m.+1 G, on S | to] →
+ [transitive^m 'C_G[x | to], on S :\ x | to].
+ +
+
+ This is the converse implication of Aschbacher (15.12).1
+
+
+