# Library action

 Group action: orbits, stabilisers, transitivity.
is_action D to == the function to : T -> aT -> T defines an action
of D : {set aT} on T.
action D T == structure for a function defining an action of D.
act_dom to == the domain D of to : action D rT.
{action: aT &-> T} == structure for a total action.
:= action [set: aT] T
TotalAction to1 toM == the constructor for total actions; to1 and toM
are the proofs of the action identities for 1 and
a * b, respectively.
is_groupAction R to == to is a group action on range R: for all a in D,
the permutation induced by to a is in Aut R. Thus
the action of D must be trivial outside R.
groupAction D R == the structure for group actions of D on R. This
is a telescope on action D rT.
gact_range to == the range R of to : groupAction D R.
GroupAction toAut == construct a groupAction for action to from
toAut : actm to @* D \subset Aut R (actm to is
the morphism to {perm rT} associated to 'to').
orbit to A x == the orbit of x under the action of A via to.
amove to A x y == the set of a in A whose action send x to y.
'C_A[x | to] == the stabiliser of x : rT in A :&: D.
'C_A(S | to) == the point-wise stabiliser of S : {set rT} in D :&: A.
'N_A(S | to) == the global stabiliser of S : {set rT} in D :&: A.
'Fix_(S | to)[a] == the set of fixpoints of a in S.
'Fix_(S | to)(A) == the set of fixpoints of A in S.
In the first three _A can be omitted and defaults to the domain D of to;
In the last two S can be omitted and defaults to [set: T], so 'Fix_to[a]
is the set of all fixpoints of a.
The domain restriction ensures that stabilisers have a canonical group
structure, but note that 'Fix sets are generally not groups. Indeed, we
provide alternative definitions when to is a group action on R:
'C_(G | to)(A) == the centraliser in R :&: G of the group action of
D :&: A via to
'C_(G | to)[a] == the centraliser in R :&: G of a \in D, via to.
These sets are groups when G is. G can be omitted: 'C(|to)(A) is the
centraliser in R of the action of D :&: A via to.
[acts A, on S | to] == A \subset D acts on the set S via to.
{acts A, on S | to} == A acts on the set S (Prop statement).
{acts A, on group G | to} == [acts A, on S | to] /\ G \subset R, i.e.,
A \subset D acts on G \subset R, via
to : groupAction D R.
[transitive A, on S | to] == A acts transitively on S.
[faithful A, on S | to] == A acts faithfully on S.
acts_irreducibly to A G == A acts irreducibly via the groupAction to
on the nontrivial group G, i.e., A does
not act on any nontrivial subgroup of G.
Important caveat: the definitions of orbit, amove, 'Fix_(S | to)(A),
transitive and faithful assume that A is a subset of the domain D. As most
of the permutation actions we consider are total this is usually harmless.
(Note that the theory of partial actions is only partially developed.)
In all of the above, to is expected to be the actual action structure,
not merely the function. There is a special scope %act for actions, and
constructions and notations for many classical actions:
'P == natural action of a permutation group via aperm.
'J == internal group action (conjugation) via conjg (_ ^ _).
'R == regular group action (right translation) via mulg (_ * _).
(but, to limit ambiguity, _ * _ is NOT a canonical action)
to^* == the action induced by to on {set rT} via to^* (== setact to).
'Js == the internal action on subsets via _ :^ _, equivalent to 'J^*.
'Rs == the regular action on subsets via rcoset, equivalent to 'R^*.
'JG == the conjugation action on {group rT} via (_ :^ _)%G.
to / H == the action induced by to on coset_of H via qact to H, and
restricted to qact_dom to H == 'N(rcosets H 'N(H) | to^* ).
'Q == the action induced to cosets by conjugation; the domain is
qact_dom 'J H, which is provably equal to 'N(H).
to %% A == the action of coset_of A via modact to A, with domain D / A
and support restricted to 'C(D :&: A | to).
to \ sAD == the action of A via ract to sAD == to, if sAD : A \subset D.
[Aut G] == the permutation action restricted to Aut G, via autact G.
<[nRA]> == the action of A on R via actby nRA == to in A and on R, and
the trivial action elsewhere; here nRA : [acts A, on R | to]
or nRA : {acts A, on group R | to}.
to^? == the action induced by to on sT : @subType rT P, via subact to
with domain subact_dom P to == 'N([set x | P x] | to).
<<phi>> == the action of phi : D >-> {perm rT}, via mact phi.
to \o f == the composite action (with domain f @*^-1 D) of the action to
with f : {morphism G >-> aT}, via comp_act to f. Here f must
be the actual morphism object (e.g., coset_morphism H), not
the underlying function (e.g., coset H).
The explicit application of an action to is usually written (to%act x a),
where the %act omitted if to is an abstract action or a set action to0^*.
Note that this form will simplify and expose the acting function.
There is a %gact scope for group actions; the notations above are
recognised in %gact when they denote canonical group actions.
Actions can be used to define morphisms:
actperm to == the morphism D >-> {perm rT} induced by to.
actm to a == if a \in D the function on D induced by the action to, else
the identity function. If to is a group action with range R
then actm to a is canonically a morphism on R.
We also define here the restriction operation on permutations (the domain
of this operations is a stabiliser), and local automorphpism groups:
restr_perm S p == if p acts on S, the permutation with support in S that
coincides with p on S; else the identity. Note that
restr_perm is a permutation group morphism that maps
Aut G to Aut S when S is a subgroup of G.
Aut_in A G == the local permutation group 'N_A(G | 'P) / 'C_A(G | 'P)
Usually A is an automorphism group, and then Aut_in A G
is isomorphic to a subgroup of Aut G, specifically
restr_perm @* A.
Finally, gproduct.v will provide a semi-direct group construction that
maps an external group action to an internal one; the theory of morphisms
between such products makes use of the following definition:
morph_act to to' f fA <=> the action of to' on the images of f and fA is
the image of the action of to, i.e., for all x and a we
have f (to x a) = to' (f x) (fA a). Note that there is
no mention of the domains of to and to'; if needed, this
predicate should be restricted via the {in ...} notation
and domain conditions should be added.


Import GroupScope.

Section ActionDef.

Variables (aT : finGroupType) (D : {set aT}) (rT : Type).
Implicit Types a b : aT.
Implicit Type x : rT.

Definition act_morph to x := forall a b, to x (a * b) = to (to x a) b.

Definition is_action to :=
left_injective to /\ forall x, {in D &, act_morph to x}.

Record action := Action {act :> rT -> aT -> rT; _ : is_action act}.

Definition clone_action to :=
let: Action _ toP := to return {type of Action for to} -> action in
fun k => k toP.

End ActionDef.

 Need to close the Section here to avoid re-declaring all Argument Scopes

Delimit Scope action_scope with act.

Notation "{ 'action' aT &-> T }" := (action [set: aT] T)
(at level 0, format "{ 'action' aT &-> T }") : type_scope.

Notation "[ 'action' 'of' to ]" := (clone_action (@Action _ _ _ to))
(at level 0, format "[ 'action' 'of' to ]") : form_scope.

Definition act_dom aT D rT of @action aT D rT := D.

Section TotalAction.

Variables (aT : finGroupType) (rT : Type) (to : rT -> aT -> rT).
Hypotheses (to1 : to^~ 1 =1 id) (toM : forall x, act_morph to x).

Lemma is_total_action : is_action setT to.

Definition TotalAction := Action is_total_action.

End TotalAction.

Section ActionDefs.

Variables (aT aT' : finGroupType) (D : {set aT}) (D' : {set aT'}).

Definition morph_act rT rT' (to : action D rT) (to' : action D' rT') f fA :=
forall x a, f (to x a) = to' (f x) (fA a).

Variable rT : finType. Implicit Type to : action D rT.
Implicit Type A : {set aT}.
Implicit Type S : {set rT}.

Definition actm to a := if a \in D then to^~ a else id.

Definition setact to S a := [set to x a | x <- S].

Definition orbit to A x := to x @: A.

Definition amove to A x y := [set a \in A | to x a == y].

Definition afix to A := [set x | A \subset [set a | to x a == x]].

Definition astab S to := D :&: [set a | S \subset [set x | to x a == x]].

Definition astabs S to := D :&: [set a | S \subset to^~ a @^-1: S].

Definition acts_on A S to := {in A, forall a x, (to x a \in S) = (x \in S)}.

Definition atrans A S to := S \in orbit to A @: S.

Definition faithful A S to := A :&: astab S to \subset .

End ActionDefs.

Notation "to ^*" := (setact to) (at level 2, format "to ^*") : fun_scope.

Notation "''Fix_' to ( A )" := (afix to A)
(at level 8, to at level 2, format "''Fix_' to ( A )") : group_scope.

 camlp4 grammar factoring

Notation "''Fix_' ( to ) ( A )" := 'Fix_to(A)
(at level 8, only parsing) : group_scope.

Notation "''Fix_' ( S | to ) ( A )" := (S :&: 'Fix_to(A))
(at level 8, format "''Fix_' ( S | to ) ( A )") : group_scope.

Notation "''Fix_' to [ a ]" := ('Fix_to([set a]))
(at level 8, to at level 2, format "''Fix_' to [ a ]") : group_scope.

Notation "''Fix_' ( S | to ) [ a ]" := (S :&: 'Fix_to[a])
(at level 8, format "''Fix_' ( S | to ) [ a ]") : group_scope.

Notation "''C' ( S | to )" := (astab S to)
(at level 8, format "''C' ( S | to )") : group_scope.

Notation "''C_' A ( S | to )" := (A :&: 'C(S | to))
(at level 8, A at level 2, format "''C_' A ( S | to )") : group_scope.
Notation "''C_' ( A ) ( S | to )" := 'C_A(S | to)
(at level 8, only parsing) : group_scope.

Notation "''C' [ x | to ]" := ('C([set x] | to))
(at level 8, format "''C' [ x | to ]") : group_scope.

Notation "''C_' A [ x | to ]" := (A :&: 'C[x | to])
(at level 8, A at level 2, format "''C_' A [ x | to ]") : group_scope.
Notation "''C_' ( A ) [ x | to ]" := 'C_A[x | to]
(at level 8, only parsing) : group_scope.

Notation "''N' ( S | to )" := (astabs S to)
(at level 8, format "''N' ( S | to )") : group_scope.

Notation "''N_' A ( S | to )" := (A :&: 'N(S | to))
(at level 8, A at level 2, format "''N_' A ( S | to )") : group_scope.

Notation "[ 'acts' A , 'on' S | to ]" := (A \subset pred_of_set 'N(S | to))
(at level 0, format "[ 'acts' A , 'on' S | to ]") : form_scope.

Notation "{ 'acts' A , 'on' S | to }" := (acts_on A S to)
(at level 0, format "{ 'acts' A , 'on' S | to }") : form_scope.

Notation "[ 'transitive' A , 'on' S | to ]" := (atrans A S to)
(at level 0, format "[ 'transitive' A , 'on' S | to ]") : form_scope.

Notation "[ 'faithful' A , 'on' S | to ]" := (faithful A S to)
(at level 0, format "[ 'faithful' A , 'on' S | to ]") : form_scope.

Section RawAction.
 Lemmas that do not require the group structure on the action domain.
Some lemmas like actMin would be actually be valid for arbitrary rT,
e.g., for actions on a function type, but would be difficult to use
as a view due to the confusion between parameters and assumptions.


Variables (aT : finGroupType) (D : {set aT}) (rT : finType) (to : action D rT).

Implicit Types a : aT.
Implicit Types x y : rT.
Implicit Type A B : {set aT}.
Implicit Types S T : {set rT}.

Lemma act_inj : left_injective to.

Implicit Arguments act_inj [].

Lemma actMin : forall x, {in D &, act_morph to x}.

Lemma actmEfun : forall a, a \in D -> actm to a = to^~ a.

Lemma actmE : forall a, a \in D -> actm to a =1 to^~ a.

Lemma setactE : forall S a, to^* S a = [set to x a | x <- S].

Lemma mem_setact : forall S a x, x \in S -> to x a \in to^* S a.

Lemma card_setact : forall S a, #|to^* S a| = #|S|.

Lemma setact_is_action : is_action D to^*.

Canonical Structure set_action := Action setact_is_action.

Lemma orbitE : forall A x, orbit to A x = to x @: A.

Lemma orbitP : forall A x y,
reflect (exists2 a, a \in A & to x a = y) (y \in orbit to A x).

Lemma mem_orbit : forall A x a, a \in A -> to x a \in orbit to A x.

Lemma afixP : forall A x,
reflect (forall a, a \in A -> to x a = x) (x \in 'Fix_to(A)).

Lemma afixS : forall A B, A \subset B -> 'Fix_to(B) \subset 'Fix_to(A).

Lemma afixU : forall A B, 'Fix_to(A :|: B) = 'Fix_to(A) :&: 'Fix_to(B).

Lemma afix1P : forall a x, reflect (to x a = x) (x \in 'Fix_to[a]).

Lemma astabIdom : forall S, 'C_D(S | to) = 'C(S | to).

Lemma astab_dom : forall S, {subset 'C(S | to) <= D}.

Lemma astab_act : forall S a x, a \in 'C(S | to) -> x \in S -> to x a = x.

Lemma astabS : forall S1 S2 : {set rT},
S1 \subset S2 -> 'C(S2 | to) \subset 'C(S1 | to).

Lemma astabsIdom : forall S, 'N_D(S | to) = 'N(S | to).

Lemma astabs_dom : forall S, {subset 'N(S | to) <= D}.

Lemma astabs_act : forall S a x,
a \in 'N(S | to) -> (to x a \in S) = (x \in S).

Lemma astab_sub : forall S, 'C(S | to) \subset 'N(S | to).

Lemma astabsC : forall S, 'N(~: S | to) = 'N(S | to).

Lemma astabsI : forall S T, 'N(S | to) :&: 'N(T | to) \subset 'N(S :&: T | to).

Lemma astabs_setact : forall S a, a \in 'N(S | to) -> to^* S a = S.

Lemma astab1_set : forall S, 'C[S | set_action] = 'N(S | to).

Lemma astabs_set1 : forall x, 'N([set x] | to) = 'C[x | to].

Lemma acts_dom : forall A S, [acts A, on S | to] -> A \subset D.

Lemma acts_act : forall A S, [acts A, on S | to] -> {acts A, on S | to}.

Lemma astabCin : forall A S,
A \subset D -> (A \subset 'C(S | to)) = (S \subset 'Fix_to(A)).

Section ActsSetop.

Variables (A : {set aT}) (S T : {set rT}).
Hypotheses (AactS : [acts A, on S | to]) (AactT : [acts A, on T | to]).

Lemma astabU : 'C(S :|: T | to) = 'C(S | to) :&: 'C(T | to).

Lemma astabsU : 'N(S | to) :&: 'N(T | to) \subset 'N(S :|: T | to).

Lemma astabsD : 'N(S | to) :&: 'N(T | to) \subset 'N(S :\: T| to).

Lemma actsI : [acts A, on S :&: T | to].

Lemma actsU : [acts A, on S :|: T | to].

Lemma actsD : [acts A, on S :\: T | to].

End ActsSetop.

Lemma acts_in_orbit : forall A S x y,
[acts A, on S | to] -> y \in orbit to A x -> x \in S -> y \in S.

Lemma subset_faithful : forall A B S,
B \subset A -> [faithful A, on S | to] -> [faithful B, on S | to].

Section Reindex.

Variables (vT : Type) (idx : vT) (op : Monoid.com_law idx) (S : {set rT}).

Lemma reindex_astabs : forall a F, a \in 'N(S | to) ->
\big[op/idx]_(i \in S) F i = \big[op/idx]_(i \in S) F (to i a).

Lemma reindex_acts : forall A a F, [acts A, on S | to] -> a \in A ->
\big[op/idx]_(i \in S) F i = \big[op/idx]_(i \in S) F (to i a).

End Reindex.

End RawAction.

 Warning: this directive depends on names of bound variables in the
definition of injective, in ssrfun.v.

Implicit Arguments act_inj [[aT] [D] [rT] x1 x2].

Notation "to ^*" := (set_action to) : action_scope.

Implicit Arguments orbitP [aT D rT to A x y].
Implicit Arguments afixP [aT D rT to A x].
Implicit Arguments afix1P [aT D rT to a x].

Implicit Arguments reindex_astabs [aT D rT vT idx op S F].
Implicit Arguments reindex_acts [aT D rT vT idx op S A a F].

Section PartialAction.
 Lemmas that require a (partial) group domain.


Variables (aT : finGroupType) (D : {group aT}) (rT : finType).
Variable to : action D rT.

Implicit Types a : aT.
Implicit Types x y : rT.
Implicit Types A B : {set aT}.
Implicit Types G H : {group aT}.
Implicit Types S : {set rT}.

Lemma act1 : forall x, to x 1 = x.

Lemma actKin : {in D, right_loop invg to}.

Lemma actKVin : {in D, rev_right_loop invg to}.

Lemma setactVin : forall S a, a \in D -> to^* S a^-1 = to^~ a @^-1: S.

Lemma actXin : forall x a i, a \in D -> to x (a ^+ i) = iter i (to^~ a) x.

Lemma afix1 : 'Fix_to(1) = setT.

Lemma afixD1 : forall G, 'Fix_to(G^#) = 'Fix_to(G).

Lemma orbit_refl : forall G x, x \in orbit to G x.

Local Notation orbit_rel A := (fun x y => y \in orbit to A x).

Lemma contra_orbit : forall G x y, x \notin orbit to G y -> x != y.

Lemma orbit_in_sym : forall G, G \subset D -> symmetric (orbit_rel G).

Lemma orbit_in_trans : forall G, G \subset D -> transitive (orbit_rel G).

Lemma orbit_in_transl : forall G x y,
G \subset D -> y \in orbit to G x -> orbit to G y = orbit to G x.

Lemma orbit_in_transr : forall G x y z,
G \subset D -> y \in orbit to G x ->
(y \in orbit to G z) = (x \in orbit to G z).

Lemma orbit_inv_in : forall A x y, A \subset D ->
(y \in orbit to A^-1 x) = (x \in orbit to A y).

Lemma orbit_lcoset_in : forall A a x, A \subset D -> a \in D ->
orbit to (a *: A) x = orbit to A (to x a).

Lemma orbit_rcoset_in : forall A a x y, A \subset D -> a \in D ->
(to y a \in orbit to (A :* a) x) = (y \in orbit to A x).

Lemma orbit_conjsg_in : forall A a x y, A \subset D -> a \in D ->
(to y a \in orbit to (A :^ a) (to x a)) = (y \in orbit to A x).

Lemma orbit1P : forall G x,
reflect (orbit to G x = [set x]) (x \in 'Fix_to(G)).

Lemma card_orbit1 : forall G x,
#|orbit to G x| = 1%N -> orbit to G x = [set x].

Lemma group_set_astab : forall S, group_set 'C(S | to).

Canonical Structure astab_group S := group (group_set_astab S).

Lemma afix_gen_in : forall A, A \subset D -> 'Fix_to(<<A>>) = 'Fix_to(A).

Lemma afix_cycle_in : forall a, a \in D -> 'Fix_to(<[a]>) = 'Fix_to[a].

Lemma afixYin : forall A B,
A \subset D -> B \subset D -> 'Fix_to(A <*> B) = 'Fix_to(A) :&: 'Fix_to(B).

Lemma afixMin : forall G H,
G \subset D -> H \subset D -> 'Fix_to(G * H) = 'Fix_to(G) :&: 'Fix_to(H).

Lemma sub_astab1_in : forall A x,
A \subset D -> (A \subset 'C[x | to]) = (x \in 'Fix_to(A)).

Lemma group_set_astabs : forall S, group_set 'N(S | to).

Canonical Structure astabs_group S := group (group_set_astabs S).

Lemma astab_norm : forall S, 'N(S | to) \subset 'N('C(S | to)).

Lemma astab_normal : forall S, 'C(S | to) <| 'N(S | to).

Lemma acts_sub_orbit : forall G S x,
[acts G, on S | to] -> (orbit to G x \subset S) = (x \in S).

Lemma acts_orbit : forall G x, G \subset D -> [acts G, on orbit to G x | to].

Lemma acts_subnorm_fix : forall A, [acts 'N_D(A), on 'Fix_to(D :&: A) | to].

Lemma atrans_orbit : forall G x, [transitive G, on orbit to G x | to].

Section OrbitStabilizer.

Variables (G : {group aT}) (x : rT).
Hypothesis sGD : G \subset D.

Lemma amove_act : forall a,
a \in G -> amove to G x (to x a) = 'C_G[x | to] :* a.

Lemma amove_orbit : amove to G x @: orbit to G x = rcosets 'C_G[x | to] G.

Lemma amoveK :
{in orbit to G x, cancel (amove to G x) (fun Ca => to x (repr Ca))}.

Lemma orbit_stabilizer :
orbit to G x = [set to x (repr Ca) | Ca <- rcosets 'C_G[x | to] G].

Lemma act_reprK :
{in rcosets 'C_G[x | to] G, cancel (to x \o repr) (amove to G x)}.

End OrbitStabilizer.

Lemma card_orbit_in : forall G x,
G \subset D -> #|orbit to G x| = #|G : 'C_G[x | to]|.

Lemma card_orbit_in_stab : forall G x,
G \subset D -> (#|orbit to G x| * #|'C_G[x | to]|)%N = #|G|.

Lemma acts_sum_card_orbit : forall G S,
[acts G, on S | to] -> \sum_(T \in orbit to G @: S) #|T| = #|S|.

Lemma astab_setact_in : forall S a,
a \in D -> 'C(to^* S a | to) = 'C(S | to) :^ a.

Lemma astab1_act_in : forall x a, a \in D -> 'C[to x a | to] = 'C[x | to] :^ a.

Theorem Frobenius_Cauchy : forall G S, [acts G, on S | to] ->
\sum_(a \in G) #|'Fix_(S | to)[a]| = (#|orbit to G @: S| * #|G|)%N.

Lemma atrans_dvd_index_in : forall G S,
G \subset D -> [transitive G, on S | to] -> #|S| %| #|G : 'C_G(S | to)|.

Lemma atrans_dvd_in : forall G S,
G \subset D -> [transitive G, on S | to] -> #|S| %| #|G|.

Lemma atransPin : forall G S,
G \subset D -> [transitive G, on S | to] ->
forall x, x \in S -> orbit to G x = S.

Lemma atransP2in : forall G S,
G \subset D -> [transitive G, on S | to] ->
{in S &, forall x y, exists2 a, a \in G & y = to x a}.

Lemma atrans_acts_in : forall G S,
G \subset D -> [transitive G, on S | to] -> [acts G, on S | to].

Lemma subgroup_transitivePin : forall G H S x,
x \in S -> H \subset G -> G \subset D -> [transitive G, on S | to] ->
reflect ('C_G[x | to] * H = G) [transitive H, on S | to].

End PartialAction.

Implicit Arguments orbit1P [aT D rT to G x].
Implicit Arguments contra_orbit [aT D rT x y].

Notation "''C' ( S | to )" := (astab_group to S) : subgroup_scope.
Notation "''C_' A ( S | to )" := (setI_group A 'C(S | to)) : subgroup_scope.
Notation "''C_' ( A ) ( S | to )" := (setI_group A 'C(S | to))
(only parsing) : subgroup_scope.
Notation "''C' [ x | to ]" := (astab_group to [set x%g]) : subgroup_scope.
Notation "''C_' A [ x | to ]" := (setI_group A 'C[x | to]) : subgroup_scope.
Notation "''C_' ( A ) [ x | to ]" := (setI_group A 'C[x | to])
(only parsing) : subgroup_scope.
Notation "''N' ( S | to )" := (astabs_group to S) : subgroup_scope.
Notation "''N_' A ( S | to )" := (setI_group A 'N(S | to)) : subgroup_scope.

Section TotalActions.
 These lemmas are only established for total actions (domain = [set: rT])


Variable (aT : finGroupType) (rT : finType).

Variable to : {action aT &-> rT}.

Implicit Types a b : aT.
Implicit Types x y z : rT.
Implicit Types A B : {set aT}.
Implicit Types G H : {group aT}.
Implicit Types S : {set rT}.

Lemma actM : forall x a b, to x (a * b) = to (to x a) b.

Lemma actK : right_loop invg to.

Lemma actKV : rev_right_loop invg to.

Lemma actX : forall x a n, to x (a ^+ n) = iter n (to^~ a) x.

Lemma actCJ : forall a b x, to (to x a) b = to (to x b) (a ^ b).

Lemma actCJV : forall a b x, to (to x a) b = to (to x (b ^ a^-1)) a.

Lemma orbit_sym : forall G x y, (y \in orbit to G x) = (x \in orbit to G y).

Lemma orbit_trans : forall G x y z,
y \in orbit to G x -> z \in orbit to G y -> z \in orbit to G x.

Lemma orbit_transl : forall G x y,
y \in orbit to G x -> orbit to G y = orbit to G x.

Lemma orbit_transr : forall G x y z,
y \in orbit to G x -> (y \in orbit to G z) = (x \in orbit to G z).

Lemma orbit_eq_mem : forall G x y,
(orbit to G x == orbit to G y) = (x \in orbit to G y).

Lemma orbit_inv : forall A x y, (y \in orbit to A^-1 x) = (x \in orbit to A y).

Lemma orbit_lcoset : forall A a x, orbit to (a *: A) x = orbit to A (to x a).

Lemma orbit_rcoset : forall A a x y,
(to y a \in orbit to (A :* a) x) = (y \in orbit to A x).

Lemma orbit_conjsg : forall A a x y,
(to y a \in orbit to (A :^ a) (to x a)) = (y \in orbit to A x).

Lemma astabP : forall S a,
reflect (forall x, x \in S -> to x a = x) (a \in 'C(S | to)).

Lemma astab1P : forall x a, reflect (to x a = x) (a \in 'C[x | to]).

Lemma sub_astab1 : forall A x, (A \subset 'C[x | to]) = (x \in 'Fix_to(A)).

Lemma astabC : forall A S, (A \subset 'C(S | to)) = (S \subset 'Fix_to(A)).

Lemma afix_cycle : forall a, 'Fix_to(<[a]>) = 'Fix_to[a].

Lemma afix_gen : forall A, 'Fix_to(<<A>>) = 'Fix_to(A).

Lemma afixM : forall G H, 'Fix_to(G * H) = 'Fix_to(G) :&: 'Fix_to(H).

Lemma astabsP : forall S a,
reflect (forall x, (to x a \in S) = (x \in S)) (a \in 'N(S | to)).

Lemma card_orbit : forall G x, #|orbit to G x| = #|G : 'C_G[x | to]|.

Lemma dvdn_orbit : forall G x, #|orbit to G x| %| #|G|.

Lemma card_orbit_stab : forall G x,
(#|orbit to G x| * #|'C_G[x | to]|)%N = #|G|.

Lemma actsP : forall A S, reflect {acts A, on S | to} [acts A, on S | to].
Implicit Arguments actsP [A S].

Lemma setact_orbit : forall A x b,
to^* (orbit to A x) b = orbit to (A :^ b) (to x b).

Lemma astab_setact : forall S a, 'C(to^* S a | to) = 'C(S | to) :^ a.

Lemma astab1_act : forall x a, 'C[to x a | to] = 'C[x | to] :^ a.

Lemma atransP : forall G S, [transitive G, on S | to] ->
forall x, x \in S -> orbit to G x = S.

Lemma atransP2 : forall G S, [transitive G, on S | to] ->
{in S &, forall x y, exists2 a, a \in G & y = to x a}.

Lemma atrans_acts : forall G S,
[transitive G, on S | to] -> [acts G, on S | to].

Lemma atrans_supgroup : forall G H S,
G \subset H -> [transitive G, on S | to] ->
[transitive H, on S | to] = [acts H, on S | to].

Lemma atrans_acts_card : forall G S,
[transitive G, on S | to] =
[acts G, on S | to] && (#|orbit to G @: S| == 1%N).

Lemma atrans_dvd : forall G S, [transitive G, on S | to] -> #|S| %| #|G|.

 Aschbacher 5.2

Lemma acts_fix_norm : forall A B,
A \subset 'N(B) -> [acts A, on 'Fix_to(B) | to].

Lemma faithfulP : forall A S,
reflect (forall a, a \in A -> {in S, to^~ a =1 id} -> a = 1)
[faithful A, on S | to].

 This is the first part of Aschbacher (5.7)

Lemma astab_trans_gcore : forall G S u,
[transitive G, on S | to] -> u \in S -> 'C(S | to) = gcore 'C[u | to] G.

 Aschbacher 5.20

Theorem subgroup_transitiveP : forall G H S x,
x \in S -> H \subset G -> [transitive G, on S | to] ->
reflect ('C_G[x | to] * H = G) [transitive H, on S | to].

 Aschbacher 5.21

Lemma trans_subnorm_fixP : forall x G H S,
let C := 'C_G[x | to] in let T := 'Fix_(S | to)(H) in
[transitive G, on S | to] -> x \in S -> H \subset C ->
reflect ((H :^: G) ::&: C = H :^: C) [transitive 'N_G(H), on T | to].

End TotalActions.

Implicit Arguments astabP [aT rT to S a].
Implicit Arguments astab1P [aT rT to x a].
Implicit Arguments astabsP [aT rT to S a].
Implicit Arguments atransP [aT rT to G S].
Implicit Arguments actsP [aT rT to A S].
Implicit Arguments faithfulP [aT rT to A S].

Section Restrict.

Variables (aT : finGroupType) (D : {set aT}) (rT : Type).
Variables (to : action D rT) (A : {set aT}).

Definition ract of A \subset D := act to.

Variable sAD : A \subset D.

Lemma ract_is_action : is_action A (ract sAD).

Canonical Structure raction := Action ract_is_action.

Lemma ractE : raction =1 to.

 Other properties of raction need rT : finType; we defer them
until after the definition of actperm.


End Restrict.

Notation "to \ sAD" := (raction to sAD) (at level 50) : action_scope.

Section ActBy.

Variables (aT : finGroupType) (D : {set aT}) (rT : finType).

Definition actby_cond (A : {set aT}) R (to : action D rT) : Prop :=
[acts A, on R | to].

Definition actby A R to of actby_cond A R to :=
fun x a => if (x \in R) && (a \in A) then to x a else x.

Variables (A : {group aT}) (R : {set rT}) (to : action D rT).
Hypothesis nRA : actby_cond A R to.

Lemma actby_is_action : is_action A (actby nRA).

Canonical Structure action_by := Action actby_is_action.
Local Notation "<[nRA]>" := action_by : action_scope.

Lemma actbyE : forall x a, x \in R -> a \in A -> <[nRA]>%act x a = to x a.

Lemma afix_actby : forall B, 'Fix_<[nRA]>(B) = ~: R :|: 'Fix_to(A :&: B).

Lemma astab_actby : forall S, 'C(S | <[nRA]>) = 'C_A(R :&: S | to).

Lemma astabs_actby : forall S, 'N(S | <[nRA]>) = 'N_A(R :&: S | to).

Lemma acts_actby : forall (B : {set aT}) S,
[acts B, on S | <[nRA]>] = (B \subset A) && [acts B, on R :&: S | to].

End ActBy.

Notation "<[ nRA ] >" := (action_by nRA) : action_scope.

Section SubAction.

Variables (aT : finGroupType) (D : {group aT}).
Variables (rT : finType) (sP : pred rT) (sT : subFinType sP) (to : action D rT).
Implicit Type A : {set aT}.
Implicit Type u : sT.
Implicit Type S : {set sT}.

Definition subact_dom := 'N([set x | sP x] | to).
Canonical Structure subact_dom_group := [group of subact_dom].

Implicit Type Na : {a | a \in subact_dom}.
Lemma sub_act_proof : forall u Na, sP (to (val u) (val Na)).

Definition subact u a :=
if insub a is Some Na then Sub _ (sub_act_proof u Na) else u.

Lemma val_subact : forall u a,
val (subact u a) = if a \in subact_dom then to (val u) a else val u.

Lemma subact_is_action : is_action subact_dom subact.

Canonical Structure subaction := Action subact_is_action.

Lemma astab_subact : forall S,
'C(S | subaction) = subact_dom :&: 'C(val @: S | to).

Lemma astabs_subact : forall S,
'N(S | subaction) = subact_dom :&: 'N(val @: S | to).

Lemma afix_subact : forall A,
A \subset subact_dom -> 'Fix_subaction(A) = val @^-1: 'Fix_to(A).

End SubAction.

Notation "to ^?" := (subaction _ to)
(at level 2, format "to ^?") : action_scope.

Section QuotientAction.

Variables (aT : finGroupType) (D : {group aT}) (rT : finGroupType).
Variables (to : action D rT) (H : {group rT}).

Definition qact_dom := 'N(rcosets H 'N(H) | to^*).
Canonical Structure qact_dom_group := [group of qact_dom].

Local Notation subdom := (subact_dom (coset_range H) to^*).
Fact qact_subdomE : subdom = qact_dom.
Lemma qact_proof : qact_dom \subset subdom.

Definition qact : coset_of H -> aT -> coset_of H := act (to^*^? \ qact_proof).

Canonical Structure quotient_action := [action of qact].

Lemma acts_qact_dom : [acts qact_dom, on 'N(H) | to].

Lemma qactEcond : forall x a,
x \in 'N(H) ->
quotient_action (coset H x) a =
(if a \in qact_dom then coset H (to x a) else coset H x).

Lemma qactE : forall x a,
x \in 'N(H) -> a \in qact_dom ->
quotient_action (coset H x) a = coset H (to x a).

Lemma acts_quotient : forall (A : {set aT}) (B : {set rT}),
A \subset 'N_qact_dom(B | to) -> [acts A, on B / H | quotient_action].

Lemma astabs_quotient : forall G : {group rT},
H <| G -> 'N(G / H | quotient_action) = 'N_qact_dom(G | to).

End QuotientAction.

Notation "to / H" := (quotient_action to H) : action_scope.

Section ModAction.

Variables (aT : finGroupType) (D : {group aT}) (rT : finType).
Variable to : action D rT.
Implicit Type G : {group aT}.
Implicit Type S : {set rT}.

Section GenericMod.

Variable H : {group aT}.

Local Notation dom := 'N_D(H).
Local Notation range := 'Fix_to(D :&: H).
Let acts_dom : {acts dom, on range | to} := acts_act (acts_subnorm_fix to H).

Definition modact x (Ha : coset_of H) :=
if x \in range then to x (repr (D :&: Ha)) else x.

Lemma modactEcond : forall x a,
a \in dom -> modact x (coset H a) = (if x \in range then to x a else x).

Lemma modactE : forall x a,
a \in D -> a \in 'N(H) -> x \in range -> modact x (coset H a) = to x a.

Lemma modact_is_action : is_action (D / H) modact.

Canonical Structure mod_action := Action modact_is_action.

Section Stabilizers.

Variable S : {set rT}.
Hypothesis cSH : H \subset 'C(S | to).

Let fixSH : S \subset 'Fix_to(D :&: H).

Lemma astabs_mod : 'N(S | mod_action) = 'N(S | to) / H.

Lemma astab_mod : 'C(S | mod_action) = 'C(S | to) / H.

End Stabilizers.

Lemma afix_mod : forall G S,
H \subset 'C(S | to) -> G \subset 'N_D(H) ->
'Fix_(S | mod_action)(G / H) = 'Fix_(S | to)(G).

End GenericMod.

Lemma modact_faithful : forall G S,
[faithful G / 'C_G(S | to), on S | mod_action 'C_G(S | to)].

End ModAction.

Notation "to %% H" := (mod_action to H) : action_scope.

Section ActPerm.
 Morphism to permutations induced by an action.


Variables (aT : finGroupType) (D : {set aT}) (rT : finType).
Variable to : action D rT.

Definition actperm a := perm (act_inj to a).

Lemma actpermM : {in D &, {morph actperm : a b / a * b}}.

Canonical Structure actperm_morphism := Morphism actpermM.

Lemma actpermE : forall a x, actperm a x = to x a.

Lemma actpermK : forall x a, aperm x (actperm a) = to x a.

Lemma ker_actperm : 'ker actperm = 'C(setT | to).

End ActPerm.

Section RestrictActionTheory.

Variables (aT : finGroupType) (D : {set aT}) (rT : finType).
Variables (to : action D rT).

Lemma faithful_isom : forall (A : {group aT}) S (nSA : actby_cond A S to),
[faithful A, on S | to] -> isom A (actperm <[nSA]> @* A) (actperm <[nSA]>).

Variables (A : {set aT}) (sAD : A \subset D).

Lemma ractpermE : actperm (to \ sAD) =1 actperm to.

Lemma afix_ract : forall B, 'Fix_(to \ sAD)(B) = 'Fix_to(B).

Lemma astab_ract : forall S, 'C(S | to \ sAD) = 'C_A(S | to).

Lemma astabs_ract : forall S, 'N(S | to \ sAD) = 'N_A(S | to).

Lemma acts_ract : forall (B : {set aT}) S,
[acts B, on S | to \ sAD] = (B \subset A) && [acts B, on S | to].

End RestrictActionTheory.

Section MorphAct.
 Action induced by a morphism to permutations.


Variables (aT : finGroupType) (D : {group aT}) (rT : finType).
Variable phi : {morphism D >-> {perm rT}}.

Definition mact x a := phi a x.

Lemma mact_is_action : is_action D mact.

Canonical Structure morph_action := Action mact_is_action.

Lemma mactE : forall x a, morph_action x a = phi a x.

Lemma injm_faithful : 'injm phi -> [faithful D, on setT | morph_action].

Lemma perm_mact : forall a, actperm morph_action a = phi a.

End MorphAct.

Notation "<< phi >>" := (morph_action phi) : action_scope.

Section CompAct.

Variables (gT aT : finGroupType) (rT : finType).
Variables (D : {set aT}) (to : action D rT).
Variables (B : {set gT}) (f : {morphism B >-> aT}).

Definition comp_act x e := to x (f e).
Lemma comp_is_action : is_action (f @*^-1 D) comp_act.
Canonical Structure comp_action := Action comp_is_action.

Lemma comp_actE : forall x e, comp_action x e = to x (f e).

Lemma afix_comp : forall A : {set gT},
A \subset B -> 'Fix_comp_action(A) = 'Fix_to(f @* A).

Lemma astab_comp : forall S, 'C(S | comp_action) = f @*^-1 'C(S | to).

Lemma astabs_comp : forall S, 'N(S | comp_action) = f @*^-1 'N(S | to).

End CompAct.

Notation "to \o f" := (comp_action to f) : action_scope.

Section PermAction.
  Natural action of permutation groups.


Variable rT : finType.
Local Notation gT := {perm rT}.
Implicit Types a b c : gT.

Lemma aperm_is_action : is_action setT (@aperm rT).

Canonical Structure perm_action := Action aperm_is_action.

Lemma pcycleE : forall a, pcycle a = orbit perm_action <[a]>%g.

Lemma perm_act1P : forall a, reflect (forall x, aperm x a = x) (a == 1).

Lemma perm_faithful : forall A, [faithful A, on setT | perm_action].

Lemma actperm_id : forall p, actperm perm_action p = p.

End PermAction.

Implicit Arguments perm_act1P [rT a].

Notation "'P" := (perm_action _) (at level 0) : action_scope.

Section ActpermOrbits.

Variables (aT : finGroupType) (D : {group aT}) (rT : finType).
Variable to : action D rT.

Lemma orbit_morphim_actperm : forall A : {set aT},
A \subset D -> orbit 'P (actperm to @* A) =1 orbit to A.

Lemma pcycle_actperm : forall a : aT,
a \in D -> pcycle (actperm to a) =1 orbit to <[a]>.

End ActpermOrbits.

Section RestrictPerm.

Variables (T : finType) (S : {set T}).

Definition restr_perm := actperm (<[subxx 'N(S | 'P)]>).
Canonical Structure restr_perm_morphism := [morphism of restr_perm].

Lemma restr_perm_on : forall p, perm_on S (restr_perm p).

Lemma triv_restr_perm : forall p, p \notin 'N(S | 'P) -> restr_perm p = 1.

Lemma restr_permE : {in 'N(S | 'P) & S, forall p, restr_perm p =1 p}.

Lemma ker_restr_perm : 'ker restr_perm = 'C(S | 'P).

Lemma im_restr_perm : forall p, restr_perm p @: S = S.

End RestrictPerm.

Section AutIn.

Variable gT : finGroupType.

Definition Aut_in A (B : {set gT}) := 'N_A(B | 'P) / 'C_A(B | 'P).

Variables G H : {group gT}.
Hypothesis sHG: H \subset G.

Lemma Aut_restr_perm : forall a, a \in Aut G -> restr_perm H a \in Aut H.

Lemma restr_perm_Aut : restr_perm H @* Aut G \subset Aut H.

Lemma Aut_in_isog : Aut_in (Aut G) H \isog restr_perm H @* Aut G.

Lemma Aut_sub_fullP :
reflect (forall h : {morphism H >-> gT}, 'injm h -> h @* H = H ->
exists g : {morphism G >-> gT},
[/\ 'injm g, g @* G = G & {in H, g =1 h}])
(Aut_in (Aut G) H \isog Aut H).

End AutIn.

Section InjmAutIn.

Variables (gT rT : finGroupType) (D G H : {group gT}) (f : {morphism D >-> rT}).
Hypotheses (injf : 'injm f) (sGD : G \subset D) (sHG : H \subset G).
Local Notation fGisom := (Aut_isom injf sGD).
Local Notation fHisom := (Aut_isom injf sHD).
Local Notation inH := (restr_perm H).
Local Notation infH := (restr_perm (f @* H)).

Lemma astabs_Aut_isom : forall a,
a \in Aut G -> (fGisom a \in 'N(f @* H | 'P)) = (a \in 'N(H | 'P)).

Lemma isom_restr_perm : forall a,
a \in Aut G -> fHisom (inH a) = infH (fGisom a).

Lemma restr_perm_isom : isom (inH @* Aut G) (infH @* Aut (f @* G)) fHisom.

Lemma injm_Aut_sub : Aut_in (Aut (f @* G)) (f @* H) \isog Aut_in (Aut G) H.

Lemma injm_Aut_full :
(Aut_in (Aut (f @* G)) (f @* H) \isog Aut (f @* H))
= (Aut_in (Aut G) H \isog Aut H).

End InjmAutIn.

Section GroupAction.

Variables (aT rT : finGroupType) (D : {set aT}) (R : {set rT}).
Local Notation actT := (action D rT).

Definition is_groupAction (to : actT) :=
{in D, forall a, actperm to a \in Aut R}.

Structure groupAction := GroupAction {gact :> actT; _ : is_groupAction gact}.

Definition clone_groupAction to :=
let: GroupAction _ toA := to return {type of GroupAction for to} -> _ in
fun k => k toA : groupAction.

End GroupAction.

Delimit Scope groupAction_scope with gact.

Notation "[ 'groupAction' 'of' to ]" :=
(clone_groupAction (@GroupAction _ _ _ _ to))
(at level 0, format "[ 'groupAction' 'of' to ]") : form_scope.

Section GroupActionDefs.

Variables (aT rT : finGroupType) (D : {set aT}) (R : {set rT}).
Implicit Type A : {set aT}.
Implicit Type S : {set rT}.
Implicit Type to : groupAction D R.

Definition gact_range of groupAction D R := R.

Definition gacent to A := 'Fix_(R | to)(D :&: A).

Definition acts_on_group A S to := [acts A, on S | to] /\ S \subset R.

Coercion actby_cond_group A S to : acts_on_group A S to -> actby_cond A S to :=
@proj1 _ _.

Definition acts_irreducibly A S to :=
[min S of G | (G :!=: 1) && [acts A, on G | to]].

End GroupActionDefs.

Notation "''C_' ( | to ) ( A )" := (gacent to A)
(at level 8, format "''C_' ( | to ) ( A )") : group_scope.
Notation "''C_' ( G | to ) ( A )" := (G :&: 'C_(|to)(A))
(at level 8, format "''C_' ( G | to ) ( A )") : group_scope.
Notation "''C_' ( | to ) [ a ]" := 'C_(|to)([set a])
(at level 8, format "''C_' ( | to ) [ a ]") : group_scope.
Notation "''C_' ( G | to ) [ a ]" := 'C_(G | to)([set a])
(at level 8, format "''C_' ( G | to ) [ a ]") : group_scope.

Notation "{ 'acts' A , 'on' 'group' G | to }" := (acts_on_group A G to)
(at level 0, format "{ 'acts' A , 'on' 'group' G | to }") : form_scope.

Section RawGroupAction.

Variables (aT rT : finGroupType) (D : {set aT}) (R : {set rT}).
Variable to : groupAction D R.

Lemma actperm_Aut : is_groupAction R to.

Lemma im_actperm_Aut : actperm to @* D \subset Aut R.

Lemma gact_out : forall x a, a \in D -> x \notin R -> to x a = x.

Lemma gactM : {in D, forall a, {in R &, {morph to^~ a : x y / x * y}}}.

Lemma actmM : forall a, {in R &, {morph actm to a : x y / x * y}}.

Canonical Structure act_morphism a := Morphism (actmM a).

Lemma morphim_actm :
{in D, forall a (S : {set rT}), S \subset R -> actm to a @* S = to^* S a}.

Variables (a : aT) (A B : {set aT}) (S : {set rT}).

Lemma gacentIdom : 'C_(|to)(D :&: A) = 'C_(|to)(A).

Lemma gacentIim : 'C_(R | to)(A) = 'C_(|to)(A).

Lemma gacentS : A \subset B -> 'C_(|to)(B) \subset 'C_(|to)(A).

Lemma gacentU : 'C_(|to)(A :|: B) = 'C_(|to)(A) :&: 'C_(|to)(B).

Hypotheses (Da : a \in D) (sAD : A \subset D) (sSR : S \subset R).

Lemma gacentE : 'C_(|to)(A) = 'Fix_(R | to)(A).

Lemma gacent1E : 'C_(|to)[a] = 'Fix_(R | to)[a].

Lemma subgacentE : 'C_(S | to)(A) = 'Fix_(S | to)(A).

Lemma subgacent1E : 'C_(S | to)[a] = 'Fix_(S | to)[a].

End RawGroupAction.

Section GroupActionTheory.

Variables aT rT : finGroupType.
Variables (D : {group aT}) (R : {group rT}) (to : groupAction D R).
Implicit Type A B : {set aT}.
Implicit Types G H : {group aT}.
Implicit Type S : {set rT}.
Implicit Types M N : {group rT}.

Lemma gact1 : {in D, forall a, to 1 a = 1}.

Lemma gactV : {in D, forall a, {in R, {morph to^~ a : x / x^-1}}}.

Lemma gactX : {in D, forall a n, {in R, {morph to^~ a : x / x ^+ n}}}.

Lemma gactJ : {in D, forall a, {in R &, {morph to^~ a : x y / x ^ y}}}.

Lemma gactR : {in D, forall a, {in R &, {morph to^~ a : x y / [~ x, y]}}}.

Lemma gact_stable : {acts D, on R | to}.

Lemma group_set_gacent : forall A, group_set 'C_(|to)(A).

Canonical Structure gacent_group A := Group (group_set_gacent A).

Lemma gacent1 : 'C_(|to)(1) = R.

Lemma gacent_gen : forall A, A \subset D -> 'C_(|to)(<<A>>) = 'C_(|to)(A).

Lemma gacentD1 : forall A, 'C_(|to)(A^#) = 'C_(|to)(A).

Lemma gacent_cycle : forall a, a \in D -> 'C_(|to)(<[a]>) = 'C_(|to)[a].

Lemma gacentY : forall A B,
A \subset D -> B \subset D -> 'C_(|to)(A <*> B) = 'C_(|to)(A) :&: 'C_(|to)(B).

Lemma gacentM : forall G H,
G \subset D -> H \subset D -> 'C_(|to)(G * H) = 'C_(|to)(G) :&: 'C_(|to)(H).

Lemma astab1 : 'C(1 | to) = D.

Lemma astab_range : 'C(R | to) = 'C(setT | to).

Lemma gacentC : forall A S,
A \subset D -> S \subset R ->
(S \subset 'C_(|to)(A)) = (A \subset 'C(S | to)).

Lemma astab_gen : forall S, S \subset R -> 'C(<<S>> | to) = 'C(S | to).

Lemma astabM : forall M N,
M \subset R -> N \subset R -> 'C(M * N | to) = 'C(M | to) :&: 'C(N | to).

Lemma astabs1 : 'N(1 | to) = D.

Lemma astabs_range : 'N(R | to) = D.

Lemma astabsD1 : forall S, 'N(S^# | to) = 'N(S | to).

Lemma gacts_range : forall A, A \subset D -> {acts A, on group R | to}.

Lemma acts_subnorm_gacent : forall A,
A \subset D -> [acts 'N_D(A), on 'C_(| to)(A) | to].

Lemma acts_subnorm_subgacent : forall A B S,
A \subset D -> [acts B, on S | to] -> [acts 'N_B(A), on 'C_(S | to)(A) | to].

Lemma acts_gen : forall A S,
S \subset R -> [acts A, on S | to] -> [acts A, on <<S>> | to].

Lemma acts_joing : forall A M N,
M \subset R -> N \subset R -> [acts A, on M | to] -> [acts A, on N | to] ->
[acts A, on M <*> N | to].

Lemma injm_actm : forall a, 'injm (actm to a).

Lemma im_actm : forall a, actm to a @* R = R.

Lemma acts_char : forall G M, G \subset D -> M \char R -> [acts G, on M | to].

Lemma gacts_char : forall G M,
G \subset D -> M \char R -> {acts G, on group M | to}.

Section Restrict.

Variables (A : {group aT}) (sAD : A \subset D).

Lemma ract_is_groupAction : is_groupAction R (to \ sAD).

Canonical Structure ract_groupAction := GroupAction ract_is_groupAction.

Lemma gacent_ract : forall B, 'C_(|ract_groupAction)(B) = 'C_(|to)(A :&: B).

End Restrict.

Section ActBy.

Variables (A : {group aT}) (G : {group rT}) (nGAg : {acts A, on group G | to}).

Lemma actby_is_groupAction : is_groupAction G <[nGAg]>.

Canonical Structure actby_groupAction := GroupAction actby_is_groupAction.

Lemma gacent_actby : forall B,
'C_(|actby_groupAction)(B) = 'C_(G | to)(A :&: B).

End ActBy.

Section Quotient.

Variable H : {group rT}.

Lemma acts_qact_dom_norm : {acts qact_dom to H, on 'N(H) | to}.

Lemma qact_is_groupAction : is_groupAction (R / H) (to / H).

Canonical Structure quotient_groupAction := GroupAction qact_is_groupAction.

Lemma qact_domE : H \subset R -> qact_dom to H = 'N(H | to).

End Quotient.

Section Mod.

Variable H : {group aT}.

Lemma modact_is_groupAction : is_groupAction 'C_(|to)(H) (to %% H).

Canonical Structure mod_groupAction := GroupAction modact_is_groupAction.

Lemma modgactE : forall x a,
H \subset 'C(R | to) -> a \in 'N_D(H) -> (to %% H)%act x (coset H a) = to x a.

Lemma gacent_mod : forall G M,
H \subset 'C(M | to) -> G \subset 'N(H) ->
'C_(M | mod_groupAction)(G / H) = 'C_(M | to)(G).

Lemma acts_irr_mod : forall G M,
H \subset 'C(M | to) -> G \subset 'N(H) -> acts_irreducibly G M to ->
acts_irreducibly (G / H) M mod_groupAction.

End Mod.

Lemma modact_coset_astab : forall x a,
a \in D -> (to %% 'C(R | to))%act x (coset _ a) = to x a.

Lemma acts_irr_mod_astab : forall G M,
acts_irreducibly G M to ->
acts_irreducibly (G / 'C_G(M | to)) M (mod_groupAction _).

Section CompAct.

Variables (gT : finGroupType) (G : {group gT}) (f : {morphism G >-> aT}).

Lemma comp_is_groupAction : is_groupAction R (comp_action to f).
Canonical Structure comp_groupAction := GroupAction comp_is_groupAction.

Lemma gacent_comp : forall U, 'C_(|comp_groupAction)(U) = 'C_(|to)(f @* U).

End CompAct.

End GroupActionTheory.

Notation "''C_' ( | to ) ( A )" := (gacent_group to A) : subgroup_scope.
Notation "''C_' ( G | to ) ( A )" :=
(setI_group G 'C_(|to)(A)) : subgroup_scope.
Notation "''C_' ( | to ) [ a ]" := (gacent_group to [set a%g]) : subgroup_scope.
Notation "''C_' ( G | to ) [ a ]" :=
(setI_group G 'C_(|to)[a]) : subgroup_scope.

Notation "to \ sAD" := (ract_groupAction to sAD) : groupAction_scope.
Notation "<[ nGA ] >" := (actby_groupAction nGA) : groupAction_scope.
Notation "to / H" := (quotient_groupAction to H) : groupAction_scope.
Notation "to %% H" := (mod_groupAction to H) : groupAction_scope.
Notation "to \o f" := (comp_groupAction to f) : groupAction_scope.

 Conjugation and right translation actions.


Section InternalActionDefs.

Variable gT : finGroupType.
Implicit Type A : {set gT}.
Implicit Type G : {group gT}.

 This is not a Canonical Structure because it is seldom used, and it would
cause too many spurious matches (any group product would be viewed as an
action!).

Definition mulgr_action := TotalAction (@mulg1 gT) (@mulgA gT).

Canonical Structure conjg_action := TotalAction (@conjg1 gT) (@conjgM gT).

Lemma conjg_is_groupAction : is_groupAction setT conjg_action.

Canonical Structure conjg_groupAction := GroupAction conjg_is_groupAction.

Lemma rcoset_is_action : is_action setT (@rcoset gT).

Canonical Structure rcoset_action := Action rcoset_is_action.

Canonical Structure conjsg_action := TotalAction (@conjsg1 gT) (@conjsgM gT).

Lemma conjG_is_action : is_action setT (@conjG_group gT).

Definition conjG_action := Action conjG_is_action.

End InternalActionDefs.

Notation "'R" := (@mulgr_action _) (at level 0) : action_scope.
Notation "'Rs" := (@rcoset_action _) (at level 0) : action_scope.
Notation "'J" := (@conjg_action _) (at level 0) : action_scope.
Notation "'J" := (@conjg_groupAction _) (at level 0) : groupAction_scope.
Notation "'Js" := (@conjsg_action _) (at level 0) : action_scope.
Notation "'JG" := (@conjG_action _) (at level 0) : action_scope.
Notation "'Q" := ('J / _)%act (at level 0) : action_scope.
Notation "'Q" := ('J / _)%gact (at level 0) : groupAction_scope.

Section InternalGroupAction.

Variable gT : finGroupType.
Implicit Types A B : {set gT}.
Implicit Types G H : {group gT}.
Implicit Type x : gT.

  Various identities for actions on groups.


Lemma orbitR : forall G x, orbit 'R G x = x *: G.

Lemma astab1R : forall x, 'C[x | 'R] = 1.

Lemma astabR : forall G, 'C(G | 'R) = 1.

Lemma astabsR : forall G, 'N(G | 'R) = G.

Lemma atransR : forall G, [transitive G, on G | 'R].

Lemma faithfulR : forall G, [faithful G, on G | 'R].

Definition Cayley_repr G := actperm <[atrans_acts (atransR G)]>.

Theorem Cayley_isom : forall G, isom G (Cayley_repr G @* G) (Cayley_repr G).

Theorem Cayley_isog : forall G, G \isog Cayley_repr G @* G.

Lemma orbitJ : forall G x, orbit 'J G x = x ^: G.

Lemma afixJ : forall A, 'Fix_'J(A) = 'C(A).

Lemma astabJ : forall A, 'C(A |'J) = 'C(A).

Lemma astab1J : forall x, 'C[x |'J] = 'C[x].

Lemma astabsJ : forall A, 'N(A | 'J) = 'N(A).

Lemma setactJ : forall A x, 'J^*%act A x = A :^ x.

Lemma gacentJ : forall A, 'C_(|'J)(A) = 'C(A).

Lemma orbitRs : forall G A, orbit 'Rs G A = rcosets A G.

Lemma sub_afixRs_norms : forall G x A,
(G :* x \in 'Fix_'Rs(A)) = (A \subset G :^ x).

Lemma sub_afixRs_norm : forall G x, (G :* x \in 'Fix_'Rs(G)) = (x \in 'N(G)).

Lemma afixRs_rcosets : forall A G,
'Fix_(rcosets G A | 'Rs)(G) = rcosets G 'N_A(G).

Lemma astab1Rs : forall G, 'C[G : {set gT} | 'Rs] = G.

Lemma actsRs_rcosets : forall H G, [acts G, on rcosets H G | 'Rs].

Lemma transRs_rcosets : forall H G, [transitive G, on rcosets H G | 'Rs].

 This is the second part of Aschbacher (5.7)

Lemma astabRs_rcosets : forall H G, 'C(rcosets H G | 'Rs) = gcore H G.

Lemma orbitJs : forall G A, orbit 'Js G A = A :^: G.

Lemma astab1Js : forall A, 'C[A | 'Js] = 'N(A).

Lemma card_conjugates : forall A G, #|A :^: G| = #|G : 'N_G(A)|.

Lemma afixJG : forall G A, (G \in 'Fix_'JG(A)) = (A \subset 'N(G)).

Lemma astab1JG : forall G, 'C[G | 'JG] = 'N(G).

Lemma dom_qactJ : forall H, qact_dom 'J H = 'N(H).

Lemma qactJ : forall H (Hy : coset_of H) x,
'Q%act Hy x = if x \in 'N(H) then Hy ^ coset H x else Hy.

Lemma actsQ : forall A B H,
A \subset 'N(H) -> A \subset 'N(B) -> [acts A, on B / H | 'Q].

Lemma astabsQ : forall G H, H <| G -> 'N(G / H | 'Q) = 'N(H) :&: 'N(G).

Lemma astabQ : forall H Abar, 'C(Abar |'Q) = coset H @*^-1 'C(Abar).

Lemma sub_astabQ : forall A H Bbar,
(A \subset 'C(Bbar | 'Q)) = (A \subset 'N(H)) && (A / H \subset 'C(Bbar)).

Lemma sub_astabQR : forall A B H,
A \subset 'N(H) -> B \subset 'N(H) ->
(A \subset 'C(B / H | 'Q)) = ([~: A, B] \subset H).

Lemma astabQR : forall A H, A \subset 'N(H) ->
'C(A / H | 'Q) = [set x \in 'N(H) | [~: [set x], A] \subset H].

Lemma quotient_astabQ : forall H Abar, 'C(Abar | 'Q) / H = 'C(Abar).

Section CardClass.

Variable G : {group gT}.

Lemma index_cent1 : forall x, #|G : 'C_G[x]| = #|x ^: G|.

Lemma sum_card_class : \sum_(C \in classes G) #|C| = #|G|.

Lemma class_formula : \sum_(C \in classes G) #|G : 'C_G[repr C]| = #|G|.

Lemma card_classes_abelian : abelian G -> #|classes G| = #|G|.

End CardClass.

 This is proved by more elementary means in groups.v
Lemma index2_normal : forall G H, H \subset G -> #|G : H| = 2 -> H <| G.
Proof.
move=> G H sHG indexHG; rewrite /normal sHG; apply/subsetP=> x Gx.
case Hx: (x \in H); first by rewrite inE conjGid.
have defHx: [set H :* x] = rcosets H G :\ gval H.
apply/eqP; rewrite eqEcard sub1set !inE cards1 -rcosetE mem_orbit //=.
rewrite (sameP eqP afix1P) -sub_astab1 astab1Rs sub1set Hx /=.
by rewrite -ltnS -indexHG [#|G : H|](cardsD1 (gval H)) orbit_refl.
rewrite -sub_afixRs_norm -sub_astab1 -astabs_set1 defHx.
by rewrite actsD ?astabs_set1 ?astab1Rs // (subset_trans sHG) ?actsRs_rcosets.
Qed.



End InternalGroupAction.

Lemma gacentQ : forall (gT : finGroupType) (H : {group gT}) (A : {set gT}),
'C_(|'Q)(A) = 'C(A / H).

Section AutAct.

Variable (gT : finGroupType) (G : {set gT}).

Definition autact := act ('P \ subsetT (Aut G)).
Canonical Structure aut_action := [action of autact].

Lemma autactK : forall a, actperm aut_action a = a.

Lemma autact_is_groupAction : is_groupAction G aut_action.
Canonical Structure aut_groupAction := GroupAction autact_is_groupAction.

End AutAct.

Notation "[ 'Aut' G ]" := (aut_action G) : action_scope.
Notation "[ 'Aut' G ]" := (aut_groupAction G) : groupAction_scope.