Library primitive_action

Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
Require Import div seq fintype tuple finset.
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         80
 == the set of n-tuples with distinct values in S.             


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] && ~~ existsb 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 : forall 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 : forall 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).

Variable to : {action gT &-> sT}.
Variable n : nat.

Definition n_act (t : n.-tuple sT) a := [tuple of map (to^~ a) t].

Lemma n_act_is_action : is_action setT n_act.

Canonical Structure 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).
Variable n : nat.
Variable A : {set gT}.
Variable S : {set sT}.
Variable 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 : forall t,
  reflect (injective (tnth t) /\ forall i, tnth t i \in S) (t \in dtuple_on).

Lemma n_act_dtuple : forall t a,
  a \in 'N(S | to) -> t \in dtuple_on -> n_act to t a \in dtuple_on.

End NTransitive.

Implicit Arguments n_act [gT sT n].

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.

Variable (gT : finGroupType) (sT : finType).
Variable to : {action gT &-> sT}.
Variable G : {group gT}.
Variable S : {set sT}.

Lemma card_uniq_tuple : forall n (t : n.-tuple sT), uniq t -> #|t| = n.

Lemma n_act0 : forall (t : 0.-tuple sT) a, n_act to t a = [tuple].

Lemma dtuple_on_add : forall 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 : forall 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 : forall n (S1 S2 : {set sT}) t,
  S1 \subset S2 -> t \in n.-dtuple(S1) -> t \in n.-dtuple(S2).

Lemma n_act_add : forall 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 : forall k m,
  k <= m -> [transitive^m G, on S | to] -> [transitive^k G, on S | to].

Lemma ntransitive1 : forall m,
  0 < m -> [transitive^m G, on S | to] -> [transitive G, on S | to].

Lemma ntransitive_primitive : forall m,
  1 < m -> [transitive^m G, on S | to] -> [primitive G, on S | to].

End NTransitveProp.

Section NTransitveProp1.

Variable (gT : finGroupType) (sT : finType).

Variable to : {action gT &-> sT}.
Variable G : {group gT}.
Variable S : {set sT}.

 Corresponds to => of 15.12.1 Aschbacher 
Theorem stab_ntransitive : forall m x,
     0 < m -> x \in S -> [transitive^m.+1 G, on S | to]
  -> [transitive^m 'C_G[x | to], on S :\ x | to].

 Correspond to <= of 15.12.1 Aschbacher 
Theorem stab_ntransitiveI : forall 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.