(Joint Center)Library MathComp.primitive_action

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

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 == 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_onn_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.

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 S2t \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 < mx \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.