# Library mathcomp.fingroup.action

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.                                  *)

Require Import mathcomp.ssreflect.ssreflect.

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 == constructs 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. orbit_transversal to A S == a transversal of the partition orbit to A @: S of S, provided A acts on S via to. amove to A x y == the set of a in A whose action sends x to y. 'C_A[x | to] == the stabiliser of x : rT in A :&: D. 'C_A(S | to) == the pointwise 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 (_ * _). (However, 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), but %act can be 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 automorphism 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.

Set Implicit Arguments.

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 := a b, to x (a × b) = to (to x a) b.

Definition is_action to :=
left_injective to 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 kk 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 : 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 :=
x a, f (to x a) = to' (f x) (fA a).

Variable rT : finType. (* Most definitions require a finType structure on rT *)
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 in 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, 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 [1].

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) (x y : rT) (A B : {set aT}) (S T : {set rT}).

Lemma act_inj : left_injective to.
Implicit Arguments act_inj [].

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

Lemma actmEfun a : a \in D actm to a = to^~ a.

Lemma actmE a : a \in D actm to a =1 to^~ a.

Lemma setactE S a : to^* S a = [set to x a | x in S].

Lemma mem_setact S a x : x \in S to x a \in to^* S a.

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

Lemma setact_is_action : is_action D to^*.

Canonical set_action := Action setact_is_action.

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

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

Lemma mem_orbit A x a : a \in A to x a \in orbit to A x.

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

Lemma afixS A B : A \subset B 'Fix_to(B) \subset 'Fix_to(A).

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

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

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

Lemma astab_dom S : {subset 'C(S | to) D}.

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

Lemma astabS S1 S2 : S1 \subset S2 'C(S2 | to) \subset 'C(S1 | to).

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

Lemma astabs_dom S : {subset 'N(S | to) D}.

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

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

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

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

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

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

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

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

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

Lemma astabCin 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 A S x y :
[acts A, on S | to] y \in orbit to A x x \in S y \in S.

Lemma subset_faithful 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 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 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 x : to x 1 = x.

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

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

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

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

Lemma afix1 : 'Fix_to(1) = setT.

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

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

Lemma contra_orbit G x y : x \notin orbit to G y x != y.

Lemma orbit_in_sym G : G \subset D symmetric (orbit_rel G).

Lemma orbit_in_trans G : G \subset D transitive (orbit_rel G).

Lemma orbit_in_eqP G x y :
G \subset D reflect (orbit to G x = orbit to G y) (x \in orbit to G y).

Lemma orbit_in_transl 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_act_in x a G :
G \subset D a \in G orbit to G (to x a) = orbit to G x.

Lemma orbit_actr_in x a G y :
G \subset D a \in G (to y a \in orbit to G x) = (y \in orbit to G x).

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

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

Lemma orbit_rcoset_in 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 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 G x : reflect (orbit to G x = [set x]) (x \in 'Fix_to(G)).

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

Lemma orbit_partition G S :
[acts G, on S | to] partition (orbit to G @: S) S.

Definition orbit_transversal A S := transversal (orbit to A @: S) S.

Lemma orbit_transversalP G S (P := orbit to G @: S)
(X := orbit_transversal G S) :
[acts G, on S | to]
[/\ is_transversal X P S, X \subset S,
{in X &, x y, (y \in orbit to G x) = (x == y)}
& x, x \in S exists2 a, a \in G & to x a \in X].

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

Canonical astab_group S := group (group_set_astab S).

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

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

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

Lemma afixMin G H :
G \subset D H \subset D 'Fix_to(G × H) = 'Fix_to(G) :&: 'Fix_to(H).

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

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

Canonical astabs_group S := group (group_set_astabs S).

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

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

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

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

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

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

Section OrbitStabilizer.

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

Lemma amove_act 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 Cato x (repr Ca))}.

Lemma orbit_stabilizer :
orbit to G x = [set to x (repr Ca) | Ca in 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 G x : G \subset D #|orbit to G x| = #|G : 'C_G[x | to]|.

Lemma card_orbit_in_stab G x :
G \subset D (#|orbit to G x| × #|'C_G[x | to]|)%N = #|G|.

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

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

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

Theorem Frobenius_Cauchy 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 G S :
G \subset D [transitive G, on S | to] #|S| %| #|G : 'C_G(S | to)|.

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

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

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

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

Lemma subgroup_transitivePin 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 orbit_in_eqP [aT D rT to G x y].
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) : Group_scope.
Notation "''C_' A ( S | to )" := (setI_group A 'C(S | to)) : Group_scope.
Notation "''C_' ( A ) ( S | to )" := (setI_group A 'C(S | to))
(only parsing) : Group_scope.
Notation "''C' [ x | to ]" := (astab_group to [set x%g]) : Group_scope.
Notation "''C_' A [ x | to ]" := (setI_group A 'C[x | to]) : Group_scope.
Notation "''C_' ( A ) [ x | to ]" := (setI_group A 'C[x | to])
(only parsing) : Group_scope.
Notation "''N' ( S | to )" := (astabs_group to S) : Group_scope.
Notation "''N_' A ( S | to )" := (setI_group A 'N(S | to)) : Group_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) (x y z : rT) (A B : {set aT}) (G H : {group aT}).
Implicit Type S : {set rT}.

Lemma actM 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 x a n : to x (a ^+ n) = iter n (to^~ a) x.

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

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

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

Lemma orbit_trans G x y z :
x \in orbit to G y y \in orbit to G z x \in orbit to G z.

Lemma orbit_eqP G x y :
reflect (orbit to G x = orbit to G y) (x \in orbit to G y).

Lemma orbit_transl G x y z :
y \in orbit to G x (y \in orbit to G z) = (x \in orbit to G z).

Lemma orbit_act G a x: a \in G orbit to G (to x a) = orbit to G x.

Lemma orbit_actr G a x y :
a \in G (to y a \in orbit to G x) = (y \in orbit to G x).

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

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

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

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

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

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

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

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

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

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

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

Lemma afixM G H : 'Fix_to(G × H) = 'Fix_to(G) :&: 'Fix_to(H).

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

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

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

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

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

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

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

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

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

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

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

Lemma atrans_supgroup 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 G S :
[transitive G, on S | to] =
[acts G, on S | to] && (#|orbit to G @: S| == 1%N).

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

This is Aschbacher (5.2)
Lemma acts_fix_norm A B : A \subset 'N(B) [acts A, on 'Fix_to(B) | to].

Lemma faithfulP A S :
reflect ( 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)
This is Aschbacher (5.20)
This is Aschbacher (5.21)
Lemma trans_subnorm_fixP 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 orbit_eqP [aT rT to G x y].
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 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 aif (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 action_by := Action actby_is_action.

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

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

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

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

Lemma acts_actby (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 subact_dom_group := [group of subact_dom].

Implicit Type Na : {a | a \in subact_dom}.
Lemma sub_act_proof 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 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 subaction := Action subact_is_action.

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

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

Lemma afix_subact 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 qact_dom_group := [group of qact_dom].

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 quotient_action := [action of qact].

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

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

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

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

Lemma astabs_quotient (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 Types (G : {group aT}) (S : {set rT}).

Section GenericMod.

Variable H : {group aT}.

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 x a :
a \in dom modact x (coset H a) = (if x \in range then to x a else x).

Lemma modactE 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 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 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 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 actperm_morphism := Morphism actpermM.

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

Lemma actpermK 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 (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 B : 'Fix_(to \ sAD)(B) = 'Fix_to(B).

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

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

Lemma acts_ract (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 morph_action := Action mact_is_action.

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

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

Lemma perm_mact 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 comp_action := Action comp_is_action.

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

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

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

Lemma astabs_comp 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.
Implicit Types a b c : gT.

Lemma aperm_is_action : is_action setT (@aperm rT).

Canonical perm_action := Action aperm_is_action.

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

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

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

Lemma actperm_id p : actperm perm_action p = p.

End PermAction.

Implicit Arguments perm_act1P [rT a].

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

Section ActpermOrbits.

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

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

Lemma pcycle_actperm (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 restr_perm_morphism := [morphism of restr_perm].

Lemma restr_perm_on p : perm_on S (restr_perm p).

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

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

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

Lemma im_restr_perm 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 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 ( h : {morphism H >-> gT}, 'injm h h @* H = H
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).
Let sHD := subset_trans sHG sGD.

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

Lemma isom_restr_perm 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}).

Definition is_groupAction (to : actT) :=
{in D, 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 kk 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 x a : a \in D x \notin R to x a = x.

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

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

Canonical act_morphism a := Morphism (actmM a).

Lemma morphim_actm :
{in D, 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, a, to 1 a = 1}.

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

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

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

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

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

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

Canonical gacent_group A := Group (group_set_gacent A).

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

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

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

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

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

Lemma gacentM 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 A S :
A \subset D S \subset R
(S \subset 'C_(|to)(A)) = (A \subset 'C(S | to)).

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

Lemma astabM 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 S : 'N(S^# | to) = 'N(S | to).

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

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

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

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

Lemma acts_joing 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 a : 'injm (actm to a).

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

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

Lemma gacts_char 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 ract_groupAction := GroupAction ract_is_groupAction.

Lemma gacent_ract 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 actby_groupAction := GroupAction actby_is_groupAction.

Lemma gacent_actby 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 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 mod_groupAction := GroupAction modact_is_groupAction.

Lemma modgactE 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 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 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 x a :
a \in D (to %% 'C(R | to))%act x (coset _ a) = to x a.

Lemma acts_irr_mod_astab 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 comp_groupAction := GroupAction comp_is_groupAction.

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

End CompAct.

End GroupActionTheory.

Notation "''C_' ( | to ) ( A )" := (gacent_group to A) : Group_scope.
Notation "''C_' ( G | to ) ( A )" :=
(setI_group G 'C_(|to)(A)) : Group_scope.
Notation "''C_' ( | to ) [ a ]" := (gacent_group to [set a%g]) : Group_scope.
Notation "''C_' ( G | to ) [ a ]" :=
(setI_group G 'C_(|to)[a]) : Group_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.

Operator group isomorphism.
Section MorphAction.

Variables (aT1 aT2 : finGroupType) (rT1 rT2 : finType).
Variables (D1 : {group aT1}) (D2 : {group aT2}).
Variables (to1 : action D1 rT1) (to2 : action D2 rT2).
Variables (A : {set aT1}) (R S : {set rT1}).
Variables (h : rT1 rT2) (f : {morphism D1 >-> aT2}).
Hypotheses (actsDR : {acts D1, on R | to1}) (injh : {in R &, injective h}).
Hypothesis defD2 : f @* D1 = D2.
Hypotheses (sSR : S \subset R) (sAD1 : A \subset D1).
Hypothesis hfJ : {in S & D1, morph_act to1 to2 h f}.

Lemma morph_astabs : f @* 'N(S | to1) = 'N(h @: S | to2).

Lemma morph_astab : f @* 'C(S | to1) = 'C(h @: S | to2).

Lemma morph_afix : h @: 'Fix_(S | to1)(A) = 'Fix_(h @: S | to2)(f @* A).

End MorphAction.

Section MorphGroupAction.

Variables (aT1 aT2 rT1 rT2 : finGroupType).
Variables (D1 : {group aT1}) (D2 : {group aT2}).
Variables (R1 : {group rT1}) (R2 : {group rT2}).
Variables (to1 : groupAction D1 R1) (to2 : groupAction D2 R2).
Variables (h : {morphism R1 >-> rT2}) (f : {morphism D1 >-> aT2}).
Hypotheses (iso_h : isom R1 R2 h) (iso_f : isom D1 D2 f).
Hypothesis hfJ : {in R1 & D1, morph_act to1 to2 h f}.
Implicit Types (A : {set aT1}) (S : {set rT1}) (M : {group rT1}).

Lemma morph_gastabs S : S \subset R1 f @* 'N(S | to1) = 'N(h @* S | to2).

Lemma morph_gastab S : S \subset R1 f @* 'C(S | to1) = 'C(h @* S | to2).

Lemma morph_gacent A : A \subset D1 h @* 'C_(|to1)(A) = 'C_(|to2)(f @* A).

Lemma morph_gact_irr A M :
A \subset D1 M \subset R1
acts_irreducibly (f @* A) (h @* M) to2 = acts_irreducibly A M to1.

End MorphGroupAction.

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 action 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 conjg_action := TotalAction (@conjg1 gT) (@conjgM gT).

Lemma conjg_is_groupAction : is_groupAction setT conjg_action.

Canonical conjg_groupAction := GroupAction conjg_is_groupAction.

Lemma rcoset_is_action : is_action setT (@rcoset gT).

Canonical rcoset_action := Action rcoset_is_action.

Canonical 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 8) : action_scope.
Notation "'Rs" := (@rcoset_action _) (at level 8) : action_scope.
Notation "'J" := (@conjg_action _) (at level 8) : action_scope.
Notation "'J" := (@conjg_groupAction _) (at level 8) : groupAction_scope.
Notation "'Js" := (@conjsg_action _) (at level 8) : action_scope.
Notation "'JG" := (@conjG_action _) (at level 8) : action_scope.
Notation "'Q" := ('J / _)%act (at level 8) : action_scope.
Notation "'Q" := ('J / _)%gact (at level 8) : 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 G x : orbit 'R G x = x *: G.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

This is the second part of Aschbacher (5.7)
Lemma astabRs_rcosets H G : 'C(rcosets H G | 'Rs) = gcore H G.

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

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

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

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

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

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

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

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

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

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

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

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

Lemma astabQR A H : A \subset 'N(H)
'C(A / H | 'Q) = [set x in 'N(H