- -

Library mathcomp.solvable.primitive_action

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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 }).
- -
-

- -

- 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 ].
- -
-

- -

- This is the converse implication of Aschbacher (15.12).1 -

-Theorem stab_ntransitiveI m x :
-     x \in S → [transitive G , on S | to ] →
-     [transitive ^m 'C_G [x | to ], on S :\ x | to ] →
-  [transitive ^m .+1 G , on S | to ].
- -
-End NTransitveProp1.
-