+ +

Library mathcomp.fingroup.action

+ +

+(* (c) Copyright 2006-2016 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 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 : ∀ 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.
+ +
+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. +

+ +
+Notation "to ^*" := (set_action to) : action_scope.
+ +
+ +
+ +
+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 Ca ⇒ to 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.
+ +
+ +
+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 ].
+ +
+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) +

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

+ +

+ This is Aschbacher (5.20) +

+Theorem subgroup_transitiveP 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 ].
+ +
+

+ +

+ 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.
+ +
+ +
+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 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 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.
+ +
+ +
+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 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 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 "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.
+ +
+

+ +

+ 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 ) | [~: [set x ], A ] \subset H ].
+ +
+Lemma quotient_astabQ H Abar : 'C (Abar | 'Q ) / H = 'C (Abar ).
+ +
+Lemma conj_astabQ A H x :
+  x \in 'N (H ) → 'C (A / H | 'Q ) :^ x = 'C (A :^ x / H | 'Q ).
+ +
+Section CardClass.
+ +
+Variable G : {group gT }.
+ +
+Lemma index_cent1 x : #|G : 'C_G [x ]| = #|x ^: G |.
+ +
+Lemma classes_partition : partition (classes G) 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 abelian_classP : reflect {in G , ∀ x, x ^: G = [set x ]} (abelian G).
+ +
+Lemma card_classes_abelian : abelian G = (#|classes G | == #|G |).
+ +
+End CardClass.
+ +
+End InternalGroupAction.
+ +
+Lemma gacentQ (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 aut_action := [action of autact ].
+ +
+Lemma autactK a : actperm aut_action a = a.
+ +
+Lemma autact_is_groupAction : is_groupAction G aut_action.
+ Canonical aut_groupAction := GroupAction autact_is_groupAction.
+ +
+End AutAct.
+ +
+Notation "[ 'Aut' G ]" := (aut_action G) : action_scope.
+Notation "[ 'Aut' G ]" := (aut_groupAction G) : groupAction_scope.
+ +
+