# Library mathcomp.solvable.primitive_action

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
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 partition 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].
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.