- -

Library mathcomp.fingroup.action

- -

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

- -

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