Module mathcomp.finite_group.action
From mathcomp Require Import ssreflect ssrbool ssrfun ssrnotations eqtype.From mathcomp Require Import ssrnat div seq prime fintype bigop finset.
From mathcomp Require Import fingroup morphism perm automorphism quotient.
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 to^*.
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.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Declare Scope action_scope.
Declare Scope groupAction_scope.
Local Open Scope group_scope.
Section ActionDef.
Variables (aT : finGroupType) (D : {set aT}) (rT : Type).
Implicit Types a b : aT.
Implicit Type x : rT.
Definition act_morph to x := forall a b, to x (a * b) = to (to x a) b.
Definition is_action to :=
left_injective to /\ forall x, {in D &, act_morph to x}.
Record action := Action {act :> rT -> aT -> rT; _ : is_action act}.
Definition clone_action to :=
let: Action _ toP := to return {type of Action for to} -> action in
fun k => k toP.
End ActionDef.
Delimit Scope action_scope with act.
Bind Scope action_scope with action.
Arguments act_morph {aT rT%_type} to x%_g.
Arguments is_action {aT} D%_g {rT} to.
Arguments act {aT D%_g rT%_type} to%_act x%_g a%_g : rename.
Arguments clone_action [aT D%_g rT%_type to%_act] _.
Notation "{ 'action' aT &-> T }" := (action [set: aT] T)
(format "{ 'action' aT &-> T }") : type_scope.
Notation "[ 'action' 'of' to ]" := (clone_action (@Action _ _ _ to))
(format "[ 'action' 'of' to ]") : form_scope.
Definition act_dom aT D rT & @action aT D rT := D.
Section TotalAction.
Variables (aT : finGroupType) (rT : Type) (to : rT -> aT -> rT).
Hypotheses (to1 : to^~ 1 =1 id) (toM : forall x, act_morph to x).
Lemma is_total_action : is_action setT to.
Proof.
Definition TotalAction := Action is_total_action.
End TotalAction.
Section ActionDefs.
Variables (aT aT' : finGroupType) (D : {set aT}) (D' : {set aT'}).
Definition morph_act rT rT' (to : action D rT) (to' : action D' rT') f fA :=
forall x a, f (to x a) = to' (f x) (fA a).
Variable rT : finType.
Implicit Type to : action D rT.
Implicit Type A : {set aT}.
Implicit Type S : {set rT}.
Definition actm to a := if a \in D then to^~ a else id.
Definition setact to S a := [set to x a | x 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, forall a x, (to x a \in S) = (x \in S)}.
Definition atrans A S to := S \in orbit to A @: S.
Definition faithful A S to := A :&: astab S to \subset [1].
End ActionDefs.
Arguments setact {aT D%_g rT} to%_act S%_g a%_g.
Arguments orbit {aT D%_g rT} to%_act A%_g x%_g.
Arguments amove {aT D%_g rT} to%_act A%_g x%_g y%_g.
Arguments afix {aT D%_g rT} to%_act A%_g.
Arguments astab {aT D%_g rT} S%_g to%_act.
Arguments astabs {aT D%_g rT} S%_g to%_act.
Arguments acts_on {aT D%_g rT} A%_g S%_g to%_act.
Arguments atrans {aT D%_g rT} A%_g S%_g to%_act.
Arguments faithful {aT D%_g rT} A%_g S%_g to%_act.
Notation "to ^*" := (setact to) : function_scope.
Prenex Implicits orbit amove.
Notation "''Fix_' to ( A )" := (afix to A)
(to at level 2, format "''Fix_' to ( A )") : group_scope.
Notation "''Fix_' ( to ) ( A )" := 'Fix_to(A) (only parsing) : group_scope.
Notation "''Fix_' ( S | to ) ( A )" := (S :&: 'Fix_to(A))
(format "''Fix_' ( S | to ) ( A )") : group_scope.
Notation "''Fix_' to [ a ]" := ('Fix_to([set a]))
(to at level 2, format "''Fix_' to [ a ]") : group_scope.
Notation "''Fix_' ( S | to ) [ a ]" := (S :&: 'Fix_to[a])
(format "''Fix_' ( S | to ) [ a ]") : group_scope.
Notation "''C' ( S | to )" := (astab S to) : group_scope.
Notation "''C_' A ( S | to )" := (A :&: 'C(S | to)) : group_scope.
Notation "''C_' ( A ) ( S | to )" := 'C_A(S | to) (only parsing) : group_scope.
Notation "''C' [ x | to ]" := ('C([set x] | to)) : group_scope.
Notation "''C_' A [ x | to ]" := (A :&: 'C[x | to]) : group_scope.
Notation "''C_' ( A ) [ x | to ]" := 'C_A[x | to] (only parsing) : group_scope.
Notation "''N' ( S | to )" := (astabs S to)
(format "''N' ( S | to )") : group_scope.
Notation "''N_' A ( S | to )" := (A :&: 'N(S | to))
(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))
(format "[ 'acts' A , 'on' S | to ]") : form_scope.
Notation "{ 'acts' A , 'on' S | to }" := (acts_on A S to)
(format "{ 'acts' A , 'on' S | to }") : type_scope.
Notation "[ 'transitive' A , 'on' S | to ]" := (atrans A S to)
(format "[ 'transitive' A , 'on' S | to ]") : form_scope.
Notation "[ 'faithful' A , 'on' S | to ]" := (faithful A S to)
(format "[ 'faithful' A , 'on' S | to ]") : form_scope.
Section RawAction.
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
Proof.
Lemma actMin x : {in D &, act_morph to x}.
Proof.
Lemma actmEfun a : a \in D -> actm to a = to^~ a.
Proof.
Lemma actmE a : a \in D -> actm to a =1 to^~ a.
Proof.
Lemma setactE S a : to^* S a = [set to x a | x in S].
Proof.
by []. Qed.
Lemma mem_setact S a x : x \in S -> to x a \in to^* S a.
Proof.
Lemma card_setact S a : #|to^* S a| = #|S|.
Proof.
Lemma setact_is_action : is_action D to^*.
Proof.
Canonical set_action := Action setact_is_action.
Lemma orbitE A x : orbit to A x = to x @: A
Proof.
by []. Qed.
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.
Proof.
Lemma afixP A x : reflect (forall a, a \in A -> to x a = x) (x \in 'Fix_to(A)).
Proof.
Lemma afixS A B : A \subset B -> 'Fix_to(B) \subset 'Fix_to(A).
Proof.
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}.
Proof.
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}.
Proof.
Lemma astabs_act S a x : a \in 'N(S | to) -> (to x a \in S) = (x \in S).
Proof.
rewrite 2!inE subEproper properEcard => /andP[_].
rewrite (card_preimset _ (act_inj _)) ltnn andbF orbF => /eqP{2}->.
by rewrite inE.
Qed.
rewrite (card_preimset _ (act_inj _)) ltnn andbF orbF => /eqP{2}->.
by rewrite inE.
Qed.
Lemma astab_sub S : 'C(S | to) \subset 'N(S | to).
Proof.
Lemma astabsC S : 'N(~: S | to) = 'N(S | to).
Proof.
apply/setP=> a; apply/idP/idP=> nSa; rewrite !inE (astabs_dom nSa).
by rewrite -setCS -preimsetC; apply/subsetP=> x; rewrite inE astabs_act.
by rewrite preimsetC setCS; apply/subsetP=> x; rewrite inE astabs_act.
Qed.
by rewrite -setCS -preimsetC; apply/subsetP=> x; rewrite inE astabs_act.
by rewrite preimsetC setCS; apply/subsetP=> x; rewrite inE astabs_act.
Qed.
Lemma astabsI S T : 'N(S | to) :&: 'N(T | to) \subset 'N(S :&: T | to).
Proof.
Lemma astabs_setact S a : a \in 'N(S | to) -> to^* S a = S.
Proof.
move=> nSa; apply/eqP; rewrite eqEcard card_setact leqnn andbT.
by apply/subsetP=> _ /imsetP[x Sx ->]; rewrite astabs_act.
Qed.
by apply/subsetP=> _ /imsetP[x Sx ->]; rewrite astabs_act.
Qed.
Lemma astab1_set S : 'C[S | set_action] = 'N(S | to).
Proof.
Lemma astabs_set1 x : 'N([set x] | to) = 'C[x | to].
Proof.
Lemma acts_dom A S : [acts A, on S | to] -> A \subset D.
Proof.
Lemma acts_act A S : [acts A, on S | to] -> {acts A, on S | to}.
Proof.
Lemma astabCin A S :
A \subset D -> (A \subset 'C(S | to)) = (S \subset 'Fix_to(A)).
Proof.
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].
Proof.
Lemma actsD : [acts A, on S :\: T | to].
Proof.
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.
Proof.
Lemma subset_faithful A B S :
B \subset A -> [faithful A, on S | to] -> [faithful B, on S | to].
Proof.
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).
Proof.
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).
Proof.
End Reindex.
End RawAction.
Arguments act_inj {aT D rT} to a [x1 x2] : rename.
Notation "to ^*" := (set_action to) : action_scope.
Arguments orbitP {aT D rT to A x y}.
Arguments afixP {aT D rT to A x}.
Arguments afix1P {aT D rT to a x}.
Arguments reindex_astabs [aT D rT] to [vT idx op S] a [F].
Arguments reindex_acts [aT D rT] to [vT idx op S A a F].
Section PartialAction.
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 inv to}.
Lemma actKVin : {in D, rev_right_loop inv to}.
Lemma setactVin S a : a \in D -> to^* S a^-1 = to^~ a @^-1: S.
Proof.
Lemma actXin x a i : a \in D -> to x (a ^+ i) = iter i (to^~ a) x.
Proof.
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.
Local Notation orbit_rel A := (fun x y => x \in orbit to A y).
Lemma contra_orbit G x y : x \notin orbit to G y -> x != y.
Proof.
Lemma orbit_in_sym G : G \subset D -> symmetric (orbit_rel G).
Proof.
Lemma orbit_in_trans G : G \subset D -> transitive (orbit_rel G).
Proof.
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).
Proof.
move=> sGD; apply: (iffP idP) => [yGx|<-]; last exact: orbit_refl.
by apply/setP=> z; apply/idP/idP=> /orbit_in_trans-> //; rewrite orbit_in_sym.
Qed.
by apply/setP=> z; apply/idP/idP=> /orbit_in_trans-> //; rewrite orbit_in_sym.
Qed.
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).
Proof.
Lemma orbit_act_in x a G :
G \subset D -> a \in G -> orbit to G (to x a) = orbit to G x.
Proof.
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).
Proof.
Lemma orbit_inv_in A x y :
A \subset D -> (y \in orbit to A^-1 x) = (x \in orbit to A y).
Proof.
Lemma orbit_lcoset_in A a x :
A \subset D -> a \in D ->
orbit to (a *: A) x = orbit to A (to x a).
Proof.
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).
Proof.
move=> sAD Da; rewrite -orbit_inv_in ?mul_subG ?sub1set // invMg.
by rewrite invg_set1 orbit_lcoset_in ?inv_subG ?groupV ?actKin ?orbit_inv_in.
Qed.
by rewrite invg_set1 orbit_lcoset_in ?inv_subG ?groupV ?actKin ?orbit_inv_in.
Qed.
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).
Proof.
move=> sAD Da; rewrite conjsgE.
by rewrite orbit_lcoset_in ?groupV ?mul_subG ?sub1set ?actKin ?orbit_rcoset_in.
Qed.
by rewrite orbit_lcoset_in ?groupV ?mul_subG ?sub1set ?actKin ?orbit_rcoset_in.
Qed.
Lemma orbit1P G x : reflect (orbit to G x = [set x]) (x \in 'Fix_to(G)).
Proof.
Lemma card_orbit1 G x : #|orbit to G x| = 1%N -> orbit to G x = [set x].
Proof.
Lemma orbit_partition G S :
[acts G, on S | to] -> partition (orbit to G @: S) S.
Proof.
move=> actsGS; have sGD := acts_dom actsGS.
have eqiG: {in S & &, equivalence_rel [rel x y | y \in orbit to G x]}.
by move=> x y z * /=; rewrite orbit_refl; split=> // /orbit_in_eqP->.
congr (partition _ _): (equivalence_partitionP eqiG).
apply: eq_in_imset => x Sx; apply/setP=> y.
by rewrite inE /= andb_idl // => /acts_in_orbit->.
Qed.
have eqiG: {in S & &, equivalence_rel [rel x y | y \in orbit to G x]}.
by move=> x y z * /=; rewrite orbit_refl; split=> // /orbit_in_eqP->.
congr (partition _ _): (equivalence_partitionP eqiG).
apply: eq_in_imset => x Sx; apply/setP=> y.
by rewrite inE /= andb_idl // => /acts_in_orbit->.
Qed.
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 &, forall x y, (y \in orbit to G x) = (x == y)}
& forall x, x \in S -> exists2 a, a \in G & to x a \in X].
Proof.
move/orbit_partition; rewrite -/P => partP.
have [/eqP defS tiP _] := and3P partP.
have trXP: is_transversal X P S := transversalP partP.
have sXS: X \subset S := transversal_sub trXP.
split=> // [x y Xx Xy /= | x Sx].
have Sx := subsetP sXS x Xx.
rewrite -(inj_in_eq (pblock_inj trXP)) // eq_pblock ?defS //.
by rewrite (def_pblock tiP (imset_f _ Sx)) ?orbit_refl.
have /imsetP[y Xy defxG]: orbit to G x \in pblock P @: X.
by rewrite (pblock_transversal trXP) ?imset_f.
suffices /orbitP[a Ga def_y]: y \in orbit to G x by exists a; rewrite ?def_y.
by rewrite defxG mem_pblock defS (subsetP sXS).
Qed.
have [/eqP defS tiP _] := and3P partP.
have trXP: is_transversal X P S := transversalP partP.
have sXS: X \subset S := transversal_sub trXP.
split=> // [x y Xx Xy /= | x Sx].
have Sx := subsetP sXS x Xx.
rewrite -(inj_in_eq (pblock_inj trXP)) // eq_pblock ?defS //.
by rewrite (def_pblock tiP (imset_f _ Sx)) ?orbit_refl.
have /imsetP[y Xy defxG]: orbit to G x \in pblock P @: X.
by rewrite (pblock_transversal trXP) ?imset_f.
suffices /orbitP[a Ga def_y]: y \in orbit to G x by exists a; rewrite ?def_y.
by rewrite defxG mem_pblock defS (subsetP sXS).
Qed.
Lemma group_set_astab S : group_set 'C(S | to).
Proof.
Canonical astab_group S := group (group_set_astab S).
Lemma afix_gen_in A : A \subset D -> 'Fix_to(<<A>>) = 'Fix_to(A).
Proof.
Lemma afix_cycle_in a : a \in D -> 'Fix_to(<[a]>) = 'Fix_to[a].
Proof.
Lemma afixYin A B :
A \subset D -> B \subset D -> 'Fix_to(A <*> B) = 'Fix_to(A) :&: 'Fix_to(B).
Proof.
Lemma afixMin G H :
G \subset D -> H \subset D -> 'Fix_to(G * H) = 'Fix_to(G) :&: 'Fix_to(H).
Proof.
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).
Proof.
apply/group_setP; split=> [|a b cSa cSb].
by rewrite !inE group1; apply/subsetP=> x Sx; rewrite inE act1.
rewrite !inE groupM ?(@astabs_dom _ _ _ to S) //; apply/subsetP=> x Sx.
by rewrite inE actMin ?(@astabs_dom _ _ _ to S) ?astabs_act.
Qed.
by rewrite !inE group1; apply/subsetP=> x Sx; rewrite inE act1.
rewrite !inE groupM ?(@astabs_dom _ _ _ to S) //; apply/subsetP=> x Sx.
by rewrite inE actMin ?(@astabs_dom _ _ _ to S) ?astabs_act.
Qed.
Canonical astabs_group S := group (group_set_astabs S).
Lemma astab_norm S : 'N(S | to) \subset 'N('C(S | to)).
Proof.
Lemma astab_normal S : 'C(S | to) <| 'N(S | to).
Proof.
Lemma acts_sub_orbit G S x :
[acts G, on S | to] -> (orbit to G x \subset S) = (x \in S).
Proof.
move/acts_act=> GactS.
apply/subsetP/idP=> [| Sx y]; first by apply; apply: orbit_refl.
by case/orbitP=> a Ga <-{y}; rewrite GactS.
Qed.
apply/subsetP/idP=> [| Sx y]; first by apply; apply: orbit_refl.
by case/orbitP=> a Ga <-{y}; rewrite GactS.
Qed.
Lemma acts_orbit G x : G \subset D -> [acts G, on orbit to G x | to].
Proof.
Lemma acts_subnorm_fix A : [acts 'N_D(A), on 'Fix_to(D :&: A) | to].
Proof.
Lemma atrans_orbit G x : [transitive G, on orbit to G x | to].
Proof.
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.
Proof.
Lemma amove_orbit : amove to G x @: orbit to G x = rcosets 'C_G[x | to] G.
Proof.
Lemma amoveK :
{in orbit to G x, cancel (amove to G x) (fun Ca => to x (repr Ca))}.
Proof.
Lemma orbit_stabilizer :
orbit to G x = [set to x (repr Ca) | Ca in rcosets 'C_G[x | to] G].
Proof.
rewrite -amove_orbit -imset_comp /=; apply/setP=> z.
by apply/idP/imsetP=> [xGz | [y xGy ->]]; first exists z; rewrite /= ?amoveK.
Qed.
by apply/idP/imsetP=> [xGz | [y xGy ->]]; first exists z; rewrite /= ?amoveK.
Qed.
Lemma act_reprK :
{in rcosets 'C_G[x | to] G, cancel (to x \o repr) (amove to G x)}.
Proof.
move=> _ /rcosetsP[a Ga ->] /=; rewrite amove_act ?rcoset_repr //.
rewrite -[G :&: _]/(gval _); case: repr_rcosetP => b /setIP[Gb _].
exact: groupM.
Qed.
rewrite -[G :&: _]/(gval _); case: repr_rcosetP => b /setIP[Gb _].
exact: groupM.
Qed.
End OrbitStabilizer.
Lemma card_orbit_in G x : G \subset D -> #|orbit to G x| = #|G : 'C_G[x | to]|.
Proof.
Lemma card_orbit_in_stab G x :
G \subset D -> (#|orbit to G x| * #|'C_G[x | to]|)%N = #|G|.
Proof.
Lemma acts_sum_card_orbit G S :
[acts G, on S | to] -> \sum_(T in orbit to G @: S) #|T| = #|S|.
Proof.
Lemma astab_setact_in S a : a \in D -> 'C(to^* S a | to) = 'C(S | to) :^ a.
Proof.
Lemma astab1_act_in x a : a \in D -> 'C[to x a | to] = 'C[x | to] :^ a.
Proof.
Theorem Frobenius_Cauchy G S : [acts G, on S | to] ->
\sum_(a in G) #|'Fix_(S | to)[a]| = (#|orbit to G @: S| * #|G|)%N.
Proof.
move=> GactS; have sGD := acts_dom GactS.
transitivity (\sum_(a in G) \sum_(x in 'Fix_(S | to)[a]) 1%N).
by apply: eq_bigr => a _; rewrite -sum1_card.
rewrite (exchange_big_dep [in S]) /= => [a x _|]; first by case/setIP.
rewrite (set_partition_big _ (orbit_partition GactS)) -sum_nat_const /=.
apply: eq_bigr => _ /imsetP[x Sx ->].
rewrite -(card_orbit_in_stab x sGD) -sum_nat_const.
apply: eq_bigr => y; rewrite orbit_in_sym // => /imsetP[a Ga defx].
rewrite defx astab1_act_in ?(subsetP sGD) //.
rewrite -{2}(conjGid Ga) -conjIg cardJg -sum1_card setIA (setIidPl sGD).
by apply: eq_bigl => b; rewrite !(sub1set, inE) -(acts_act GactS Ga) -defx Sx.
Qed.
transitivity (\sum_(a in G) \sum_(x in 'Fix_(S | to)[a]) 1%N).
by apply: eq_bigr => a _; rewrite -sum1_card.
rewrite (exchange_big_dep [in S]) /= => [a x _|]; first by case/setIP.
rewrite (set_partition_big _ (orbit_partition GactS)) -sum_nat_const /=.
apply: eq_bigr => _ /imsetP[x Sx ->].
rewrite -(card_orbit_in_stab x sGD) -sum_nat_const.
apply: eq_bigr => y; rewrite orbit_in_sym // => /imsetP[a Ga defx].
rewrite defx astab1_act_in ?(subsetP sGD) //.
rewrite -{2}(conjGid Ga) -conjIg cardJg -sum1_card setIA (setIidPl sGD).
by apply: eq_bigl => b; rewrite !(sub1set, inE) -(acts_act GactS Ga) -defx Sx.
Qed.
Lemma atrans_dvd_index_in G S :
G \subset D -> [transitive G, on S | to] -> #|S| %| #|G : 'C_G(S | to)|.
Proof.
Lemma atrans_dvd_in G S :
G \subset D -> [transitive G, on S | to] -> #|S| %| #|G|.
Proof.
Lemma atransPin G S :
G \subset D -> [transitive G, on S | to] ->
forall x, x \in S -> orbit to G x = S.
Proof.
Lemma atransP2in G S :
G \subset D -> [transitive G, on S | to] ->
{in S &, forall x y, exists2 a, a \in G & y = to x a}.
Lemma atrans_acts_in G S :
G \subset D -> [transitive G, on S | to] -> [acts G, on S | to].
Proof.
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].
Proof.
move=> Sx sHG sGD trG; have sHD := subset_trans sHG sGD.
apply: (iffP idP) => [trH | defG].
rewrite group_modr //; apply/setIidPl/subsetP=> a Ga.
have Sxa: to x a \in S by rewrite (acts_act (atrans_acts_in sGD trG)).
have [b Hb xab]:= atransP2in sHD trH Sxa Sx.
have Da := subsetP sGD a Ga; have Db := subsetP sHD b Hb.
rewrite -(mulgK b a) mem_mulg ?groupV // !inE groupM //= sub1set inE.
by rewrite actMin -?xab.
apply/imsetP; exists x => //; apply/setP=> y; rewrite -(atransPin sGD trG Sx).
apply/imsetP/imsetP=> [] [a]; last by exists a; first apply: (subsetP sHG).
rewrite -defG => /imset2P[c b /setIP[_ cxc] Hb ->] ->.
exists b; rewrite ?actMin ?(astab_dom cxc) ?(subsetP sHD) //.
by rewrite (astab_act cxc) ?inE.
Qed.
apply: (iffP idP) => [trH | defG].
rewrite group_modr //; apply/setIidPl/subsetP=> a Ga.
have Sxa: to x a \in S by rewrite (acts_act (atrans_acts_in sGD trG)).
have [b Hb xab]:= atransP2in sHD trH Sxa Sx.
have Da := subsetP sGD a Ga; have Db := subsetP sHD b Hb.
rewrite -(mulgK b a) mem_mulg ?groupV // !inE groupM //= sub1set inE.
by rewrite actMin -?xab.
apply/imsetP; exists x => //; apply/setP=> y; rewrite -(atransPin sGD trG Sx).
apply/imsetP/imsetP=> [] [a]; last by exists a; first apply: (subsetP sHG).
rewrite -defG => /imset2P[c b /setIP[_ cxc] Hb ->] ->.
exists b; rewrite ?actMin ?(astab_dom cxc) ?(subsetP sHD) //.
by rewrite (astab_act cxc) ?inE.
Qed.
End PartialAction.
Arguments orbit_transversal {aT D%_g rT} to%_act A%_g S%_g.
Arguments orbit_in_eqP {aT D rT to G x y}.
Arguments orbit1P {aT D rT to G x}.
Arguments contra_orbit [aT D rT] to G [x y].
Notation "''C' ( S | to )" := (astab_group to S) : Group_scope.
Notation "''C_' A ( S | to )" := (setI_group A 'C(S | to)) : Group_scope.
Notation "''C_' ( A ) ( S | to )" := (setI_group A 'C(S | to))
(only parsing) : Group_scope.
Notation "''C' [ x | to ]" := (astab_group to [set x%g]) : Group_scope.
Notation "''C_' A [ x | to ]" := (setI_group A 'C[x | to]) : Group_scope.
Notation "''C_' ( A ) [ x | to ]" := (setI_group A 'C[x | to])
(only parsing) : Group_scope.
Notation "''N' ( S | to )" := (astabs_group to S) : Group_scope.
Notation "''N_' A ( S | to )" := (setI_group A 'N(S | to)) : Group_scope.
Section TotalActions.
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 inv to.
Lemma actKV : rev_right_loop inv 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).
Proof.
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.
Proof.
Lemma orbit_eqP G x y :
reflect (orbit to G x = orbit to G y) (x \in orbit to G y).
Proof.
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).
Proof.
Lemma orbit_act G a x: a \in G -> orbit to G (to x a) = orbit to G x.
Proof.
Lemma orbit_actr G a x y :
a \in G -> (to y a \in orbit to G x) = (y \in orbit to G x).
Proof.
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).
Proof.
Lemma orbit_lcoset A a x : orbit to (a *: A) x = orbit to A (to x a).
Proof.
Lemma orbit_rcoset A a x y :
(to y a \in orbit to (A :* a) x) = (y \in orbit to A x).
Proof.
Lemma orbit_conjsg A a x y :
(to y a \in orbit to (A :^ a) (to x a)) = (y \in orbit to A x).
Proof.
Lemma astabP S a : reflect (forall x, x \in S -> to x a = x) (a \in 'C(S | to)).
Proof.
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)).
Proof.
Lemma astabC A S : (A \subset 'C(S | to)) = (S \subset 'Fix_to(A)).
Lemma afix_cycle a : 'Fix_to(<[a]>) = 'Fix_to[a].
Proof.
Lemma afix_gen A : 'Fix_to(<<A>>) = 'Fix_to(A).
Proof.
Lemma afixM G H : 'Fix_to(G * H) = 'Fix_to(G) :&: 'Fix_to(H).
Lemma astabsP S a :
reflect (forall x, (to x a \in S) = (x \in S)) (a \in 'N(S | to)).
Proof.
Lemma card_orbit G x : #|orbit to G x| = #|G : 'C_G[x | to]|.
Proof.
Lemma dvdn_orbit G x : #|orbit to G x| %| #|G|.
Proof.
Lemma card_orbit_stab G x : (#|orbit to G x| * #|'C_G[x | to]|)%N = #|G|.
Proof.
Lemma actsP A S : reflect {acts A, on S | to} [acts A, on S | to].
Proof.
Lemma setact_orbit A x b : to^* (orbit to A x) b = orbit to (A :^ b) (to x b).
Proof.
Lemma astab_setact S a : 'C(to^* S a | to) = 'C(S | to) :^ a.
Proof.
Lemma astab1_act x a : 'C[to x a | to] = 'C[x | to] :^ a.
Proof.
Lemma atransP G S : [transitive G, on S | to] ->
forall x, x \in S -> orbit to G x = S.
Lemma atransP2 G S : [transitive G, on S | to] ->
{in S &, forall 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].
Proof.
Lemma atrans_supgroup G H S :
G \subset H -> [transitive G, on S | to] ->
[transitive H, on S | to] = [acts H, on S | to].
Proof.
move=> sGH trG; apply/idP/idP=> [|actH]; first exact: atrans_acts.
case/imsetP: trG => x Sx defS; apply/imsetP; exists x => //.
by apply/eqP; rewrite eqEsubset acts_sub_orbit ?Sx // defS imsetS.
Qed.
case/imsetP: trG => x Sx defS; apply/imsetP; exists x => //.
by apply/eqP; rewrite eqEsubset acts_sub_orbit ?Sx // defS imsetS.
Qed.
Lemma atrans_acts_card G S :
[transitive G, on S | to] =
[acts G, on S | to] && (#|orbit to G @: S| == 1%N).
Proof.
apply/idP/andP=> [GtrS | [nSG]].
split; first exact: atrans_acts.
rewrite ((_ @: S =P [set S]) _) ?cards1 // eqEsubset sub1set.
apply/andP; split=> //; apply/subsetP=> _ /imsetP[x Sx ->].
by rewrite inE (atransP GtrS).
rewrite eqn_leq andbC lt0n => /andP[/existsP[X /imsetP[x Sx X_Gx]]].
rewrite (cardD1 X) {X}X_Gx imset_f // ltnS leqn0 => /eqP GtrS.
apply/imsetP; exists x => //; apply/eqP.
rewrite eqEsubset acts_sub_orbit // Sx andbT.
apply/subsetP=> y Sy; have:= card0_eq GtrS (orbit to G y).
by rewrite !inE /= imset_f // andbT => /eqP <-; apply: orbit_refl.
Qed.
split; first exact: atrans_acts.
rewrite ((_ @: S =P [set S]) _) ?cards1 // eqEsubset sub1set.
apply/andP; split=> //; apply/subsetP=> _ /imsetP[x Sx ->].
by rewrite inE (atransP GtrS).
rewrite eqn_leq andbC lt0n => /andP[/existsP[X /imsetP[x Sx X_Gx]]].
rewrite (cardD1 X) {X}X_Gx imset_f // ltnS leqn0 => /eqP GtrS.
apply/imsetP; exists x => //; apply/eqP.
rewrite eqEsubset acts_sub_orbit // Sx andbT.
apply/subsetP=> y Sy; have:= card0_eq GtrS (orbit to G y).
by rewrite !inE /= imset_f // andbT => /eqP <-; apply: orbit_refl.
Qed.
Lemma atrans_dvd G S : [transitive G, on S | to] -> #|S| %| #|G|.
Proof.
Lemma acts_fix_norm A B : A \subset 'N(B) -> [acts A, on 'Fix_to(B) | to].
Proof.
Lemma faithfulP A S :
reflect (forall a, a \in A -> {in S, to^~ a =1 id} -> a = 1)
[faithful A, on S | to].
Proof.
Lemma astab_trans_gcore G S u :
[transitive G, on S | to] -> u \in S -> 'C(S | to) = gcore 'C[u | to] G.
Proof.
move=> transG Su; apply/eqP; rewrite eqEsubset.
rewrite gcore_max ?astabS ?sub1set //=.
exact: subset_trans (atrans_acts transG) (astab_norm _ _).
apply/subsetP=> x cSx; apply/astabP=> uy.
case/(atransP2 transG Su) => y Gy ->{uy}.
by apply/astab1P; rewrite astab1_act (bigcapP cSx).
Qed.
rewrite gcore_max ?astabS ?sub1set //=.
exact: subset_trans (atrans_acts transG) (astab_norm _ _).
apply/subsetP=> x cSx; apply/astabP=> uy.
case/(atransP2 transG Su) => y Gy ->{uy}.
by apply/astab1P; rewrite astab1_act (bigcapP cSx).
Qed.
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].
Proof.
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].
Proof.
move=> C T trGS Sx sHC; have actGS := acts_act (atrans_acts trGS).
have:= sHC; rewrite subsetI sub_astab1 => /andP[sHG cHx].
have Tx: x \in T by rewrite inE Sx.
apply: (iffP idP) => [trN | trC].
apply/setP=> Ha; apply/setIdP/imsetP=> [[]|[a Ca ->{Ha}]]; last first.
by rewrite conj_subG //; case/setIP: Ca => Ga _; rewrite imset_f.
case/imsetP=> a Ga ->{Ha}; rewrite subsetI !sub_conjg => /andP[_ sHCa].
have Txa: to x a^-1 \in T.
by rewrite inE -sub_astab1 astab1_act actGS ?Sx ?groupV.
have [b] := atransP2 trN Tx Txa; case/setIP=> Gb nHb cxba.
exists (b * a); last by rewrite conjsgM (normP nHb).
by rewrite inE groupM //; apply/astab1P; rewrite actM -cxba actKV.
apply/imsetP; exists x => //; apply/setP=> y; apply/idP/idP=> [Ty|].
have [Sy cHy]:= setIP Ty; have [a Ga defy] := atransP2 trGS Sx Sy.
have: H :^ a^-1 \in H :^: C.
rewrite -trC inE subsetI imset_f 1?conj_subG ?groupV // sub_conjgV.
by rewrite -astab1_act -defy sub_astab1.
case/imsetP=> b /setIP[Gb /astab1P cxb] defHb.
rewrite defy -{1}cxb -actM mem_orbit // inE groupM //.
by apply/normP; rewrite conjsgM -defHb conjsgKV.
case/imsetP=> a /setIP[Ga nHa] ->{y}.
by rewrite inE actGS // Sx (acts_act (acts_fix_norm _) nHa).
Qed.
have:= sHC; rewrite subsetI sub_astab1 => /andP[sHG cHx].
have Tx: x \in T by rewrite inE Sx.
apply: (iffP idP) => [trN | trC].
apply/setP=> Ha; apply/setIdP/imsetP=> [[]|[a Ca ->{Ha}]]; last first.
by rewrite conj_subG //; case/setIP: Ca => Ga _; rewrite imset_f.
case/imsetP=> a Ga ->{Ha}; rewrite subsetI !sub_conjg => /andP[_ sHCa].
have Txa: to x a^-1 \in T.
by rewrite inE -sub_astab1 astab1_act actGS ?Sx ?groupV.
have [b] := atransP2 trN Tx Txa; case/setIP=> Gb nHb cxba.
exists (b * a); last by rewrite conjsgM (normP nHb).
by rewrite inE groupM //; apply/astab1P; rewrite actM -cxba actKV.
apply/imsetP; exists x => //; apply/setP=> y; apply/idP/idP=> [Ty|].
have [Sy cHy]:= setIP Ty; have [a Ga defy] := atransP2 trGS Sx Sy.
have: H :^ a^-1 \in H :^: C.
rewrite -trC inE subsetI imset_f 1?conj_subG ?groupV // sub_conjgV.
by rewrite -astab1_act -defy sub_astab1.
case/imsetP=> b /setIP[Gb /astab1P cxb] defHb.
rewrite defy -{1}cxb -actM mem_orbit // inE groupM //.
by apply/normP; rewrite conjsgM -defHb conjsgKV.
case/imsetP=> a /setIP[Ga nHa] ->{y}.
by rewrite inE actGS // Sx (acts_act (acts_fix_norm _) nHa).
Qed.
End TotalActions.
Arguments astabP {aT rT to S a}.
Arguments orbit_eqP {aT rT to G x y}.
Arguments astab1P {aT rT to x a}.
Arguments astabsP {aT rT to S a}.
Arguments atransP {aT rT to G S}.
Arguments actsP {aT rT to A S}.
Arguments faithfulP {aT rT to A S}.
Section Restrict.
Variables (aT : finGroupType) (D : {set aT}) (rT : Type).
Variables (to : action D rT) (A : {set aT}).
Definition ract & A \subset D := act to.
Variable sAD : A \subset D.
Lemma ract_is_action : is_action A (ract sAD).
Proof.
Canonical raction := Action ract_is_action.
Lemma ractE : raction =1 to
Proof.
by []. Qed.
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 & 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).
Proof.
rewrite /actby; split=> [a x y | x a b Aa Ab /=]; last first.
rewrite Aa Ab groupM // !andbT actMin ?(subsetP (acts_dom nRA)) //.
by case Rx: (x \in R); rewrite ?(acts_act nRA) ?Rx.
case Aa: (a \in A); rewrite ?andbF ?andbT //.
case Rx: (x \in R); case Ry: (y \in R) => // eqxy; first exact: act_inj eqxy.
by rewrite -eqxy (acts_act nRA Aa) Rx in Ry.
by rewrite eqxy (acts_act nRA Aa) Ry in Rx.
Qed.
rewrite Aa Ab groupM // !andbT actMin ?(subsetP (acts_dom nRA)) //.
by case Rx: (x \in R); rewrite ?(acts_act nRA) ?Rx.
case Aa: (a \in A); rewrite ?andbF ?andbT //.
case Rx: (x \in R); case Ry: (y \in R) => // eqxy; first exact: act_inj eqxy.
by rewrite -eqxy (acts_act nRA Aa) Rx in Ry.
by rewrite eqxy (acts_act nRA Aa) Ry in Rx.
Qed.
Canonical action_by := Action actby_is_action.
Local Notation "<[nRA]>" := action_by : action_scope.
Lemma actbyE x a : x \in R -> a \in A -> <[nRA]>%act x a = to x a.
Proof.
Lemma afix_actby B : 'Fix_<[nRA]>(B) = ~: R :|: 'Fix_to(A :&: B).
Proof.
Lemma astab_actby S : 'C(S | <[nRA]>) = 'C_A(R :&: S | to).
Proof.
Lemma astabs_actby S : 'N(S | <[nRA]>) = 'N_A(R :&: S | to).
Proof.
Lemma acts_actby (B : {set aT}) S :
[acts B, on S | <[nRA]>] = (B \subset A) && [acts B, on R :&: S | to].
Proof.
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)).
Proof.
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.
Proof.
split=> [a u v eq_uv | u a b Na Nb]; apply: val_inj.
move/(congr1 val): eq_uv; rewrite !val_subact.
by case: (a \in _); first move/act_inj.
have Da := astabs_dom Na; have Db := astabs_dom Nb.
by rewrite !val_subact Na Nb groupM ?actMin.
Qed.
move/(congr1 val): eq_uv; rewrite !val_subact.
by case: (a \in _); first move/act_inj.
have Da := astabs_dom Na; have Db := astabs_dom Nb.
by rewrite !val_subact Na Nb groupM ?actMin.
Qed.
Canonical subaction := Action subact_is_action.
Lemma astab_subact S : 'C(S | subaction) = subact_dom :&: 'C(val @: S | to).
Proof.
apply/setP=> a; rewrite inE in_setI; apply: andb_id2l => sDa.
have [Da _] := setIP sDa; rewrite !inE Da.
apply/subsetP/subsetP=> [cSa _ /imsetP[x Sx ->] | cSa x Sx] /[!inE].
by have:= cSa x Sx; rewrite inE -val_eqE val_subact sDa.
by have:= cSa _ (imset_f val Sx); rewrite inE -val_eqE val_subact sDa.
Qed.
have [Da _] := setIP sDa; rewrite !inE Da.
apply/subsetP/subsetP=> [cSa _ /imsetP[x Sx ->] | cSa x Sx] /[!inE].
by have:= cSa x Sx; rewrite inE -val_eqE val_subact sDa.
by have:= cSa _ (imset_f val Sx); rewrite inE -val_eqE val_subact sDa.
Qed.
Lemma astabs_subact S : 'N(S | subaction) = subact_dom :&: 'N(val @: S | to).
Proof.
apply/setP=> a; rewrite inE in_setI; apply: andb_id2l => sDa.
have [Da _] := setIP sDa; rewrite !inE Da.
apply/subsetP/subsetP=> [nSa _ /imsetP[x Sx ->] | nSa x Sx] /[!inE].
by have /[1!inE]/(imset_f val) := nSa x Sx; rewrite val_subact sDa.
have /[1!inE]/imsetP[y Sy def_y] := nSa _ (imset_f val Sx).
by rewrite ((_ a =P y) _) // -val_eqE val_subact sDa def_y.
Qed.
have [Da _] := setIP sDa; rewrite !inE Da.
apply/subsetP/subsetP=> [nSa _ /imsetP[x Sx ->] | nSa x Sx] /[!inE].
by have /[1!inE]/(imset_f val) := nSa x Sx; rewrite val_subact sDa.
have /[1!inE]/imsetP[y Sy def_y] := nSa _ (imset_f val Sx).
by rewrite ((_ a =P y) _) // -val_eqE val_subact sDa def_y.
Qed.
Lemma afix_subact A :
A \subset subact_dom -> 'Fix_subaction(A) = val @^-1: 'Fix_to(A).
Proof.
End SubAction.
Notation "to ^?" := (subaction _ to) (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].
Local Notation subdom := (subact_dom (coset_range H) to^*).
Fact qact_subdomE : subdom = qact_dom.
Lemma qact_proof : qact_dom \subset subdom.
Proof.
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].
Proof.
apply/subsetP=> a nNa; rewrite !inE (astabs_dom nNa); apply/subsetP=> x Nx.
have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE imset_f.
rewrite inE -(astabs_act _ nNa) => /rcosetsP[y Ny defHy].
have: to x a \in H :* y by rewrite -defHy (imset_f (to^~a)) ?rcoset_refl.
by apply: subsetP; rewrite mul_subG ?sub1set ?normG.
Qed.
have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE imset_f.
rewrite inE -(astabs_act _ nNa) => /rcosetsP[y Ny defHy].
have: to x a \in H :* y by rewrite -defHy (imset_f (to^~a)) ?rcoset_refl.
by apply: subsetP; rewrite mul_subG ?sub1set ?normG.
Qed.
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).
Proof.
move=> Nx; apply: val_inj; rewrite val_subact //= qact_subdomE.
have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE imset_f.
case nNa: (a \in _); rewrite // -(astabs_act _ nNa).
rewrite !val_coset ?(acts_act acts_qact_dom nNa) //=.
case/rcosetsP=> y Ny defHy; rewrite defHy; apply: rcoset_eqP.
by rewrite rcoset_sym -defHy (imset_f (_^~_)) ?rcoset_refl.
Qed.
have: H :* x \in rcosets H 'N(H) by rewrite -rcosetE imset_f.
case nNa: (a \in _); rewrite // -(astabs_act _ nNa).
rewrite !val_coset ?(acts_act acts_qact_dom nNa) //=.
case/rcosetsP=> y Ny defHy; rewrite defHy; apply: rcoset_eqP.
by rewrite rcoset_sym -defHy (imset_f (_^~_)) ?rcoset_refl.
Qed.
Lemma qactE x a :
x \in 'N(H) -> a \in qact_dom ->
quotient_action (coset H x) a = coset H (to x a).
Proof.
Lemma acts_quotient (A : {set aT}) (B : {set rT}) :
A \subset 'N_qact_dom(B | to) -> [acts A, on B / H | quotient_action].
Proof.
move=> nBA; apply: subset_trans {A}nBA _; apply/subsetP=> a /setIP[dHa nBa].
rewrite inE dHa inE; apply/subsetP=> _ /morphimP[x nHx Bx ->].
rewrite inE /= qactE //.
by rewrite mem_morphim ?(acts_act acts_qact_dom) ?(astabs_act _ nBa).
Qed.
rewrite inE dHa inE; apply/subsetP=> _ /morphimP[x nHx Bx ->].
rewrite inE /= qactE //.
by rewrite mem_morphim ?(acts_act acts_qact_dom) ?(astabs_act _ nBa).
Qed.
Lemma astabs_quotient (G : {group rT}) :
H <| G -> 'N(G / H | quotient_action) = 'N_qact_dom(G | to).
Proof.
move=> nsHG; have [_ nHG] := andP nsHG.
apply/eqP; rewrite eqEsubset acts_quotient // andbT.
apply/subsetP=> a nGa; have dHa := astabs_dom nGa; have [Da _]:= setIdP dHa.
rewrite inE dHa 2!inE Da; apply/subsetP=> x Gx; have nHx := subsetP nHG x Gx.
rewrite -(quotientGK nsHG) 2!inE (acts_act acts_qact_dom) ?nHx //= inE.
by rewrite -qactE // (astabs_act _ nGa) mem_morphim.
Qed.
apply/eqP; rewrite eqEsubset acts_quotient // andbT.
apply/subsetP=> a nGa; have dHa := astabs_dom nGa; have [Da _]:= setIdP dHa.
rewrite inE dHa 2!inE Da; apply/subsetP=> x Gx; have nHx := subsetP nHG x Gx.
rewrite -(quotientGK nsHG) 2!inE (acts_act acts_qact_dom) ?nHx //= inE.
by rewrite -qactE // (astabs_act _ nGa) mem_morphim.
Qed.
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}.
Local Notation dom := 'N_D(H).
Local Notation range := 'Fix_to(D :&: H).
Let acts_dom : {acts dom, on range | to} := acts_act (acts_subnorm_fix to H).
Definition modact x (Ha : coset_of H) :=
if x \in range then to x (repr (D :&: Ha)) else x.
Lemma modactEcond x a :
a \in dom -> modact x (coset H a) = (if x \in range then to x a else x).
Proof.
Lemma modactE x a :
a \in D -> a \in 'N(H) -> x \in range -> modact x (coset H a) = to x a.
Proof.
Lemma modact_is_action : is_action (D / H) modact.
Proof.
split=> [Ha x y | x Ha Hb]; last first.
case/morphimP=> a Na Da ->{Ha}; case/morphimP=> b Nb Db ->{Hb}.
rewrite -morphM //= !modactEcond // ?groupM ?(introT setIP _) //.
by case: ifP => Cx; rewrite ?(acts_dom, Cx, actMin, introT setIP _).
case: (set_0Vmem (D :&: Ha)) => [Da0 | [a /setIP[Da NHa]]].
by rewrite /modact Da0 repr_set0 !act1 !if_same.
have Na := subsetP (coset_norm _) _ NHa.
have NDa: a \in 'N_D(H) by rewrite inE Da.
rewrite -(coset_mem NHa) !modactEcond //.
do 2![case: ifP] => Cy Cx // eqxy; first exact: act_inj eqxy.
by rewrite -eqxy acts_dom ?Cx in Cy.
by rewrite eqxy acts_dom ?Cy in Cx.
Qed.
case/morphimP=> a Na Da ->{Ha}; case/morphimP=> b Nb Db ->{Hb}.
rewrite -morphM //= !modactEcond // ?groupM ?(introT setIP _) //.
by case: ifP => Cx; rewrite ?(acts_dom, Cx, actMin, introT setIP _).
case: (set_0Vmem (D :&: Ha)) => [Da0 | [a /setIP[Da NHa]]].
by rewrite /modact Da0 repr_set0 !act1 !if_same.
have Na := subsetP (coset_norm _) _ NHa.
have NDa: a \in 'N_D(H) by rewrite inE Da.
rewrite -(coset_mem NHa) !modactEcond //.
do 2![case: ifP] => Cy Cx // eqxy; first exact: act_inj eqxy.
by rewrite -eqxy acts_dom ?Cx in Cy.
by rewrite eqxy acts_dom ?Cy in Cx.
Qed.
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.
Proof.
apply/setP=> Ha; apply/idP/morphimP=> [nSa | [a nHa nSa ->]].
case/morphimP: (astabs_dom nSa) => a nHa Da defHa.
exists a => //; rewrite !inE Da; apply/subsetP=> x Sx; rewrite !inE.
by have:= Sx; rewrite -(astabs_act x nSa) defHa /= modactE ?(subsetP fixSH).
have Da := astabs_dom nSa; rewrite !inE mem_quotient //; apply/subsetP=> x Sx.
by rewrite !inE /= modactE ?(astabs_act x nSa) ?(subsetP fixSH).
Qed.
case/morphimP: (astabs_dom nSa) => a nHa Da defHa.
exists a => //; rewrite !inE Da; apply/subsetP=> x Sx; rewrite !inE.
by have:= Sx; rewrite -(astabs_act x nSa) defHa /= modactE ?(subsetP fixSH).
have Da := astabs_dom nSa; rewrite !inE mem_quotient //; apply/subsetP=> x Sx.
by rewrite !inE /= modactE ?(astabs_act x nSa) ?(subsetP fixSH).
Qed.
Lemma astab_mod : 'C(S | mod_action) = 'C(S | to) / H.
Proof.
apply/setP=> Ha; apply/idP/morphimP=> [cSa | [a nHa cSa ->]].
case/morphimP: (astab_dom cSa) => a nHa Da defHa.
exists a => //; rewrite !inE Da; apply/subsetP=> x Sx; rewrite !inE.
by rewrite -{2}[x](astab_act cSa) // defHa /= modactE ?(subsetP fixSH).
have Da := astab_dom cSa; rewrite !inE mem_quotient //; apply/subsetP=> x Sx.
by rewrite !inE /= modactE ?(astab_act cSa) ?(subsetP fixSH).
Qed.
case/morphimP: (astab_dom cSa) => a nHa Da defHa.
exists a => //; rewrite !inE Da; apply/subsetP=> x Sx; rewrite !inE.
by rewrite -{2}[x](astab_act cSa) // defHa /= modactE ?(subsetP fixSH).
have Da := astab_dom cSa; rewrite !inE mem_quotient //; apply/subsetP=> x Sx.
by rewrite !inE /= modactE ?(astab_act cSa) ?(subsetP fixSH).
Qed.
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).
Proof.
move=> cSH /subsetIP[sGD nHG].
apply/eqP; rewrite eqEsubset !subsetI !subsetIl /= -!astabCin ?quotientS //.
have cfixH F: H \subset 'C(S :&: F | to).
by rewrite (subset_trans cSH) // astabS ?subsetIl.
rewrite andbC astab_mod ?quotientS //=; first by rewrite astabCin ?subsetIr.
by rewrite -(quotientSGK nHG) //= -astab_mod // astabCin ?quotientS ?subsetIr.
Qed.
apply/eqP; rewrite eqEsubset !subsetI !subsetIl /= -!astabCin ?quotientS //.
have cfixH F: H \subset 'C(S :&: F | to).
by rewrite (subset_trans cSH) // astabS ?subsetIl.
rewrite andbC astab_mod ?quotientS //=; first by rewrite astabCin ?subsetIr.
by rewrite -(quotientSGK nHG) //= -astab_mod // astabCin ?quotientS ?subsetIr.
Qed.
End GenericMod.
Lemma modact_faithful G S :
[faithful G / 'C_G(S | to), on S | mod_action 'C_G(S | to)].
Proof.
End ModAction.
Notation "to %% H" := (mod_action to H) : action_scope.
Section ActPerm.
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.
Proof.
Lemma actpermK x a : aperm x (actperm a) = to x a.
Proof.
Lemma ker_actperm : 'ker actperm = 'C(setT | to).
Proof.
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]>).
Proof.
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)
Proof.
by []. Qed.
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].
Proof.
End RestrictActionTheory.
Section MorphAct.
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.
Proof.
Canonical morph_action := Action mact_is_action.
Lemma mactE x a : morph_action x a = phi a x
Proof.
by []. Qed.
Lemma injm_faithful : 'injm phi -> [faithful D, on setT | morph_action].
Proof.
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.
Proof.
Lemma comp_actE x e : comp_action x e = to x (f e)
Proof.
by []. Qed.
Lemma afix_comp (A : {set gT}) :
A \subset B -> 'Fix_comp_action(A) = 'Fix_to(f @* A).
Proof.
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.
Variable rT : finType.
Local Notation gT := {perm rT}.
Implicit Types a b c : gT.
Lemma aperm_is_action : is_action setT (@aperm rT).
Proof.
Canonical perm_action := Action aperm_is_action.
Lemma porbitE a : porbit a = orbit perm_action <[a]>%g.
Proof.
Lemma perm_act1P a : reflect (forall x, aperm x a = x) (a == 1).
Proof.
Lemma perm_faithful A : [faithful A, on setT | perm_action].
Proof.
Lemma actperm_id p : actperm perm_action p = p.
End PermAction.
Arguments perm_act1P {rT a}.
Notation "'P" := (perm_action _) : 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.
Proof.
move=> sAD x; rewrite morphimEsub // /orbit -imset_comp.
by apply: eq_imset => a //=; rewrite actpermK.
Qed.
by apply: eq_imset => a //=; rewrite actpermK.
Qed.
Lemma porbit_actperm (a : aT) :
a \in D -> porbit (actperm to a) =1 orbit to <[a]>.
Proof.
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, forall p, restr_perm p =1 p}.
Lemma ker_restr_perm : 'ker restr_perm = 'C(S | 'P).
Proof.
Lemma im_restr_perm p : restr_perm p @: S = S.
Proof.
Lemma restr_perm_commute s : commute (restr_perm s) s.
Proof.
have [sC|/triv_restr_perm->] := boolP (s \in 'N(S | 'P)); last first.
exact: (commute_sym (commute1 _)).
apply/permP => x; have /= xsS := astabsP sC x; rewrite !permM.
have [xS|xNS] := boolP (x \in S); first by rewrite ?(restr_permE) ?xsS.
by rewrite !(out_perm (restr_perm_on _)) ?xsS.
Qed.
exact: (commute_sym (commute1 _)).
apply/permP => x; have /= xsS := astabsP sC x; rewrite !permM.
have [xS|xNS] := boolP (x \in S); first by rewrite ?(restr_permE) ?xsS.
by rewrite !(out_perm (restr_perm_on _)) ?xsS.
Qed.
End RestrictPerm.
Section Symmetry.
Variables (T : finType) (S : {set T}).
Lemma SymE : Sym S = 'C(~: S | 'P).
Proof.
End Symmetry.
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.
Proof.
Lemma restr_perm_Aut : restr_perm H @* Aut G \subset Aut H.
Proof.
Lemma Aut_in_isog : Aut_in (Aut G) H \isog restr_perm H @* Aut G.
Proof.
rewrite /Aut_in -ker_restr_perm kerE -morphpreIdom -morphimIdom -kerE /=.
by rewrite setIA (setIC _ (Aut G)) first_isog_loc ?subsetIr.
Qed.
by rewrite setIA (setIC _ (Aut G)) first_isog_loc ?subsetIr.
Qed.
Lemma Aut_sub_fullP :
reflect (forall h : {morphism H >-> gT}, 'injm h -> h @* H = H ->
exists g : {morphism G >-> gT},
[/\ 'injm g, g @* G = G & {in H, g =1 h}])
(Aut_in (Aut G) H \isog Aut H).
Proof.
rewrite (isog_transl _ Aut_in_isog) /=; set rG := _ @* _.
apply: (iffP idP) => [iso_rG h injh hH| AutHinG].
have: aut injh hH \in rG; last case/morphimP=> g nHg AutGg def_g.
suffices ->: rG = Aut H by apply: Aut_aut.
by apply/eqP; rewrite eqEcard restr_perm_Aut /= (card_isog iso_rG).
exists (autm_morphism AutGg); rewrite injm_autm im_autm; split=> // x Hx.
by rewrite -(autE injh hH Hx) def_g actpermE actbyE.
suffices ->: rG = Aut H by apply: isog_refl.
apply/eqP; rewrite eqEsubset restr_perm_Aut /=.
apply/subsetP=> h AutHh; have hH := im_autm AutHh.
have [g [injg gG eq_gh]] := AutHinG _ (injm_autm AutHh) hH.
have [Ng AutGg]: aut injg gG \in 'N(H | 'P) /\ aut injg gG \in Aut G.
rewrite Aut_aut !inE; split=> //; apply/subsetP=> x Hx.
by rewrite inE /= /aperm autE ?(subsetP sHG) // -hH eq_gh ?mem_morphim.
apply/morphimP; exists (aut injg gG) => //; apply: (eq_Aut AutHh) => [|x Hx].
by rewrite (subsetP restr_perm_Aut) // mem_morphim.
by rewrite restr_permE //= /aperm autE ?eq_gh ?(subsetP sHG).
Qed.
apply: (iffP idP) => [iso_rG h injh hH| AutHinG].
have: aut injh hH \in rG; last case/morphimP=> g nHg AutGg def_g.
suffices ->: rG = Aut H by apply: Aut_aut.
by apply/eqP; rewrite eqEcard restr_perm_Aut /= (card_isog iso_rG).
exists (autm_morphism AutGg); rewrite injm_autm im_autm; split=> // x Hx.
by rewrite -(autE injh hH Hx) def_g actpermE actbyE.
suffices ->: rG = Aut H by apply: isog_refl.
apply/eqP; rewrite eqEsubset restr_perm_Aut /=.
apply/subsetP=> h AutHh; have hH := im_autm AutHh.
have [g [injg gG eq_gh]] := AutHinG _ (injm_autm AutHh) hH.
have [Ng AutGg]: aut injg gG \in 'N(H | 'P) /\ aut injg gG \in Aut G.
rewrite Aut_aut !inE; split=> //; apply/subsetP=> x Hx.
by rewrite inE /= /aperm autE ?(subsetP sHG) // -hH eq_gh ?mem_morphim.
apply/morphimP; exists (aut injg gG) => //; apply: (eq_Aut AutHh) => [|x Hx].
by rewrite (subsetP restr_perm_Aut) // mem_morphim.
by rewrite restr_permE //= /aperm autE ?eq_gh ?(subsetP sHG).
Qed.
End AutIn.
Arguments Aut_in {gT} A%_g B%_g.
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.
Local Notation fGisom := (Aut_isom injf sGD).
Local Notation fHisom := (Aut_isom injf sHD).
Local Notation inH := (restr_perm H).
Local Notation infH := (restr_perm (f @* H)).
Lemma astabs_Aut_isom a :
a \in Aut G -> (fGisom a \in 'N(f @* H | 'P)) = (a \in 'N(H | 'P)).
Proof.
move=> AutGa; rewrite !inE sub_morphim_pre // subsetI sHD /= /aperm.
rewrite !(sameP setIidPl eqP) !eqEsubset !subsetIl; apply: eq_subset_r => x.
rewrite !inE; apply: andb_id2l => Hx; have Gx: x \in G := subsetP sHG x Hx.
have Dax: a x \in D by rewrite (subsetP sGD) // Aut_closed.
by rewrite Aut_isomE // -!sub1set -morphim_set1 // injmSK ?sub1set.
Qed.
rewrite !(sameP setIidPl eqP) !eqEsubset !subsetIl; apply: eq_subset_r => x.
rewrite !inE; apply: andb_id2l => Hx; have Gx: x \in G := subsetP sHG x Hx.
have Dax: a x \in D by rewrite (subsetP sGD) // Aut_closed.
by rewrite Aut_isomE // -!sub1set -morphim_set1 // injmSK ?sub1set.
Qed.
Lemma isom_restr_perm a : a \in Aut G -> fHisom (inH a) = infH (fGisom a).
Proof.
move=> AutGa; case nHa: (a \in 'N(H | 'P)); last first.
by rewrite !triv_restr_perm ?astabs_Aut_isom ?nHa ?morph1.
apply: (eq_Aut (Aut_Aut_isom injf sHD _)) => [|fx Hfx /=].
by rewrite (Aut_restr_perm (morphimS f sHG)) ?Aut_Aut_isom.
have [x Dx Hx def_fx] := morphimP Hfx; have Gx := subsetP sHG x Hx.
rewrite {1}def_fx Aut_isomE ?(Aut_restr_perm sHG) //.
by rewrite !restr_permE ?astabs_Aut_isom // def_fx Aut_isomE.
Qed.
by rewrite !triv_restr_perm ?astabs_Aut_isom ?nHa ?morph1.
apply: (eq_Aut (Aut_Aut_isom injf sHD _)) => [|fx Hfx /=].
by rewrite (Aut_restr_perm (morphimS f sHG)) ?Aut_Aut_isom.
have [x Dx Hx def_fx] := morphimP Hfx; have Gx := subsetP sHG x Hx.
rewrite {1}def_fx Aut_isomE ?(Aut_restr_perm sHG) //.
by rewrite !restr_permE ?astabs_Aut_isom // def_fx Aut_isomE.
Qed.
Lemma restr_perm_isom : isom (inH @* Aut G) (infH @* Aut (f @* G)) fHisom.
Proof.
apply: sub_isom; rewrite ?restr_perm_Aut ?injm_Aut_isom //=.
rewrite -(im_Aut_isom injf sGD) -!morphim_comp.
apply: eq_in_morphim; last exact: isom_restr_perm.
(* TODO: investigate why rewrite does not match in the same order *)
apply/setP=> a; rewrite in_setI [in RHS]in_setI; apply: andb_id2r => AutGa.
(* the middle rewrite was rewrite 2!in_setI *)
rewrite /= inE andbC inE (Aut_restr_perm sHG) //=.
by symmetry; rewrite inE AutGa inE astabs_Aut_isom.
Qed.
rewrite -(im_Aut_isom injf sGD) -!morphim_comp.
apply: eq_in_morphim; last exact: isom_restr_perm.
(* TODO: investigate why rewrite does not match in the same order *)
apply/setP=> a; rewrite in_setI [in RHS]in_setI; apply: andb_id2r => AutGa.
(* the middle rewrite was rewrite 2!in_setI *)
rewrite /= inE andbC inE (Aut_restr_perm sHG) //=.
by symmetry; rewrite inE AutGa inE astabs_Aut_isom.
Qed.
Lemma injm_Aut_sub : Aut_in (Aut (f @* G)) (f @* H) \isog Aut_in (Aut G) H.
Proof.
do 2!rewrite isog_sym (isog_transl _ (Aut_in_isog _ _)).
by rewrite isog_sym (isom_isog _ _ restr_perm_isom) // restr_perm_Aut.
Qed.
by rewrite isog_sym (isom_isog _ _ restr_perm_isom) // restr_perm_Aut.
Qed.
Lemma injm_Aut_full :
(Aut_in (Aut (f @* G)) (f @* H) \isog Aut (f @* H))
= (Aut_in (Aut G) H \isog Aut H).
Proof.
End InjmAutIn.
Section GroupAction.
Variables (aT rT : finGroupType) (D : {set aT}) (R : {set rT}).
Local Notation actT := (action D rT).
Definition is_groupAction (to : actT) :=
{in D, forall a, actperm to a \in Aut R}.
Structure groupAction := GroupAction {gact :> actT; _ : is_groupAction gact}.
Definition clone_groupAction to :=
let: GroupAction _ toA := to return {type of GroupAction for to} -> _ in
fun k => k toA : groupAction.
End GroupAction.
Delimit Scope groupAction_scope with gact.
Bind Scope groupAction_scope with groupAction.
Arguments is_groupAction {aT rT D%_g} R%_g to%_act.
Arguments groupAction {aT rT} D%_g R%_g.
Arguments gact {aT rT D%_g R%_g} to%_gact : rename.
Notation "[ 'groupAction' 'of' to ]" :=
(clone_groupAction (@GroupAction _ _ _ _ to))
(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 & 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.
Arguments gacent {aT rT D%_g R%_g} to%_gact A%_g.
Arguments acts_on_group {aT rT D%_g R%_g} A%_g S%_g to%_gact.
Arguments acts_irreducibly {aT rT D%_g R%_g} A%_g S%_g to%_gact.
Notation "''C_' ( | to ) ( A )" := (gacent to A) : group_scope.
Notation "''C_' ( G | to ) ( A )" := (G :&: 'C_(|to)(A)) : group_scope.
Notation "''C_' ( | to ) [ a ]" := 'C_(|to)([set a]) : group_scope.
Notation "''C_' ( G | to ) [ a ]" := 'C_(G | to)([set a]) : group_scope.
Notation "{ 'acts' A , 'on' 'group' G | to }" := (acts_on_group A G to)
(format "{ 'acts' A , 'on' 'group' G | to }") : type_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
Proof.
Lemma im_actperm_Aut : actperm to @* D \subset Aut R.
Proof.
Lemma gact_out x a : a \in D -> x \notin R -> to x a = x.
Proof.
Lemma gactM : {in D, forall a, {in R &, {morph to^~ a : x y / x * y}}}.
Proof.
move=> a Da /= x y; rewrite -!(actpermE to); apply: morphicP x y.
by rewrite Aut_morphic ?actperm_Aut.
Qed.
by rewrite Aut_morphic ?actperm_Aut.
Qed.
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, forall a (S : {set rT}), S \subset R -> actm to a @* S = to^* S a}.
Variables (a : aT) (A B : {set aT}) (S : {set rT}).
Lemma gacentIdom : 'C_(|to)(D :&: A) = 'C_(|to)(A).
Lemma gacentIim : 'C_(R | to)(A) = 'C_(|to)(A).
Lemma gacentS : A \subset B -> 'C_(|to)(B) \subset 'C_(|to)(A).
Lemma gacentU : 'C_(|to)(A :|: B) = 'C_(|to)(A) :&: 'C_(|to)(B).
Hypotheses (Da : a \in D) (sAD : A \subset D) (sSR : S \subset R).
Lemma gacentE : 'C_(|to)(A) = 'Fix_(R | to)(A).
Lemma gacent1E : 'C_(|to)[a] = 'Fix_(R | to)[a].
Lemma subgacentE : 'C_(S | to)(A) = 'Fix_(S | to)(A).
Lemma subgacent1E : 'C_(S | to)[a] = 'Fix_(S | to)[a].
End RawGroupAction.
Section GroupActionTheory.
Variables aT rT : finGroupType.
Variables (D : {group aT}) (R : {group rT}) (to : groupAction D R).
Implicit Type A B : {set aT}.
Implicit Types G H : {group aT}.
Implicit Type S : {set rT}.
Implicit Types M N : {group rT}.
Lemma gact1 : {in D, forall a, to 1 a = 1}.
Lemma gactV : {in D, forall a, {in R, {morph to^~ a : x / x^-1}}}.
Lemma gactX : {in D, forall a n, {in R, {morph to^~ a : x / x ^+ n}}}.
Lemma gactJ : {in D, forall a, {in R &, {morph to^~ a : x y / x ^ y}}}.
Lemma gactR : {in D, forall a, {in R &, {morph to^~ a : x y / [~ x, y]}}}.
Lemma gact_stable : {acts D, on R | to}.
Proof.
Lemma group_set_gacent A : group_set 'C_(|to)(A).
Proof.
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).
Proof.
rewrite -gacentIdom -gacent_gen ?subsetIl // setIDA genD1 ?group1 //.
by rewrite gacent_gen ?subsetIl // gacentIdom.
Qed.
by rewrite gacent_gen ?subsetIl // gacentIdom.
Qed.
Lemma gacent_cycle a : a \in D -> 'C_(|to)(<[a]>) = 'C_(|to)[a].
Proof.
Lemma gacentY A B :
A \subset D -> B \subset D -> 'C_(|to)(A <*> B) = 'C_(|to)(A) :&: 'C_(|to)(B).
Proof.
Lemma gacentM G H :
G \subset D -> H \subset D -> 'C_(|to)(G * H) = 'C_(|to)(G) :&: 'C_(|to)(H).
Proof.
Lemma astab1 : 'C(1 | to) = D.
Lemma astab_range : 'C(R | to) = 'C(setT | to).
Proof.
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).
Proof.
Lemma astabM M N :
M \subset R -> N \subset R -> 'C(M * N | to) = 'C(M | to) :&: 'C(N | to).
Proof.
Lemma astabs1 : 'N(1 | to) = D.
Proof.
Lemma astabs_range : 'N(R | to) = D.
Proof.
Lemma astabsD1 S : 'N(S^# | to) = 'N(S | to).
Proof.
case S1: (1 \in S); last first.
by rewrite (setDidPl _) // disjoint_sym disjoints_subset sub1set inE S1.
apply/eqP; rewrite eqEsubset andbC -{1}astabsIdom -{1}astabs1 setIC astabsD /=.
by rewrite -{2}(setD1K S1) -astabsIdom -{1}astabs1 astabsU.
Qed.
by rewrite (setDidPl _) // disjoint_sym disjoints_subset sub1set inE S1.
apply/eqP; rewrite eqEsubset andbC -{1}astabsIdom -{1}astabs1 setIC astabsD /=.
by rewrite -{2}(setD1K S1) -astabsIdom -{1}astabs1 astabsU.
Qed.
Lemma gacts_range A : A \subset D -> {acts A, on group R | to}.
Proof.
Lemma acts_subnorm_gacent A : A \subset D ->
[acts 'N_D(A), on 'C_(| to)(A) | to].
Proof.
move=> sAD; rewrite gacentE // actsI ?astabs_range ?subsetIl //.
by rewrite -{2}(setIidPr sAD) acts_subnorm_fix.
Qed.
by rewrite -{2}(setIidPr sAD) acts_subnorm_fix.
Qed.
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].
Proof.
move=> sAD actsB; rewrite actsI //; first by rewrite subIset ?actsB.
by rewrite (subset_trans _ (acts_subnorm_gacent sAD)) ?setSI ?(acts_dom actsB).
Qed.
by rewrite (subset_trans _ (acts_subnorm_gacent sAD)) ?setSI ?(acts_dom actsB).
Qed.
Lemma acts_gen A S :
S \subset R -> [acts A, on S | to] -> [acts A, on <<S>> | to].
Proof.
move=> sSR actsA; apply: {A}subset_trans actsA _.
apply/subsetP=> a nSa; have Da := astabs_dom nSa; rewrite !inE Da.
apply: subset_trans (_ : <<S>> \subset actm to a @*^-1 <<S>>) _.
rewrite gen_subG subsetI sSR; apply/subsetP=> x Sx.
by rewrite inE /= actmE ?mem_gen // astabs_act.
by apply/subsetP=> x /[!inE]; case/andP=> Rx; rewrite /= actmE.
Qed.
apply/subsetP=> a nSa; have Da := astabs_dom nSa; rewrite !inE Da.
apply: subset_trans (_ : <<S>> \subset actm to a @*^-1 <<S>>) _.
rewrite gen_subG subsetI sSR; apply/subsetP=> x Sx.
by rewrite inE /= actmE ?mem_gen // astabs_act.
by apply/subsetP=> x /[!inE]; case/andP=> Rx; rewrite /= actmE.
Qed.
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.
Proof.
Lemma acts_char G M : G \subset D -> M \char R -> [acts G, on M | to].
Proof.
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).
Proof.
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]>.
Proof.
Canonical actby_groupAction := GroupAction actby_is_groupAction.
Lemma gacent_actby B :
'C_(|actby_groupAction)(B) = 'C_(G | to)(A :&: B).
Proof.
End ActBy.
Section Quotient.
Variable H : {group rT}.
Lemma acts_qact_dom_norm : {acts qact_dom to H, on 'N(H) | to}.
Proof.
move=> a HDa /= x; rewrite {2}(('N(H) =P to^~ a @^-1: 'N(H)) _) ?inE {x}//.
rewrite eqEcard (card_preimset _ (act_inj _ _)) leqnn andbT.
apply/subsetP=> x Nx; rewrite inE; move/(astabs_act (H :* x)): HDa.
rewrite mem_rcosets mulSGid ?normG // Nx => /rcosetsP[y Ny defHy].
suffices: to x a \in H :* y by apply: subsetP; rewrite mul_subG ?sub1set ?normG.
by rewrite -defHy; apply: imset_f; apply: rcoset_refl.
Qed.
rewrite eqEcard (card_preimset _ (act_inj _ _)) leqnn andbT.
apply/subsetP=> x Nx; rewrite inE; move/(astabs_act (H :* x)): HDa.
rewrite mem_rcosets mulSGid ?normG // Nx => /rcosetsP[y Ny defHy].
suffices: to x a \in H :* y by apply: subsetP; rewrite mul_subG ?sub1set ?normG.
by rewrite -defHy; apply: imset_f; apply: rcoset_refl.
Qed.
Lemma qact_is_groupAction : is_groupAction (R / H) (to / H).
Proof.
move=> a HDa /=; have Da := astabs_dom HDa.
rewrite inE; apply/andP; split.
apply/subsetP=> Hx /=; case: (cosetP Hx) => x Nx ->{Hx}.
apply: contraR => R'Hx; rewrite actpermE qactE // gact_out //.
by apply: contra R'Hx; apply: mem_morphim.
apply/morphicP=> Hx Hy; rewrite !actpermE.
case/morphimP=> x Nx Gx ->{Hx}; case/morphimP=> y Ny Gy ->{Hy}.
by rewrite -morphM ?qactE ?groupM ?gactM // morphM ?acts_qact_dom_norm.
Qed.
rewrite inE; apply/andP; split.
apply/subsetP=> Hx /=; case: (cosetP Hx) => x Nx ->{Hx}.
apply: contraR => R'Hx; rewrite actpermE qactE // gact_out //.
by apply: contra R'Hx; apply: mem_morphim.
apply/morphicP=> Hx Hy; rewrite !actpermE.
case/morphimP=> x Nx Gx ->{Hx}; case/morphimP=> y Ny Gy ->{Hy}.
by rewrite -morphM ?qactE ?groupM ?gactM // morphM ?acts_qact_dom_norm.
Qed.
Canonical quotient_groupAction := GroupAction qact_is_groupAction.
Lemma qact_domE : H \subset R -> qact_dom to H = 'N(H | to).
Proof.
move=> sHR; apply/setP=> a; apply/idP/idP=> nHa; have Da := astabs_dom nHa.
rewrite !inE Da; apply/subsetP=> x Hx; rewrite inE -(rcoset1 H).
have /rcosetsP[y Ny defHy]: to^~ a @: H \in rcosets H 'N(H).
by rewrite (astabs_act _ nHa); apply/rcosetsP; exists 1; rewrite ?mulg1.
by rewrite (rcoset_eqP (_ : 1 \in H :* y)) -defHy -1?(gact1 Da) mem_setact.
rewrite !inE Da; apply/subsetP=> Hx /[1!inE] /rcosetsP[x Nx ->{Hx}].
apply/imsetP; exists (to x a).
case Rx: (x \in R); last by rewrite gact_out ?Rx.
rewrite inE; apply/subsetP=> _ /imsetP[y Hy ->].
rewrite -(actKVin to Da y) -gactJ // ?(subsetP sHR, astabs_act, groupV) //.
by rewrite memJ_norm // astabs_act ?groupV.
apply/eqP; rewrite rcosetE eqEcard.
rewrite (card_imset _ (act_inj _ _)) !card_rcoset leqnn andbT.
apply/subsetP=> _ /imsetP[y Hxy ->]; rewrite !mem_rcoset in Hxy *.
have Rxy := subsetP sHR _ Hxy; rewrite -(mulgKV x y).
case Rx: (x \in R); last by rewrite !gact_out ?mulgK // 1?groupMl ?Rx.
by rewrite -gactV // -gactM 1?groupMr ?groupV // mulgK astabs_act.
Qed.
rewrite !inE Da; apply/subsetP=> x Hx; rewrite inE -(rcoset1 H).
have /rcosetsP[y Ny defHy]: to^~ a @: H \in rcosets H 'N(H).
by rewrite (astabs_act _ nHa); apply/rcosetsP; exists 1; rewrite ?mulg1.
by rewrite (rcoset_eqP (_ : 1 \in H :* y)) -defHy -1?(gact1 Da) mem_setact.
rewrite !inE Da; apply/subsetP=> Hx /[1!inE] /rcosetsP[x Nx ->{Hx}].
apply/imsetP; exists (to x a).
case Rx: (x \in R); last by rewrite gact_out ?Rx.
rewrite inE; apply/subsetP=> _ /imsetP[y Hy ->].
rewrite -(actKVin to Da y) -gactJ // ?(subsetP sHR, astabs_act, groupV) //.
by rewrite memJ_norm // astabs_act ?groupV.
apply/eqP; rewrite rcosetE eqEcard.
rewrite (card_imset _ (act_inj _ _)) !card_rcoset leqnn andbT.
apply/subsetP=> _ /imsetP[y Hxy ->]; rewrite !mem_rcoset in Hxy *.
have Rxy := subsetP sHR _ Hxy; rewrite -(mulgKV x y).
case Rx: (x \in R); last by rewrite !gact_out ?mulgK // 1?groupMl ?Rx.
by rewrite -gactV // -gactM 1?groupMr ?groupV // mulgK astabs_act.
Qed.
End Quotient.
Section Mod.
Variable H : {group aT}.
Lemma modact_is_groupAction : is_groupAction 'C_(|to)(H) (to %% H).
Proof.
move=> Ha /morphimP[a Na Da ->]; have NDa: a \in 'N_D(H) by apply/setIP.
rewrite inE; apply/andP; split.
apply/subsetP=> x; rewrite 2!inE andbC actpermE /= modactEcond //.
by apply: contraR; case: ifP => // E Rx; rewrite gact_out.
apply/morphicP=> x y /setIP[Rx cHx] /setIP[Ry cHy].
rewrite /= !actpermE /= !modactE ?gactM //.
suffices: x * y \in 'C_(|to)(H) by case/setIP.
by rewrite groupM //; apply/setIP.
Qed.
rewrite inE; apply/andP; split.
apply/subsetP=> x; rewrite 2!inE andbC actpermE /= modactEcond //.
by apply: contraR; case: ifP => // E Rx; rewrite gact_out.
apply/morphicP=> x y /setIP[Rx cHx] /setIP[Ry cHy].
rewrite /= !actpermE /= !modactE ?gactM //.
suffices: x * y \in 'C_(|to)(H) by case/setIP.
by rewrite groupM //; apply/setIP.
Qed.
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.
Proof.
move=> cRH NDa /=; have [Da Na] := setIP NDa.
have [Rx | notRx] := boolP (x \in R).
by rewrite modactE //; apply/afixP=> b /setIP[_ /(subsetP cRH)/astab_act->].
rewrite gact_out //= /modact; case: ifP => // _; rewrite gact_out //.
suffices: a \in D :&: coset H a by case/mem_repr/setIP.
by rewrite inE Da val_coset // rcoset_refl.
Qed.
have [Rx | notRx] := boolP (x \in R).
by rewrite modactE //; apply/afixP=> b /setIP[_ /(subsetP cRH)/astab_act->].
rewrite gact_out //= /modact; case: ifP => // _; rewrite gact_out //.
suffices: a \in D :&: coset H a by case/mem_repr/setIP.
by rewrite inE Da val_coset // rcoset_refl.
Qed.
Lemma gacent_mod G M :
H \subset 'C(M | to) -> G \subset 'N(H) ->
'C_(M | mod_groupAction)(G / H) = 'C_(M | to)(G).
Proof.
move=> cMH nHG; rewrite -gacentIdom gacentE ?subsetIl // setICA.
have sHD: H \subset D by rewrite (subset_trans cMH) ?subsetIl.
rewrite -quotientGI // afix_mod ?setIS // setICA -gacentIim (setIC R) -setIA.
rewrite -gacentE ?subsetIl // gacentIdom setICA (setIidPr _) //.
by rewrite gacentC // ?(subset_trans cMH) ?astabS ?subsetIl // setICA subsetIl.
Qed.
have sHD: H \subset D by rewrite (subset_trans cMH) ?subsetIl.
rewrite -quotientGI // afix_mod ?setIS // setICA -gacentIim (setIC R) -setIA.
rewrite -gacentE ?subsetIl // gacentIdom setICA (setIidPr _) //.
by rewrite gacentC // ?(subset_trans cMH) ?astabS ?subsetIl // setICA subsetIl.
Qed.
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.
Proof.
move=> cMH nHG /mingroupP[/andP[ntM nMG] minM].
apply/mingroupP; rewrite ntM astabs_mod ?quotientS //; split=> // L modL ntL.
have cLH: H \subset 'C(L | to) by rewrite (subset_trans cMH) ?astabS //.
apply: minM => //; case/andP: modL => ->; rewrite astabs_mod ?quotientSGK //.
by rewrite (subset_trans cLH) ?astab_sub.
Qed.
apply/mingroupP; rewrite ntM astabs_mod ?quotientS //; split=> // L modL ntL.
have cLH: H \subset 'C(L | to) by rewrite (subset_trans cMH) ?astabS //.
apply: minM => //; case/andP: modL => ->; rewrite astabs_mod ?quotientSGK //.
by rewrite (subset_trans cLH) ?astab_sub.
Qed.
End Mod.
Lemma modact_coset_astab x a :
a \in D -> (to %% 'C(R | to))%act x (coset _ a) = to x a.
Proof.
Lemma acts_irr_mod_astab G M :
acts_irreducibly G M to ->
acts_irreducibly (G / 'C_G(M | to)) M (mod_groupAction _).
Proof.
move=> irrG; have /andP[_ nMG] := mingroupp irrG.
apply: acts_irr_mod irrG; first exact: subsetIr.
by rewrite normsI ?normG // (subset_trans nMG) // astab_norm.
Qed.
apply: acts_irr_mod irrG; first exact: subsetIr.
by rewrite normsI ?normG // (subset_trans nMG) // astab_norm.
Qed.
Section CompAct.
Variables (gT : finGroupType) (G : {group gT}) (f : {morphism G >-> aT}).
Lemma comp_is_groupAction : is_groupAction R (comp_action to f).
Proof.
Lemma gacent_comp U : 'C_(|comp_groupAction)(U) = 'C_(|to)(f @* U).
Proof.
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.
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).
Proof.
apply/setP=> fx; apply/morphimP/idP=> [[x D1x nSx ->] | nSx].
rewrite 2!inE -{1}defD2 mem_morphim //=; apply/subsetP=> _ /imsetP[u Su ->].
by rewrite inE -hfJ ?imset_f // (astabs_act _ nSx).
have [|x D1x _ def_fx] := morphimP (_ : fx \in f @* D1).
by rewrite defD2 (astabs_dom nSx).
exists x => //; rewrite !inE D1x; apply/subsetP=> u Su.
have /imsetP[u' Su' /injh def_u']: h (to1 u x) \in h @: S.
by rewrite hfJ // -def_fx (astabs_act _ nSx) imset_f.
by rewrite inE def_u' ?actsDR ?(subsetP sSR).
Qed.
rewrite 2!inE -{1}defD2 mem_morphim //=; apply/subsetP=> _ /imsetP[u Su ->].
by rewrite inE -hfJ ?imset_f // (astabs_act _ nSx).
have [|x D1x _ def_fx] := morphimP (_ : fx \in f @* D1).
by rewrite defD2 (astabs_dom nSx).
exists x => //; rewrite !inE D1x; apply/subsetP=> u Su.
have /imsetP[u' Su' /injh def_u']: h (to1 u x) \in h @: S.
by rewrite hfJ // -def_fx (astabs_act _ nSx) imset_f.
by rewrite inE def_u' ?actsDR ?(subsetP sSR).
Qed.
Lemma morph_astab : f @* 'C(S | to1) = 'C(h @: S | to2).
Proof.
apply/setP=> fx; apply/morphimP/idP=> [[x D1x cSx ->] | cSx].
rewrite 2!inE -{1}defD2 mem_morphim //=; apply/subsetP=> _ /imsetP[u Su ->].
by rewrite inE -hfJ // (astab_act cSx).
have [|x D1x _ def_fx] := morphimP (_ : fx \in f @* D1).
by rewrite defD2 (astab_dom cSx).
exists x => //; rewrite !inE D1x; apply/subsetP=> u Su.
rewrite inE -(inj_in_eq injh) ?actsDR ?(subsetP sSR) ?hfJ //.
by rewrite -def_fx (astab_act cSx) ?imset_f.
Qed.
rewrite 2!inE -{1}defD2 mem_morphim //=; apply/subsetP=> _ /imsetP[u Su ->].
by rewrite inE -hfJ // (astab_act cSx).
have [|x D1x _ def_fx] := morphimP (_ : fx \in f @* D1).
by rewrite defD2 (astab_dom cSx).
exists x => //; rewrite !inE D1x; apply/subsetP=> u Su.
rewrite inE -(inj_in_eq injh) ?actsDR ?(subsetP sSR) ?hfJ //.
by rewrite -def_fx (astab_act cSx) ?imset_f.
Qed.
Lemma morph_afix : h @: 'Fix_(S | to1)(A) = 'Fix_(h @: S | to2)(f @* A).
Proof.
apply/setP=> hu; apply/imsetP/setIP=> [[u /setIP[Su cAu] ->]|].
split; first by rewrite imset_f.
by apply/afixP=> _ /morphimP[x D1x Ax ->]; rewrite -hfJ ?(afixP cAu).
case=> /imsetP[u Su ->] /afixP c_hu_fA; exists u; rewrite // inE Su.
apply/afixP=> x Ax; have Dx := subsetP sAD1 x Ax.
by apply: injh; rewrite ?actsDR ?(subsetP sSR) ?hfJ // c_hu_fA ?mem_morphim.
Qed.
split; first by rewrite imset_f.
by apply/afixP=> _ /morphimP[x D1x Ax ->]; rewrite -hfJ ?(afixP cAu).
case=> /imsetP[u Su ->] /afixP c_hu_fA; exists u; rewrite // inE Su.
apply/afixP=> x Ax; have Dx := subsetP sAD1 x Ax.
by apply: injh; rewrite ?actsDR ?(subsetP sSR) ?hfJ // c_hu_fA ?mem_morphim.
Qed.
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).
Proof.
have [[_ defD2] [injh _]] := (isomP iso_f, isomP iso_h).
move=> sSR1; rewrite (morphimEsub _ sSR1).
apply: (morph_astabs (gact_stable to1) (injmP injh)) => // u x.
by move/(subsetP sSR1); apply: hfJ.
Qed.
move=> sSR1; rewrite (morphimEsub _ sSR1).
apply: (morph_astabs (gact_stable to1) (injmP injh)) => // u x.
by move/(subsetP sSR1); apply: hfJ.
Qed.
Lemma morph_gastab S : S \subset R1 -> f @* 'C(S | to1) = 'C(h @* S | to2).
Proof.
have [[_ defD2] [injh _]] := (isomP iso_f, isomP iso_h).
move=> sSR1; rewrite (morphimEsub _ sSR1).
apply: (morph_astab (gact_stable to1) (injmP injh)) => // u x.
by move/(subsetP sSR1); apply: hfJ.
Qed.
move=> sSR1; rewrite (morphimEsub _ sSR1).
apply: (morph_astab (gact_stable to1) (injmP injh)) => // u x.
by move/(subsetP sSR1); apply: hfJ.
Qed.
Lemma morph_gacent A : A \subset D1 -> h @* 'C_(|to1)(A) = 'C_(|to2)(f @* A).
Proof.
have [[_ defD2] [injh defR2]] := (isomP iso_f, isomP iso_h).
move=> sAD1; rewrite !gacentE //; first by rewrite -defD2 morphimS.
rewrite morphimEsub ?subsetIl // -{1}defR2 morphimEdom.
exact: (morph_afix (gact_stable to1) (injmP injh)).
Qed.
move=> sAD1; rewrite !gacentE //; first by rewrite -defD2 morphimS.
rewrite morphimEsub ?subsetIl // -{1}defR2 morphimEdom.
exact: (morph_afix (gact_stable to1) (injmP injh)).
Qed.
Lemma morph_gact_irr A M :
A \subset D1 -> M \subset R1 ->
acts_irreducibly (f @* A) (h @* M) to2 = acts_irreducibly A M to1.
Proof.
move=> sAD1 sMR1.
have [[injf defD2] [injh defR2]] := (isomP iso_f, isomP iso_h).
have h_eq1 := morphim_injm_eq1 injh.
apply/mingroupP/mingroupP=> [] [/andP[ntM actAM] minM].
split=> [|U]; first by rewrite -h_eq1 // ntM -(injmSK injf) ?morph_gastabs.
case/andP=> ntU acts_fAU sUM; have sUR1 := subset_trans sUM sMR1.
apply: (injm_morphim_inj injh) => //; apply: minM; last exact: morphimS.
by rewrite h_eq1 // ntU -morph_gastabs ?morphimS.
split=> [|U]; first by rewrite h_eq1 // ntM -morph_gastabs ?morphimS.
case/andP=> ntU acts_fAU sUhM.
have sUhR1 := subset_trans sUhM (morphimS h sMR1).
have sU'M: h @*^-1 U \subset M by rewrite sub_morphpre_injm.
rewrite /= -(minM _ _ sU'M) ?morphpreK // -h_eq1 ?subsetIl // -(injmSK injf) //.
by rewrite morph_gastabs ?(subset_trans sU'M) // morphpreK ?ntU.
Qed.
have [[injf defD2] [injh defR2]] := (isomP iso_f, isomP iso_h).
have h_eq1 := morphim_injm_eq1 injh.
apply/mingroupP/mingroupP=> [] [/andP[ntM actAM] minM].
split=> [|U]; first by rewrite -h_eq1 // ntM -(injmSK injf) ?morph_gastabs.
case/andP=> ntU acts_fAU sUM; have sUR1 := subset_trans sUM sMR1.
apply: (injm_morphim_inj injh) => //; apply: minM; last exact: morphimS.
by rewrite h_eq1 // ntU -morph_gastabs ?morphimS.
split=> [|U]; first by rewrite h_eq1 // ntM -morph_gastabs ?morphimS.
case/andP=> ntU acts_fAU sUhM.
have sUhR1 := subset_trans sUhM (morphimS h sMR1).
have sU'M: h @*^-1 U \subset M by rewrite sub_morphpre_injm.
rewrite /= -(minM _ _ sU'M) ?morphpreK // -h_eq1 ?subsetIl // -(injmSK injf) //.
by rewrite morph_gastabs ?(subset_trans sU'M) // morphpreK ?ntU.
Qed.
End MorphGroupAction.
Section InternalActionDefs.
Variable gT : finGroupType.
Implicit Type A : {set gT}.
Implicit Type G : {group gT}.
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.
Proof.
Canonical conjg_groupAction := GroupAction conjg_is_groupAction.
Lemma rcoset_is_action : is_action setT (@rcoset gT).
Proof.
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).
Proof.
Definition conjG_action := Action conjG_is_action.
End InternalActionDefs.
Notation "'R" := (@mulgr_action _) : action_scope.
Notation "'Rs" := (@rcoset_action _) : action_scope.
Notation "'J" := (@conjg_action _) : action_scope.
Notation "'J" := (@conjg_groupAction _) : groupAction_scope.
Notation "'Js" := (@conjsg_action _) : action_scope.
Notation "'JG" := (@conjG_action _) : action_scope.
Notation "'Q" := ('J / _)%act : action_scope.
Notation "'Q" := ('J / _)%gact : groupAction_scope.
Section InternalGroupAction.
Variable gT : finGroupType.
Implicit Types A B : {set gT}.
Implicit Types G H : {group gT}.
Implicit Type x : gT.
Lemma orbitR G x : orbit 'R G x = x *: G.
Proof.
Lemma astab1R x : 'C[x | 'R] = 1.
Lemma astabR G : 'C(G | 'R) = 1.
Lemma astabsR G : 'N(G | 'R) = G.
Proof.
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).
Proof.
Theorem Cayley_isog G : G \isog Cayley_repr G @* G.
Proof.
Lemma orbitJ G x : orbit 'J G x = x ^: G
Proof.
by []. Qed.
Lemma afixJ A : 'Fix_('J)(A) = 'C(A).
Proof.
Lemma astabJ A : 'C(A |'J) = 'C(A).
Proof.
Lemma astab1J x : 'C[x |'J] = 'C[x].
Lemma astabsJ A : 'N(A | 'J) = 'N(A).
Proof.
Lemma setactJ A x : 'J^*%act A x = A :^ x
Proof.
by []. Qed.
Lemma gacentJ A : 'C_(|'J)(A) = 'C(A).
Lemma orbitRs G A : orbit 'Rs G A = rcosets A G
Proof.
by []. Qed.
Lemma sub_afixRs_norms G x A : (G :* x \in 'Fix_('Rs)(A)) = (A \subset G :^ x).
Proof.
Lemma sub_afixRs_norm G x : (G :* x \in 'Fix_('Rs)(G)) = (x \in 'N(G)).
Proof.
Lemma afixRs_rcosets A G : 'Fix_(rcosets G A | 'Rs)(G) = rcosets G 'N_A(G).
Proof.
apply/setP=> Gx; apply/setIP/rcosetsP=> [[/rcosetsP[x Ax ->]]|[x]].
by rewrite sub_afixRs_norm => Nx; exists x; rewrite // inE Ax.
by case/setIP=> Ax Nx ->; rewrite -{1}rcosetE imset_f // sub_afixRs_norm.
Qed.
by rewrite sub_afixRs_norm => Nx; exists x; rewrite // inE Ax.
by case/setIP=> Ax Nx ->; rewrite -{1}rcosetE imset_f // sub_afixRs_norm.
Qed.
Lemma astab1Rs G : 'C[G : {set gT} | 'Rs] = G.
Proof.
Lemma actsRs_rcosets H G : [acts G, on rcosets H G | 'Rs].
Proof.
Lemma transRs_rcosets H G : [transitive G, on rcosets H G | 'Rs].
Proof.
Lemma astabRs_rcosets H G : 'C(rcosets H G | 'Rs) = gcore H G.
Proof.
have transGH := transRs_rcosets H G.
by rewrite (astab_trans_gcore transGH (orbit_refl _ G _)) astab1Rs.
Qed.
by rewrite (astab_trans_gcore transGH (orbit_refl _ G _)) astab1Rs.
Qed.
Lemma orbitJs G A : orbit 'Js G A = A :^: G
Proof.
by []. Qed.
Lemma astab1Js A : 'C[A | 'Js] = 'N(A).
Lemma card_conjugates A G : #|A :^: G| = #|G : 'N_G(A)|.
Proof.
Lemma afixJG G A : (G \in 'Fix_('JG)(A)) = (A \subset 'N(G)).
Lemma astab1JG G : 'C[G | 'JG] = 'N(G).
Proof.
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.
Proof.
Lemma actsQ A B H :
A \subset 'N(H) -> A \subset 'N(B) -> [acts A, on B / H | 'Q].
Proof.
Lemma astabsQ G H : H <| G -> 'N(G / H | 'Q) = 'N(H) :&: 'N(G).
Proof.
Lemma astabQ H Abar : 'C(Abar |'Q) = coset H @*^-1 'C(Abar).
Proof.
Lemma sub_astabQ A H Bbar :
(A \subset 'C(Bbar | 'Q)) = (A \subset 'N(H)) && (A / H \subset 'C(Bbar)).
Proof.
Lemma sub_astabQR A B H :
A \subset 'N(H) -> B \subset 'N(H) ->
(A \subset 'C(B / H | 'Q)) = ([~: A, B] \subset H).
Proof.
move=> nHA nHB; rewrite sub_astabQ nHA /= (sameP commG1P eqP).
by rewrite eqEsubset sub1G andbT -quotientR // quotient_sub1 // comm_subG.
Qed.
by rewrite eqEsubset sub1G andbT -quotientR // quotient_sub1 // comm_subG.
Qed.
Lemma astabQR A H : A \subset 'N(H) ->
'C(A / H | 'Q) = [set x in 'N(H) | [~: [set x], A] \subset H].
Proof.
move=> nHA; apply/setP=> x; rewrite astabQ -morphpreIdom 2!inE -astabQ.
by case nHx: (x \in _); rewrite //= -sub1set sub_astabQR ?sub1set.
Qed.
by case nHx: (x \in _); rewrite //= -sub1set sub_astabQR ?sub1set.
Qed.
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).
Proof.
Section CardClass.
Variable G : {group gT}.
Lemma index_cent1 x : #|G : 'C_G[x]| = #|x ^: G|.
Proof.
Lemma classes_partition : partition (classes G) G.
Proof.
Lemma sum_card_class : \sum_(C in classes G) #|C| = #|G|.
Proof.
Lemma class_formula : \sum_(C in classes G) #|G : 'C_G[repr C]| = #|G|.
Proof.
Lemma abelian_classP : reflect {in G, forall x, x ^: G = [set x]} (abelian G).
Proof.
Lemma card_classes_abelian : abelian G = (#|classes G| == #|G|).
Proof.
have cGgt0 C: C \in classes G -> 1 <= #|C| ?= iff (#|C| == 1)%N.
by case/imsetP=> x _ ->; rewrite eq_sym -index_cent1.
rewrite -sum_card_class -sum1_card (leqif_sum cGgt0).
apply/abelian_classP/forall_inP=> [cGG _ /imsetP[x Gx ->]| cGG x Gx].
by rewrite cGG ?cards1.
apply/esym/eqP; rewrite eqEcard sub1set cards1 class_refl leq_eqVlt cGG //.
exact: imset_f.
Qed.
by case/imsetP=> x _ ->; rewrite eq_sym -index_cent1.
rewrite -sum_card_class -sum1_card (leqif_sum cGgt0).
apply/abelian_classP/forall_inP=> [cGG _ /imsetP[x Gx ->]| cGG x Gx].
by rewrite cGG ?cards1.
apply/esym/eqP; rewrite eqEcard sub1set cards1 class_refl leq_eqVlt cGG //.
exact: imset_f.
Qed.
End CardClass.
End InternalGroupAction.
Lemma gacentQ (gT : finGroupType) (H : {group gT}) (A : {set gT}) :
'C_(|'Q)(A) = 'C(A / H).
Proof.
apply/setP=> Hx; case: (cosetP Hx) => x Nx ->{Hx}.
rewrite -sub_cent1 -astab1J astabC sub1set -(quotientInorm H A).
have defD: qact_dom 'J H = 'N(H) by rewrite qact_domE ?subsetT ?astabsJ.
rewrite !(inE, mem_quotient) //= defD setIC.
apply/subsetP/subsetP=> [cAx _ /morphimP[a Na Aa ->] | cAx a Aa].
by move/cAx: Aa; rewrite !inE qactE ?defD ?morphJ.
have [_ Na] := setIP Aa; move/implyP: (cAx (coset H a)); rewrite mem_morphim //.
by rewrite !inE qactE ?defD ?morphJ.
Qed.
rewrite -sub_cent1 -astab1J astabC sub1set -(quotientInorm H A).
have defD: qact_dom 'J H = 'N(H) by rewrite qact_domE ?subsetT ?astabsJ.
rewrite !(inE, mem_quotient) //= defD setIC.
apply/subsetP/subsetP=> [cAx _ /morphimP[a Na Aa ->] | cAx a Aa].
by move/cAx: Aa; rewrite !inE qactE ?defD ?morphJ.
have [_ Na] := setIP Aa; move/implyP: (cAx (coset H a)); rewrite mem_morphim //.
by rewrite !inE qactE ?defD ?morphJ.
Qed.
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.
Proof.
Section perm_prime_orbit.
Variable (T : finType) (c : {perm T}).
Hypothesis Tp : prime #|T|.
Hypothesis cc : #[c]%g = #|T|.
Let cp : prime #[c]%g
Proof.
Lemma perm_prime_atrans : [transitive <[c]>, on setT | 'P].
Proof.
apply/imsetP; suff /existsP[x] : [exists x, ~~ (#|orbit 'P <[c]> x| < #[c])].
move=> oxT; suff /eqP orbit_x : orbit 'P <[c]> x == setT by exists x.
by rewrite eqEcard subsetT cardsT -cc leqNgt.
apply/forallP => olT; have o1 x : #|orbit 'P <[c]> x| == 1%N.
by case/primeP: cp => _ /(_ _ (dvdn_orbit 'P _ x))/orP[]//; rewrite ltn_eqF.
suff c1 : c = 1%g by rewrite c1 ?order1 in (cp).
apply/permP => x; rewrite perm1; apply/set1P.
by rewrite -(card_orbit1 (eqP (o1 _))) (mem_orbit 'P) ?cycle_id.
Qed.
move=> oxT; suff /eqP orbit_x : orbit 'P <[c]> x == setT by exists x.
by rewrite eqEcard subsetT cardsT -cc leqNgt.
apply/forallP => olT; have o1 x : #|orbit 'P <[c]> x| == 1%N.
by case/primeP: cp => _ /(_ _ (dvdn_orbit 'P _ x))/orP[]//; rewrite ltn_eqF.
suff c1 : c = 1%g by rewrite c1 ?order1 in (cp).
apply/permP => x; rewrite perm1; apply/set1P.
by rewrite -(card_orbit1 (eqP (o1 _))) (mem_orbit 'P) ?cycle_id.
Qed.
Lemma perm_prime_orbit x : orbit 'P <[c]> x = [set: T].
Proof.
Lemma perm_prime_astab x : 'C_<[c]>[x | 'P]%g = 1%g.
Proof.
by apply/card1_trivg/eqP; rewrite -(@eqn_pmul2l #|orbit 'P <[c]> x|)
?card_orbit_stab ?perm_prime_orbit ?cardsT ?muln1 ?prime_gt0// -cc.
Qed.
?card_orbit_stab ?perm_prime_orbit ?cardsT ?muln1 ?prime_gt0// -cc.
Qed.
End perm_prime_orbit.
End AutAct.
Arguments autact {gT} G%_g.
Arguments aut_action {gT} G%_g.
Arguments aut_groupAction {gT} G%_g.
Notation "[ 'Aut' G ]" := (aut_action G) : action_scope.
Notation "[ 'Aut' G ]" := (aut_groupAction G) : groupAction_scope.