Library mathcomp.solvable.primitive_action
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.
From HB Require Import structures*) (*HB is not needed here*)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
From mathcomp Require Import div seq fintype tuple finset.
From mathcomp Require Import fingroup action gseries.
Distributed under the terms of CeCILL-B.
From HB Require Import structures*) (*HB is not needed here*)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
From mathcomp Require Import div seq fintype tuple finset.
From mathcomp Require Import fingroup action gseries.
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.
Arguments imprimitivity_system {aT sT} A%g S%g to%act Q%g.
Arguments primitive {aT sT} A%g S%g to%act.
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.
Arguments dtuple_on {sT} n%N S%g.
Arguments ntransitive {gT sT} n%N A%g S%g to%act.
Arguments n_act {gT sT} to {n} t a.
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