Library MathComp.action

Require Import ssreflect ssrbool ssrfun eqtype ssrnat div seq fintype.
Require Import bigop finset fingroup morphism perm automorphism quotient.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

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.

Delimit Scope action_scope with act.
Bind Scope action_scope with action.
Arguments Scope act_morph [_ group_scope _ _ group_scope].
Arguments Scope is_action [_ group_scope _ _].
Arguments Scope act
  [_ group_scope type_scope action_scope group_scope group_scope].
Arguments Scope clone_action [_ group_scope type_scope action_scope _].

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.
Proof.
split⇒ [a | x a b _ _] /=; last by rewrite toM.
by apply: can_inj (to^~ a^-1) _ ⇒ x; rewrite -toM ?mulgV.
Qed.

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

Arguments Scope setact [_ group_scope _ action_scope group_scope group_scope].
Arguments Scope orbit [_ group_scope _ action_scope group_scope group_scope].
Arguments Scope amove
  [_ group_scope _ action_scope group_scope group_scope group_scope].
Arguments Scope afix [_ group_scope _ action_scope group_scope].
Arguments Scope astab [_ group_scope _ group_scope action_scope].
Arguments Scope astabs [_ group_scope _ group_scope action_scope].
Arguments Scope acts_on [_ group_scope _ group_scope group_scope action_scope].
Arguments Scope atrans [_ group_scope _ group_scope group_scope action_scope].
Arguments Scope faithful [_ group_scope _ group_scope group_scope action_scope].

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

Prenex Implicits orbit amove.

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

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.

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. by case: to ⇒ ? []. Qed.
Implicit Arguments act_inj [].

Lemma actMin x : {in D &, act_morph to x}.
Proof. by case: to ⇒ ? []. Qed.

Lemma actmEfun a : a \in D → actm to a = to^~ a.
Proof. by rewrite /actm ⇒ →. Qed.

Lemma actmE a : a \in D → actm to a =1 to^~ a.
Proof. by move⇒ Da; rewrite actmEfun. Qed.

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. exact: mem_imset. Qed.

Lemma card_setact S a : #|to ^* S a| = #|S|.
Proof. by apply: card_imset; exact: act_inj. Qed.

Lemma setact_is_action : is_action D to ^*.
Proof.
split⇒ [a R S eqRS | a b Da Db S]; last first.
  rewrite /setact /= -imset_comp; apply: eq_imset ⇒ x; exact: actMin.
apply/setP⇒ x; apply/idP/idP⇒ /(mem_setact a).
  by rewrite eqRS ⇒ /imsetP[y Sy /act_inj->].
by rewrite -eqRS ⇒ /imsetP[y Sy /act_inj->].
Qed.

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).
Proof. by apply: (iffP imsetP) ⇒ [] [a]; ∃ a. Qed.

Lemma mem_orbit A x a : a \in A → to x a \in orbit to A x.
Proof. exact: mem_imset. Qed.

Lemma afixP A x : reflect (∀ a, a \in A → to x a = x) (x \in 'Fix_to (A )).
Proof.
rewrite inE; apply: (iffP subsetP) ⇒ [xfix a /xfix | xfix a Aa].
  by rewrite inE ⇒ /eqP.
by rewrite inE xfix.
Qed.

Lemma afixS A B : A \subset B → 'Fix_to (B ) \subset 'Fix_to (A ).
Proof. by move⇒ sAB; apply/subsetP⇒ u; rewrite !inE; exact: subset_trans. Qed.

Lemma afixU A B : 'Fix_to (A :|: B ) = 'Fix_to (A ) :&: 'Fix_to (B ).
Proof. by apply/setP⇒ x; rewrite !inE subUset. Qed.

Lemma afix1P a x : reflect (to x a = x) (x \in 'Fix_to [a ]).
Proof. by rewrite inE sub1set inE; exact: eqP. Qed.

Lemma astabIdom S : 'C_D (S | to ) = 'C (S | to ).
Proof. by rewrite setIA setIid. Qed.

Lemma astab_dom S : {subset 'C (S | to ) ≤ D}.
Proof. by move⇒ a /setIP[]. Qed.

Lemma astab_act S a x : a \in 'C (S | to ) → x \in S → to x a = x.
Proof.
rewrite 2!inE ⇒ /andP[_ cSa] Sx; apply/eqP.
by have:= subsetP cSa x Sx; rewrite inE.
Qed.

Lemma astabS S1 S2 : S1 \subset S2 → 'C (S2 | to ) \subset 'C (S1 | to ).
Proof.
move⇒ sS12; apply/subsetP⇒ x; rewrite !inE ⇒ /andP[->].
exact: subset_trans.
Qed.

Lemma astabsIdom S : 'N_D (S | to ) = 'N (S | to ).
Proof. by rewrite setIA setIid. Qed.

Lemma astabs_dom S : {subset 'N (S | to ) ≤ D}.
Proof. by move⇒ a /setIdP[]. Qed.

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.

Lemma astab_sub S : 'C (S | to ) \subset 'N (S | to ).
Proof.
apply/subsetP⇒ a cSa; rewrite !inE (astab_dom cSa).
by apply/subsetP⇒ x Sx; rewrite inE (astab_act cSa).
Qed.

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.

Lemma astabsI S T : 'N (S | to ) :&: 'N (T | to ) \subset 'N (S :&: T | to ).
Proof.
apply/subsetP⇒ a; rewrite !inE -!andbA preimsetI ⇒ /and4P[-> nSa _ nTa] /=.
by rewrite setISS.
Qed.

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.

Lemma astab1_set S : 'C [S | set_action ] = 'N (S | to ).
Proof.
apply/setP⇒ a; apply/idP/idP⇒ nSa.
  case/setIdP: nSa ⇒ Da; rewrite !inE Da sub1set inE ⇒ /eqP defS.
  by apply/subsetP⇒ x Sx; rewrite inE -defS mem_setact.
by rewrite !inE (astabs_dom nSa) sub1set inE /= astabs_setact.
Qed.

Lemma astabs_set1 x : 'N ([set x ] | to ) = 'C [x | to ].
Proof.
apply/eqP; rewrite eqEsubset astab_sub andbC setIS //.
by apply/subsetP⇒ a; rewrite ?(inE ,sub1set ).
Qed.

Lemma acts_dom A S : [acts A , on S | to ] → A \subset D.
Proof. by move⇒ nSA; rewrite (subset_trans nSA) ?subsetIl. Qed.

Lemma acts_act A S : [acts A , on S | to ] → {acts A , on S | to }.
Proof. by move⇒ nAS a Aa x; rewrite astabs_act ?(subsetP nAS). Qed.

Lemma astabCin A S :
  A \subset D → (A \subset 'C (S | to )) = (S \subset 'Fix_to (A )).
Proof.
move⇒ sAD; apply/subsetP/subsetP⇒ [sAC x xS | sSF a aA].
  by apply/afixP⇒ a aA; exact: astab_act (sAC _ aA) xS.
rewrite !inE (subsetP sAD _ aA); apply/subsetP⇒ x xS.
by move/afixP/(_ _ aA): (sSF _ xS); rewrite inE ⇒ →.
Qed.

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 ).
Proof. by apply/setP⇒ a; rewrite !inE subUset; case: (a \in D). Qed.

Lemma astabsU : 'N (S | to ) :&: 'N (T | to ) \subset 'N (S :|: T | to ).
Proof.
by rewrite -(astabsC S) -(astabsC T) -(astabsC (S :|: T)) setCU astabsI.
Qed.

Lemma astabsD : 'N (S | to ) :&: 'N (T | to ) \subset 'N (S :\: T | to ).
Proof. by rewrite setDE -(astabsC T) astabsI. Qed.

Lemma actsI : [acts A , on S :&: T | to ].
Proof. by apply: subset_trans (astabsI S T); rewrite subsetI AactS. Qed.

Lemma actsU : [acts A , on S :|: T | to ].
Proof. by apply: subset_trans astabsU; rewrite subsetI AactS. Qed.

Lemma actsD : [acts A , on S :\: T | to ].
Proof. by apply: subset_trans astabsD; rewrite subsetI AactS. Qed.

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.
by move⇒ nSA/imsetP[a Aa ->{y}] Sx; rewrite (astabs_act _ (subsetP nSA a Aa)).
Qed.

Lemma subset_faithful A B S :
  B \subset A → [faithful A , on S | to ] → [faithful B , on S | to ].
Proof. by move⇒ sAB; apply: subset_trans; exact: setSI. Qed.

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.
move⇒ nSa; rewrite (reindex_inj (act_inj a)); apply: eq_bigl ⇒ x.
exact: astabs_act.
Qed.

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. by move⇒ nSA /(subsetP nSA); exact: reindex_astabs. Qed.

End Reindex.

End RawAction.

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

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

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

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

Section PartialAction.

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.
Proof. by apply: (act_inj to 1); rewrite -actMin ?mulg1. Qed.

Lemma actKin : {in D, right_loop invg to}.
Proof. by move⇒ a Da /= x; rewrite -actMin ?groupV // mulgV act1. Qed.

Lemma actKVin : {in D, rev_right_loop invg to}.
Proof. by move⇒ a Da /= x; rewrite -{2}(invgK a) actKin ?groupV. Qed.

Lemma setactVin S a : a \in D → to ^* S a ^-1 = to^~ a @^-1: S.
Proof.
by move⇒ Da; apply: can2_imset_pre; [exact: actKVin | exact: actKin].
Qed.

Lemma actXin x a i : a \in D → to x (a ^+ i) = iter i (to^~ a) x.
Proof.
move⇒ Da; elim: i ⇒ /= [|i <-]; first by rewrite act1.
by rewrite expgSr actMin ?groupX.
Qed.

Lemma afix1 : 'Fix_to (1) = setT.
Proof. by apply/setP⇒ x; rewrite !inE sub1set inE act1 eqxx. Qed.

Lemma afixD1 G : 'Fix_to (G ^#) = 'Fix_to (G ).
Proof. by rewrite -{2}(setD1K (group1 G)) afixU afix1 setTI. Qed.

Lemma orbit_refl G x : x \in orbit to G x.
Proof. by rewrite -{1}[x]act1 mem_orbit. Qed.

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

Lemma contra_orbit G x y : x \notin orbit to G y → x != y.
Proof. by apply: contraNneq ⇒ ->; exact: orbit_refl. Qed.

Lemma orbit_in_sym G : G \subset D → symmetric (orbit_rel G).
Proof.
move⇒ sGD; apply: symmetric_from_pre ⇒ x y /imsetP[a Ga].
by move/(canLR (actKin (subsetP sGD a Ga))) <-; rewrite mem_orbit ?groupV.
Qed.

Lemma orbit_in_trans G : G \subset D → transitive (orbit_rel G).
Proof.
move⇒ sGD _ x _ /imsetP[a Ga ->] /imsetP[b Gb ->].
by rewrite -actMin ?mem_orbit ?groupM // (subsetP sGD).
Qed.

Lemma orbit_in_transl G x y :
  G \subset D → y \in orbit to G x → orbit to G y = orbit to G x.
Proof.
move⇒ sGD Gxy; apply/setP⇒ z.
by apply/idP/idP; apply: orbit_in_trans; rewrite // orbit_in_sym.
Qed.

Lemma orbit_in_transr 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.
by move⇒ sGD Gxy; rewrite !(orbit_in_sym _ z) ?(orbit_in_transl _ Gxy).
Qed.

Lemma orbit_act_in x a G :
  G \subset D → a \in G → orbit to G (to x a) = orbit to G x.
Proof. by move⇒ sGD /mem_orbit/orbit_in_transl→. Qed.

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. by move⇒ sGD /mem_orbit/orbit_in_transr→. Qed.

Lemma orbit_inv_in A x y :
  A \subset D → (y \in orbit to A ^-1 x ) = (x \in orbit to A y ).
Proof.
move/subsetP⇒ sAD; apply/imsetP/imsetP⇒ [] [a Aa ->].
  by ∃ a^-1; rewrite -?mem_invg ?actKin // -groupV sAD -?mem_invg.
by ∃ a^-1; rewrite ?memV_invg ?actKin // sAD.
Qed.

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.
move/subsetP⇒ sAD Da; apply/setP⇒ y; apply/imsetP/imsetP⇒ [] [b Ab ->{y}].
  by ∃ (a^-1 × b); rewrite -?actMin ?mulKVg // ?sAD -?mem_lcoset.
by ∃ (a × b); rewrite ?mem_mulg ?set11 ?actMin // sAD.
Qed.

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.

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.

Lemma orbit1P G x : reflect (orbit to G x = [set x ]) (x \in 'Fix_to (G )).
Proof.
apply: (iffP afixP) ⇒ [xfix | xfix a Ga].
  apply/eqP; rewrite eq_sym eqEsubset sub1set -{1}[x]act1 mem_imset //=.
  by apply/subsetP⇒ y; case/imsetP⇒ a Ga ->; rewrite inE xfix.
by apply/set1P; rewrite -xfix mem_imset.
Qed.

Lemma card_orbit1 G x : #|orbit to G x| = 1%N → orbit to G x = [set x ].
Proof.
move⇒ orb1; apply/eqP; rewrite eq_sym eqEcard {}orb1 cards1.
by rewrite sub1set orbit_refl.
Qed.

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_transl→.
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 &, ∀ x y, (y \in orbit to G x ) = (x == y )}
   & ∀ 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 (mem_imset _ Sx)) ?orbit_refl.
have /imsetP[y Xy defxG]: orbit to G x \in pblock P @: X.
  by rewrite (pblock_transversal trXP) ?mem_imset.
suffices /orbitP[a Ga def_y]: y \in orbit to G x by ∃ a; rewrite ?def_y.
by rewrite defxG mem_pblock defS (subsetP sXS).
Qed.

Lemma group_set_astab S : group_set 'C (S | to ).
Proof.
apply/group_setP; split⇒ [|a b cSa cSb].
  by rewrite !inE group1; apply/subsetP⇒ x _; rewrite inE act1.
rewrite !inE groupM ?(@astab_dom _ _ _ to S) //; apply/subsetP⇒ x Sx.
by rewrite inE actMin ?(@astab_dom _ _ _ to S) ?(astab_act _ Sx).
Qed.

Canonical astab_group S := group (group_set_astab S).

Lemma afix_gen_in A : A \subset D → 'Fix_to (<<A >>) = 'Fix_to (A ).
Proof.
move⇒ sAD; apply/eqP; rewrite eqEsubset afixS ?sub_gen //=.
by rewrite -astabCin gen_subG ?astabCin.
Qed.

Lemma afix_cycle_in a : a \in D → 'Fix_to (<[a ]>) = 'Fix_to [a ].
Proof. by move⇒ Da; rewrite afix_gen_in ?sub1set. Qed.

Lemma afixYin A B :
  A \subset D → B \subset D → 'Fix_to (A <*> B ) = 'Fix_to (A ) :&: 'Fix_to (B ).
Proof. by move⇒ sAD sBD; rewrite afix_gen_in ?afixU // subUset sAD. Qed.

Lemma afixMin G H :
  G \subset D → H \subset D → 'Fix_to (G × H ) = 'Fix_to (G ) :&: 'Fix_to (H ).
Proof.
by move⇒ sGD sHD; rewrite -afix_gen_in ?mul_subG // genM_join afixYin.
Qed.

Lemma sub_astab1_in A x :
  A \subset D → (A \subset 'C [x | to ]) = (x \in 'Fix_to (A )).
Proof. by move⇒ sAD; rewrite astabCin ?sub1set. Qed.

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.

Canonical astabs_group S := group (group_set_astabs S).

Lemma astab_norm S : 'N (S | to ) \subset 'N ('C (S | to )).
Proof.
apply/subsetP⇒ a nSa; rewrite inE sub_conjg; apply/subsetP⇒ b cSb.
have [Da Db] := (astabs_dom nSa, astab_dom cSb).
rewrite mem_conjgV !inE groupJ //; apply/subsetP⇒ x Sx.
rewrite inE !actMin ?groupM ?groupV //.
by rewrite (astab_act cSb) ?actKVin ?astabs_act ?groupV.
Qed.

Lemma astab_normal S : 'C (S | to ) <| 'N (S | to ).
Proof. by rewrite /normal astab_sub astab_norm. Qed.

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; exact: 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.
move/subsetP⇒ sGD; apply/subsetP⇒ a Ga; rewrite !inE sGD //.
apply/subsetP⇒ _ /imsetP[b Gb ->].
by rewrite inE -actMin ?sGD // mem_imset ?groupM.
Qed.

Lemma acts_subnorm_fix A : [acts 'N_D (A ), on 'Fix_to (D :&: A ) | to ].
Proof.
apply/subsetP⇒ a nAa; have [Da _] := setIP nAa; rewrite !inE Da.
apply/subsetP⇒ x Cx; rewrite inE; apply/afixP⇒ b DAb.
have [Db _]:= setIP DAb; rewrite -actMin // conjgCV actMin ?groupJ ?groupV //.
by rewrite /= (afixP Cx) // memJ_norm // groupV (subsetP (normsGI _ _) _ nAa).
Qed.

Lemma atrans_orbit G x : [transitive G , on orbit to G x | to ].
Proof. by apply: mem_imset; exact: orbit_refl. Qed.

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.
move⇒ Ga; apply/setP⇒ b; have Da := ssGD Ga.
rewrite mem_rcoset !(inE , sub1set ) !groupMr ?groupV //.
by case Gb: (b \in G); rewrite //= actMin ?groupV ?ssGD ?(canF_eq (actKVin Da)).
Qed.

Lemma amove_orbit : amove to G x @: orbit to G x = rcosets 'C_G [x | to ] G.
Proof.
apply/setP ⇒ Ha; apply/imsetP/rcosetsP⇒ [[y] | [a Ga ->]].
  by case/imsetP⇒ b Gb → ->{Ha y}; ∃ b ⇒ //; rewrite amove_act.
by rewrite -amove_act //; ∃ (to x a); first exact: mem_orbit.
Qed.

Lemma amoveK :
  {in orbit to G x, cancel (amove to G x) (fun Ca ⇒ to x (repr Ca))}.
Proof.
move⇒ _ /orbitP[a Ga <-]; rewrite amove_act //= -[G :&: _]/(gval _).
case: repr_rcosetP ⇒ b; rewrite !(inE , sub1set )⇒ /and3P[Gb _ xbx].
by rewrite actMin ?ssGD ?(eqP xbx).
Qed.

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

End OrbitStabilizer.

Lemma card_orbit_in G x : G \subset D → #|orbit to G x| = #|G : 'C_G [x | to ]|.
Proof.
move⇒ sGD; rewrite orbit_stabilizer 1?card_in_imset //.
exact: can_in_inj (act_reprK _).
Qed.

Lemma card_orbit_in_stab G x :
  G \subset D → (#|orbit to G x| × #|'C_G [x | to ]|)%N = #|G|.
Proof. by move⇒ sGD; rewrite mulnC card_orbit_in ?Lagrange ?subsetIl. Qed.

Lemma acts_sum_card_orbit G S :
  [acts G , on S | to ] → \sum_(T in orbit to G @: S ) #|T| = #|S|.
Proof. by move/orbit_partition/card_partition. Qed.

Lemma astab_setact_in S a : a \in D → 'C (to ^* S a | to ) = 'C (S | to ) :^ a.
Proof.
move⇒ Da; apply/setP⇒ b; rewrite mem_conjg !inE -mem_conjg conjGid //.
apply: andb_id2l ⇒ Db; rewrite sub_imset_pre; apply: eq_subset_r ⇒ x.
by rewrite !inE !actMin ?groupM ?groupV // invgK (canF_eq (actKVin Da)).
Qed.

Lemma astab1_act_in x a : a \in D → 'C [to x a | to ] = 'C [x | to ] :^ a.
Proof. by move⇒ Da; rewrite -astab_setact_in // /setact imset_set1. Qed.

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 (mem S)) /= ⇒ [|a x _]; last 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.
move⇒ sGD /imsetP[x Sx {1}->]; rewrite card_orbit_in //.
by rewrite indexgS // setIS // astabS // sub1set.
Qed.

Lemma atrans_dvd_in G S :
  G \subset D → [transitive G , on S | to ] → #|S| %| #|G|.
Proof.
move⇒ sGD transG; apply: dvdn_trans (atrans_dvd_index_in sGD transG) _.
exact: dvdn_indexg.
Qed.

Lemma atransPin G S :
     G \subset D → [transitive G , on S | to ] →
  ∀ x, x \in S → orbit to G x = S.
Proof. by move⇒ sGD /imsetP[y _ ->] x; exact: orbit_in_transl. Qed.

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}.
Proof. by move⇒ sGD transG x y /(atransPin sGD transG) <- /imsetP. Qed.

Lemma atrans_acts_in G S :
  G \subset D → [transitive G , on S | to ] → [acts G , on S | to ].
Proof.
move⇒ sGD transG; apply/subsetP⇒ a Ga; rewrite !inE (subsetP sGD) //.
by apply/subsetP⇒ x /(atransPin sGD transG) <-; rewrite inE mem_imset.
Qed.

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; ∃ x ⇒ //; apply/setP⇒ y; rewrite -(atransPin sGD trG Sx).
apply/imsetP/imsetP⇒ [] [a]; last by ∃ a; first exact: (subsetP sHG).
rewrite -defG ⇒ /imset2P[c b /setIP[_ cxc] Hb ->] →.
∃ b; rewrite ?actMin ?(astab_dom cxc) ?(subsetP sHD) //.
by rewrite (astab_act cxc) ?inE.
Qed.

End PartialAction.

Arguments Scope orbit_transversal
  [_ group_scope _ action_scope group_scope group_scope].
Implicit Arguments orbit1P [aT D rT to G x].
Implicit Arguments contra_orbit [aT D rT x y].
Prenex Implicits orbit1P.

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.
Proof. by rewrite actMin ?inE. Qed.

Lemma actK : right_loop invg to.
Proof. by move⇒ a; apply: actKin; rewrite inE. Qed.

Lemma actKV : rev_right_loop invg to.
Proof. by move⇒ a; apply: actKVin; rewrite inE. Qed.

Lemma actX x a n : to x (a ^+ n) = iter n (to^~ a) x.
Proof. by elim: n ⇒ [|n /= <-]; rewrite ?act1 // -actM expgSr. Qed.

Lemma actCJ a b x : to (to x a) b = to (to x b) (a ^ b).
Proof. by rewrite !actM actK. Qed.

Lemma actCJV a b x : to (to x a) b = to (to x (b ^ a ^-1)) a.
Proof. by rewrite (actCJ _ a) conjgKV. Qed.

Lemma orbit_sym G x y : (y \in orbit to G x ) = (x \in orbit to G y ).
Proof. by apply: orbit_in_sym; exact: subsetT. Qed.

Lemma orbit_trans G x y z :
  y \in orbit to G x → z \in orbit to G y → z \in orbit to G x.
Proof. by apply: orbit_in_trans; exact: subsetT. Qed.

Lemma orbit_transl G x y : y \in orbit to G x → orbit to G y = orbit to G x.
Proof.
move⇒ Gxy; apply/setP⇒ z; apply/idP/idP; apply: orbit_trans ⇒ //.
by rewrite orbit_sym.
Qed.

Lemma orbit_transr G x y z :
  y \in orbit to G x → (y \in orbit to G z ) = (x \in orbit to G z ).
Proof. by move⇒ Gxy; rewrite orbit_sym (orbit_transl Gxy) orbit_sym. Qed.

Lemma orbit_act G a x: a \in G → orbit to G (to x a) = orbit to G x.
Proof. by move/mem_orbit/orbit_transl; exact. Qed.

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. by move/mem_orbit/orbit_transr; exact. Qed.

Lemma orbit_eq_mem G x y :
  (orbit to G x == orbit to G y ) = (x \in orbit to G y ).
Proof. by apply/eqP/idP⇒ [<-|]; [exact: orbit_refl | exact: orbit_transl]. Qed.

Lemma orbit_inv A x y : (y \in orbit to A ^-1 x ) = (x \in orbit to A y ).
Proof. by rewrite orbit_inv_in ?subsetT. Qed.

Lemma orbit_lcoset A a x : orbit to (a *: A) x = orbit to A (to x a).
Proof. by rewrite orbit_lcoset_in ?subsetT ?inE. Qed.

Lemma orbit_rcoset A a x y :
  (to y a \in orbit to (A :* a) x ) = (y \in orbit to A x ).
Proof. by rewrite orbit_rcoset_in ?subsetT ?inE. Qed.

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. by rewrite orbit_conjsg_in ?subsetT ?inE. Qed.

Lemma astabP S a : reflect (∀ x, x \in S → to x a = x) (a \in 'C (S | to )).
Proof.
apply: (iffP idP) ⇒ [cSa x|cSa]; first exact: astab_act.
by rewrite !inE; apply/subsetP⇒ x Sx; rewrite inE cSa.
Qed.

Lemma astab1P x a : reflect (to x a = x) (a \in 'C [x | to ]).
Proof. by rewrite !inE sub1set inE; exact: eqP. Qed.

Lemma sub_astab1 A x : (A \subset 'C [x | to ]) = (x \in 'Fix_to (A )).
Proof. by rewrite sub_astab1_in ?subsetT. Qed.

Lemma astabC A S : (A \subset 'C (S | to )) = (S \subset 'Fix_to (A )).
Proof. by rewrite astabCin ?subsetT. Qed.

Lemma afix_cycle a : 'Fix_to (<[a ]>) = 'Fix_to [a ].
Proof. by rewrite afix_cycle_in ?inE. Qed.

Lemma afix_gen A : 'Fix_to (<<A >>) = 'Fix_to (A ).
Proof. by rewrite afix_gen_in ?subsetT. Qed.

Lemma afixM G H : 'Fix_to (G × H ) = 'Fix_to (G ) :&: 'Fix_to (H ).
Proof. by rewrite afixMin ?subsetT. Qed.

Lemma astabsP S a :
  reflect (∀ x, (to x a \in S ) = (x \in S )) (a \in 'N (S | to )).
Proof.
apply: (iffP idP) ⇒ [nSa x|nSa]; first exact: astabs_act.
by rewrite !inE; apply/subsetP⇒ x; rewrite inE nSa.
Qed.

Lemma card_orbit G x : #|orbit to G x| = #|G : 'C_G [x | to ]|.
Proof. by rewrite card_orbit_in ?subsetT. Qed.

Lemma dvdn_orbit G x : #|orbit to G x| %| #|G|.
Proof. by rewrite card_orbit dvdn_indexg. Qed.

Lemma card_orbit_stab G x : (#|orbit to G x| × #|'C_G [x | to ]|)%N = #|G|.
Proof. by rewrite mulnC card_orbit Lagrange ?subsetIl. Qed.

Lemma actsP A S : reflect {acts A , on S | to } [acts A , on S | to ].
Proof.
apply: (iffP idP) ⇒ [nSA x|nSA]; first exact: acts_act.
by apply/subsetP⇒ a Aa; rewrite !inE; apply/subsetP⇒ x; rewrite inE nSA.
Qed.
Implicit Arguments actsP [A S].

Lemma setact_orbit A x b : to ^* (orbit to A x) b = orbit to (A :^ b) (to x b).
Proof.
apply/setP⇒ y; apply/idP/idP⇒ /imsetP[_ /imsetP[a Aa ->] ->{y}].
  by rewrite actCJ mem_orbit ?memJ_conjg.
by rewrite -actCJ mem_setact ?mem_orbit.
Qed.

Lemma astab_setact S a : 'C (to ^* S a | to ) = 'C (S | to ) :^ a.
Proof.
apply/setP⇒ b; rewrite mem_conjg.
apply/astabP/astabP⇒ stab x ⇒ [Sx|].
  by rewrite conjgE invgK !actM stab ?actK //; apply/imsetP; ∃ x.
by case/imsetP⇒ y Sy ->{x}; rewrite -actM conjgCV actM stab.
Qed.

Lemma astab1_act x a : 'C [to x a | to ] = 'C [x | to ] :^ a.
Proof. by rewrite -astab_setact /setact imset_set1. Qed.

Lemma atransP G S : [transitive G , on S | to ] →
  ∀ x, x \in S → orbit to G x = S.
Proof. by case/imsetP⇒ x _ → y; exact: orbit_transl. Qed.

Lemma atransP2 G S : [transitive G , on S | to ] →
  {in S &, ∀ x y, exists2 a, a \in G & y = to x a}.
Proof. by move⇒ GtrS x y /(atransP GtrS) <- /imsetP. Qed.

Lemma atrans_acts G S : [transitive G , on S | to ] → [acts G , on S | to ].
Proof.
move⇒ GtrS; apply/subsetP⇒ a Ga; rewrite !inE.
by apply/subsetP⇒ x /(atransP GtrS) <-; rewrite inE mem_imset.
Qed.

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; ∃ 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 mem_imset // ltnS leqn0 ⇒ /eqP GtrS.
apply/imsetP; ∃ x ⇒ //; apply/eqP.
rewrite eqEsubset acts_sub_orbit // Sx andbT.
apply/subsetP⇒ y Sy; have:= card0_eq GtrS (orbit to G y).
rewrite !inE /= mem_imset // andbT ⇒ /eqP <-; exact: orbit_refl.
Qed.

Lemma atrans_dvd G S : [transitive G , on S | to ] → #|S| %| #|G|.
Proof. by case/imsetP⇒ x _ ->; exact: dvdn_orbit. Qed.

Lemma acts_fix_norm A B : A \subset 'N (B ) → [acts A , on 'Fix_to (B ) | to ].
Proof.
move⇒ nAB; have:= acts_subnorm_fix to B; rewrite !setTI.
exact: subset_trans.
Qed.

Lemma faithfulP A S :
  reflect (∀ a, a \in A → {in S, to^~ a =1 id} → a = 1)
          [faithful A , on S | to ].
Proof.
apply: (iffP subsetP) ⇒ [Cto1 a Aa Ca | Cto1 a].
  apply/set1P; rewrite Cto1 // inE Aa; exact/astabP.
case/setIP⇒ Aa /astabP Ca; apply/set1P; exact: Cto1.
Qed.

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 //=; last first.
  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. by move⇒ Sx sHG; exact: subgroup_transitivePin (subsetT G). Qed.

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 mem_imset.
  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.
  ∃ (b × a); last by rewrite conjsgM (normP nHb).
  by rewrite inE groupM //; apply/astab1P; rewrite actM -cxba actKV.
apply/imsetP; ∃ 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 mem_imset 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.

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

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).
Proof.
rewrite /ract; case: to ⇒ f [injf fM].
split⇒ // x; exact: (sub_in2 (subsetP sAD)).
Qed.

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

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. by rewrite /= /actby ⇒ → →. Qed.

Lemma afix_actby B : 'Fix_<[nRA ]>(B ) = ~: R :|: 'Fix_to (A :&: B ).
Proof.
apply/setP⇒ x; rewrite !inE /= /actby.
case: (x \in R); last by apply/subsetP⇒ a _; rewrite !inE.
apply/subsetP/subsetP⇒ [cBx a | cABx a Ba]; rewrite !inE.
  by case/andP⇒ Aa /cBx; rewrite inE Aa.
by case: ifP ⇒ //= Aa; have:= cABx a; rewrite !inE Aa ⇒ →.
Qed.

Lemma astab_actby S : 'C (S | <[nRA ]>) = 'C_A (R :&: S | to ).
Proof.
apply/setP⇒ a; rewrite setIA (setIidPl (acts_dom nRA)) !inE.
case Aa: (a \in A) ⇒ //=; apply/subsetP/subsetP⇒ cRSa x ⇒ [|Sx].
  by case/setIP⇒ Rx /cRSa; rewrite !inE actbyE.
by have:= cRSa x; rewrite !inE /= /actby Aa Sx; case: (x \in R) ⇒ //; apply.
Qed.

Lemma astabs_actby S : 'N (S | <[nRA ]>) = 'N_A (R :&: S | to ).
Proof.
apply/setP⇒ a; rewrite setIA (setIidPl (acts_dom nRA)) !inE.
case Aa: (a \in A) ⇒ //=; apply/subsetP/subsetP⇒ nRSa x ⇒ [|Sx].
  by case/setIP⇒ Rx /nRSa; rewrite !inE actbyE ?(acts_act nRA) ?Rx.
have:= nRSa x; rewrite !inE /= /actby Aa Sx ?(acts_act nRA) //.
by case: (x \in R) ⇒ //; apply.
Qed.

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

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. by case: Na ⇒ a /= /(astabs_act (val u)); rewrite !inE valP. Qed.

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.
Proof.
by rewrite /subact -if_neg; case: insubP ⇒ [Na|] → //=; rewrite SubK ⇒ →.
Qed.

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.

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]; rewrite !inE.
  by have:= cSa x Sx; rewrite inE -val_eqE val_subact sDa.
by have:= cSa _ (mem_imset 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]; rewrite !inE.
  by have:= nSa x Sx; rewrite inE ⇒ /(mem_imset val); rewrite val_subact sDa.
have:= nSa _ (mem_imset val Sx); rewrite inE ⇒ /imsetP[y Sy def_y].
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.
move/subsetP⇒ sAD; apply/setP⇒ u.
rewrite !inE !(sameP setIidPl eqP); congr (_ == A).
apply/setP⇒ a; rewrite !inE; apply: andb_id2l ⇒ Aa.
by rewrite -val_eqE val_subact sAD.

Qed.

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

Local Notation subdom := (subact_dom (coset_range H) to ^*).
Fact qact_subdomE : subdom = qact_dom.
Proof. by congr 'N (_|_); apply/setP⇒ Hx; rewrite !inE genGid. Qed.
Lemma qact_proof : qact_dom \subset subdom.
Proof. by rewrite qact_subdomE. Qed.

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 mem_imset.
rewrite inE -(astabs_act _ nNa) ⇒ /rcosetsP[y Ny defHy].
have: to x a \in H :* y by rewrite -defHy (mem_imset (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 =
     (if a \in qact_dom then coset H (to x a) else coset H x ).
Proof.
move⇒ Nx; apply: val_inj; rewrite val_subact //= qact_subdomE.
have: H :* x \in rcosets H 'N (H ) by rewrite -rcosetE mem_imset.
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_transl.
by rewrite rcoset_sym -defHy (mem_imset (_^~_)) ?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. by move⇒ Nx nNa; rewrite qactEcond ?nNa. Qed.

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.

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.

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.
case/setIP⇒ Da Na; case: ifP ⇒ Cx; rewrite /modact Cx //.
rewrite val_coset // -group_modr ?sub1set //.
case: (repr _) / (repr_rcosetP (D :&: H) a) ⇒ a' Ha'.
by rewrite actMin ?(afixP Cx _ Ha') //; case/setIP: Ha'.
Qed.

Lemma modactE x a :
  a \in D → a \in 'N (H ) → x \in range → modact x (coset H a) = to x a.
Proof. by move⇒ Da Na Rx; rewrite modactEcond ?Rx // inE Da. Qed.

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.

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 ).
Proof. by rewrite -astabCin ?subsetIl // subIset ?cSH ?orbT. Qed.

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.
  ∃ 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.
  ∃ 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 //=; last 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.
rewrite /faithful astab_mod ?subsetIr //=.
by rewrite -quotientIG ?subsetIr ?trivg_quotient.
Qed.

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}}.
Proof. by move⇒ a b Da Db; apply/permP⇒ x; rewrite permM !permE actMin. Qed.

Canonical actperm_morphism := Morphism actpermM.

Lemma actpermE a x : actperm a x = to x a.
Proof. by rewrite permE. Qed.

Lemma actpermK x a : aperm x (actperm a) = to x a.
Proof. exact: actpermE. Qed.

Lemma ker_actperm : 'ker actperm = 'C (setT | to ).
Proof.
congr (_ :&: _); apply/setP⇒ a; rewrite !inE /=.
apply/eqP/subsetP⇒ [a1 x _ | a1]; first by rewrite inE -actpermE a1 perm1.
by apply/permP⇒ x; apply/eqP; have:= a1 x; rewrite !inE actpermE perm1 ⇒ →.
Qed.

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.
by move⇒ ffulAS; apply/isomP; rewrite ker_actperm astab_actby setIT.
Qed.

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

Lemma ractpermE : actperm (to \ sAD) =1 actperm to.
Proof. by move⇒ a; apply/permP⇒ x; rewrite !permE. Qed.

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 ).
Proof. by rewrite setIA (setIidPl sAD). Qed.

Lemma astabs_ract S : 'N (S | to \ sAD ) = 'N_A (S | to ).
Proof. by rewrite setIA (setIidPl sAD). Qed.

Lemma acts_ract (B : {set aT }) S :
  [acts B , on S | to \ sAD ] = (B \subset A ) && [acts B , on S | to ].
Proof. by rewrite astabs_ract subsetI. Qed.

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.
split⇒ [a x y | x a b Da Db]; first exact: perm_inj.
by rewrite /mact morphM //= permM.
Qed.

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.
move/injmP⇒ phi_inj; apply/subsetP⇒ a /setIP[Da /astab_act a1].
apply/set1P/phi_inj ⇒ //; apply/permP⇒ x.
by rewrite morph1 perm1 -mactE a1 ?inE.
Qed.

Lemma perm_mact a : actperm morph_action a = phi a.
Proof. by apply/permP⇒ x; rewrite permE. Qed.

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.
split⇒ [e | x e1 e2]; first exact: act_inj.
case/morphpreP⇒ Be1 Dfe1; case/morphpreP⇒ Be2 Dfe2.
by rewrite /comp_act morphM ?actMin.
Qed.
Canonical comp_action := Action comp_is_action.

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.
move⇒ sAB; apply/setP⇒ x; rewrite !inE /morphim (setIidPr sAB).
apply/subsetP/subsetP⇒ [cAx _ /imsetP[a Aa ->] | cfAx a Aa].
  by move/cAx: Aa; rewrite !inE.
by rewrite inE; move/(_ (f a)): cfAx; rewrite inE mem_imset // ⇒ →.
Qed.

Lemma astab_comp S : 'C (S | comp_action ) = f @*^-1 'C (S | to ).
Proof. by apply/setP⇒ x; rewrite !inE -andbA. Qed.

Lemma astabs_comp S : 'N (S | comp_action ) = f @*^-1 'N (S | to ).
Proof. by apply/setP⇒ x; rewrite !inE -andbA. Qed.

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.
by apply: is_total_action ⇒ [x|x a b]; rewrite apermE (perm1 , permM ).
Qed.

Canonical perm_action := Action aperm_is_action.

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

Lemma perm_act1P a : reflect (∀ x, aperm x a = x) (a == 1).
Proof.
apply: (iffP eqP) ⇒ [-> x | a1]; first exact: act1.
by apply/permP⇒ x; rewrite -apermE a1 perm1.
Qed.

Lemma perm_faithful A : [faithful A , on setT | perm_action ].
Proof.
apply/subsetP⇒ a /setIP[Da crTa].
by apply/set1P; apply/permP⇒ x; rewrite -apermE perm1 (astabP crTa) ?inE.
Qed.

Lemma actperm_id p : actperm perm_action p = p.
Proof. by apply/permP⇒ x; rewrite permE. Qed.

End PermAction.

Implicit Arguments perm_act1P [rT a].
Prenex Implicits perm_act1P.

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.
Proof.
move⇒ sAD x; rewrite morphimEsub // /orbit -imset_comp.
by apply: eq_imset ⇒ a //=; rewrite actpermK.
Qed.

Lemma pcycle_actperm (a : aT) :
   a \in D → pcycle (actperm to a) =1 orbit to <[a ]>.
Proof.
move⇒ Da x.
by rewrite pcycleE -orbit_morphim_actperm ?cycle_subG ?morphim_cycle.
Qed.

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).
Proof.
apply/subsetP⇒ x; apply: contraR ⇒ notSx.
by rewrite permE /= /actby (negPf notSx).
Qed.

Lemma triv_restr_perm p : p \notin 'N (S | 'P ) → restr_perm p = 1.
Proof.
move⇒ not_nSp; apply/permP⇒ x.
by rewrite !permE /= /actby (negPf not_nSp) andbF.
Qed.

Lemma restr_permE : {in 'N (S | 'P ) & S, ∀ p, restr_perm p =1 p}.
Proof. by move⇒ y x nSp Sx; rewrite /= actpermE actbyE. Qed.

Lemma ker_restr_perm : 'ker restr_perm = 'C (S | 'P ).
Proof. by rewrite ker_actperm astab_actby setIT (setIidPr (astab_sub _ _)). Qed.

Lemma im_restr_perm p : restr_perm p @: S = S.
Proof. exact: im_perm_on (restr_perm_on p). Qed.

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.
Proof.
move⇒ AutGa.
case nHa: (a \in 'N (H | 'P )); last by rewrite triv_restr_perm ?nHa ?group1.
rewrite inE restr_perm_on; apply/morphicP⇒ x y Hx Hy /=.
by rewrite !restr_permE ?groupM // -(autmE AutGa) morphM ?(subsetP sHG).
Qed.

Lemma restr_perm_Aut : restr_perm H @* Aut G \subset Aut H.
Proof.
by apply/subsetP⇒ a'; case/morphimP⇒ a _ AutGa ->{a'}; exact: Aut_restr_perm.
Qed.

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.

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).
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 exact: Aut_aut.
    by apply/eqP; rewrite eqEcard restr_perm_Aut /= (card_isog iso_rG).
  ∃ (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 exact: 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; ∃ (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 Scope Aut_in [_ group_scope group_scope].

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.

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.

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.
apply/setP⇒ a; rewrite 2!in_setI; apply: andb_id2r ⇒ AutGa.
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.

Lemma injm_Aut_full :
  (Aut_in (Aut (f @* G)) (f @* H) \isog Aut (f @* H))
      = (Aut_in (Aut G) H \isog Aut H ).
Proof.
by rewrite (isog_transl _ injm_Aut_sub) (isog_transr _ (injm_Aut injf sHD)).
Qed.

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, ∀ 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 Scope is_groupAction [_ _ group_scope group_scope action_scope].
Arguments Scope groupAction [_ _ group_scope group_scope].
Arguments Scope gact [_ _ group_scope group_scope groupAction_scope].

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.

Arguments Scope gacent
  [_ _ group_scope group_scope groupAction_scope group_scope].
Arguments Scope acts_on_group
  [_ _ group_scope group_scope group_scope group_scope groupAction_scope].
Arguments Scope acts_irreducibly
  [_ _ group_scope group_scope group_scope group_scope groupAction_scope].

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. Proof. by case: to. Qed.

Lemma im_actperm_Aut : actperm to @* D \subset Aut R.
Proof. by apply/subsetP⇒ _ /morphimP[a _ Da ->]; exact: actperm_Aut. Qed.

Lemma gact_out x a : a \in D → x \notin R → to x a = x.
Proof. by move⇒ Da Rx; rewrite -actpermE (out_Aut _ Rx) ?actperm_Aut. Qed.

Lemma gactM : {in D, ∀ 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.

Lemma actmM a : {in R &, {morph actm to a : x y / x × y}}.
Proof. rewrite /actm; case: ifP ⇒ //; exact: gactM. Qed.

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}.
Proof. by move⇒ a Da /= S sSR; rewrite /morphim /= actmEfun ?(setIidPr _). Qed.

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

Lemma gacentIdom : 'C_(|to )(D :&: A ) = 'C_(|to )(A ).
Proof. by rewrite /gacent setIA setIid. Qed.

Lemma gacentIim : 'C_(R | to )(A ) = 'C_(|to )(A ).
Proof. by rewrite setIA setIid. Qed.

Lemma gacentS : A \subset B → 'C_(|to )(B ) \subset 'C_(|to )(A ).
Proof. by move⇒ sAB; rewrite !(setIS , afixS ). Qed.

Lemma gacentU : 'C_(|to )(A :|: B ) = 'C_(|to )(A ) :&: 'C_(|to )(B ).
Proof. by rewrite -setIIr -afixU -setIUr. Qed.

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

Lemma gacentE : 'C_(|to )(A ) = 'Fix_(R | to )(A ).
Proof. by rewrite -{2}(setIidPr sAD). Qed.

Lemma gacent1E : 'C_(|to )[a ] = 'Fix_(R | to )[a ].
Proof. by rewrite /gacent [D :&: _](setIidPr _) ?sub1set. Qed.

Lemma subgacentE : 'C_(S | to )(A ) = 'Fix_(S | to )(A ).
Proof. by rewrite gacentE setIA (setIidPl sSR). Qed.

Lemma subgacent1E : 'C_(S | to )[a ] = 'Fix_(S | to )[a ].
Proof. by rewrite gacent1E setIA (setIidPl sSR). Qed.

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}.
Proof. by move⇒ a Da; rewrite /= -actmE ?morph1. Qed.

Lemma gactV : {in D, ∀ a, {in R, {morph to^~ a : x / x^-1}}}.
Proof. by move⇒ a Da /= x Rx; move; rewrite -!actmE ?morphV. Qed.

Lemma gactX : {in D, ∀ a n, {in R, {morph to^~ a : x / x ^+ n}}}.
Proof. by move⇒ a Da /= n x Rx; rewrite -!actmE // morphX. Qed.

Lemma gactJ : {in D, ∀ a, {in R &, {morph to^~ a : x y / x ^ y}}}.
Proof. by move⇒ a Da /= x Rx y Ry; rewrite -!actmE // morphJ. Qed.

Lemma gactR : {in D, ∀ a, {in R &, {morph to^~ a : x y / [~ x, y]}}}.
Proof. by move⇒ a Da /= x Rx y Ry; rewrite -!actmE // morphR. Qed.

Lemma gact_stable : {acts D , on R | to }.
Proof.
apply: acts_act; apply/subsetP⇒ a Da; rewrite !inE Da.
apply/subsetP⇒ x; rewrite inE; apply: contraLR ⇒ R'xa.
by rewrite -(actKin to Da x) gact_out ?groupV.
Qed.

Lemma group_set_gacent A : group_set 'C_(|to )(A ).
Proof.
apply/group_setP; split⇒ [|x y].
  by rewrite !inE group1; apply/subsetP⇒ a /setIP[Da _]; rewrite inE gact1.
case/setIP⇒ Rx /afixP cAx /setIP[Ry /afixP cAy].
rewrite inE groupM //; apply/afixP⇒ a Aa.
by rewrite gactM ?cAx ?cAy //; case/setIP: Aa.
Qed.

Canonical gacent_group A := Group (group_set_gacent A).

Lemma gacent1 : 'C_(|to )(1) = R.
Proof. by rewrite /gacent (setIidPr (sub1G _)) afix1 setIT. Qed.

Lemma gacent_gen A : A \subset D → 'C_(|to )(<<A >>) = 'C_(|to )(A ).
Proof.
by move⇒ sAD; rewrite /gacent ![D :&: _](setIidPr _) ?gen_subG ?afix_gen_in.
Qed.

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.

Lemma gacent_cycle a : a \in D → 'C_(|to )(<[a ]>) = 'C_(|to )[a ].
Proof. by move⇒ Da; rewrite gacent_gen ?sub1set. Qed.

Lemma gacentY A B :
  A \subset D → B \subset D → 'C_(|to )(A <*> B ) = 'C_(|to )(A ) :&: 'C_(|to )(B ).
Proof. by move⇒ sAD sBD; rewrite gacent_gen ?gacentU // subUset sAD. Qed.

Lemma gacentM G H :
  G \subset D → H \subset D → 'C_(|to )(G × H ) = 'C_(|to )(G ) :&: 'C_(|to )(H ).
Proof.
by move⇒ sGD sHB; rewrite -gacent_gen ?mul_subG // genM_join gacentY.
Qed.

Lemma astab1 : 'C (1 | to ) = D.
Proof.
by apply/setP⇒ x; rewrite ?(inE , sub1set ) andb_idr //; move/gact1⇒ →.
Qed.

Lemma astab_range : 'C (R | to ) = 'C (setT | to ).
Proof.
apply/eqP; rewrite eqEsubset andbC astabS ?subsetT //=.
apply/subsetP⇒ a cRa; have Da := astab_dom cRa; rewrite !inE Da.
apply/subsetP⇒ x; rewrite -(setUCr R) !inE.
by case/orP⇒ ?; [rewrite (astab_act cRa) | rewrite gact_out].
Qed.

Lemma gacentC A S :
    A \subset D → S \subset R →
  (S \subset 'C_(|to )(A )) = (A \subset 'C (S | to )).
Proof. by move⇒ sAD sSR; rewrite subsetI sSR astabCin // (setIidPr sAD). Qed.

Lemma astab_gen S : S \subset R → 'C (<<S >> | to ) = 'C (S | to ).
Proof.
move⇒ sSR; apply/setP⇒ a; case Da: (a \in D); last by rewrite !inE Da.
by rewrite -!sub1set -!gacentC ?sub1set ?gen_subG.
Qed.

Lemma astabM M N :
  M \subset R → N \subset R → 'C (M × N | to ) = 'C (M | to ) :&: 'C (N | to ).
Proof.
move⇒ sMR sNR; rewrite -astabU -astab_gen ?mul_subG // genM_join.
by rewrite astab_gen // subUset sMR.
Qed.

Lemma astabs1 : 'N (1 | to ) = D.
Proof. by rewrite astabs_set1 astab1. Qed.

Lemma astabs_range : 'N (R | to ) = D.
Proof.
apply/setIidPl; apply/subsetP⇒ a Da; rewrite inE.
by apply/subsetP⇒ x Rx; rewrite inE gact_stable.
Qed.

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.

Lemma gacts_range A : A \subset D → {acts A , on group R | to }.
Proof. by move⇒ sAD; split; rewrite ?astabs_range. Qed.

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.

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.

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; rewrite !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 ].
Proof. by move⇒ sMR sNR nMA nNA; rewrite acts_gen ?actsU // subUset sMR. Qed.

Lemma injm_actm a : 'injm (actm to a ).
Proof.
apply/injmP⇒ x y Rx Ry; rewrite /= /actm; case: ifP ⇒ Da //.
exact: act_inj.
Qed.

Lemma im_actm a : actm to a @* R = R.
Proof.
apply/eqP; rewrite eqEcard (card_injm (injm_actm a)) // leqnn andbT.
apply/subsetP⇒ _ /morphimP[x Rx _ ->] /=.
by rewrite /actm; case: ifP ⇒ // Da; rewrite gact_stable.
Qed.

Lemma acts_char G M : G \subset D → M \char R → [acts G , on M | to ].
Proof.
move⇒ sGD /charP[sMR charM].
apply/subsetP⇒ a Ga; have Da := subsetP sGD a Ga; rewrite !inE Da.
apply/subsetP⇒ x Mx; have Rx := subsetP sMR x Mx.
by rewrite inE -(charM _ (injm_actm a) (im_actm a)) -actmE // mem_morphim.
Qed.

Lemma gacts_char G M :
  G \subset D → M \char R → {acts G , on group M | to }.
Proof. by move⇒ sGD charM; split; rewrite (acts_char , char_sub ). Qed.

Section Restrict.

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

Lemma ract_is_groupAction : is_groupAction R (to \ sAD).
Proof. by move⇒ a Aa /=; rewrite ractpermE actperm_Aut ?(subsetP sAD). Qed.

Canonical ract_groupAction := GroupAction ract_is_groupAction.

Lemma gacent_ract B : 'C_(|ract_groupAction )(B ) = 'C_(|to )(A :&: B ).
Proof. by rewrite /gacent afix_ract setIA (setIidPr sAD). Qed.

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.
move⇒ a Aa; rewrite /= inE; apply/andP; split.
  apply/subsetP⇒ x; apply: contraR ⇒ Gx.
  by rewrite actpermE /= /actby (negbTE Gx).
apply/morphicP⇒ x y Gx Gy; rewrite !actpermE /= /actby Aa groupM ?Gx ?Gy //=.
by case nGAg; move/acts_dom; do 2!move/subsetP⇒ ?; rewrite gactM; auto.
Qed.

Canonical actby_groupAction := GroupAction actby_is_groupAction.

Lemma gacent_actby B :
  'C_(|actby_groupAction )(B ) = 'C_(G | to )(A :&: B ).
Proof.
rewrite /gacent afix_actby !setIA setIid setIUr setICr set0U.
by have [nAG sGR] := nGAg; rewrite (setIidPr (acts_dom nAG)) (setIidPl sGR).
Qed.

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: mem_imset; exact: 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.

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) -{1}(mulg1 H) -rcosetE mem_imset ?group1.
  by rewrite (@rcoset_transl _ H 1 y) -defHy -1?(gact1 Da) mem_setact.
rewrite !inE Da; apply/subsetP⇒ Hx; rewrite inE ⇒ /rcosetsP[x Nx ->{Hx}].
apply/imsetP; ∃ (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 exact/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.
rewrite groupM //; exact/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.

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.

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.

End Mod.

Lemma modact_coset_astab x a :
  a \in D → (to %% 'C (R | to ))%act x (coset _ a) = to x a.
Proof.
move⇒ Da; apply: modgactE ⇒ {x}//.
rewrite !inE Da; apply/subsetP⇒ _ /imsetP[c Cc ->].
have Dc := astab_dom Cc; rewrite !inE groupJ //.
apply/subsetP⇒ x Rx; rewrite inE conjgE !actMin ?groupM ?groupV //.
by rewrite (astab_act Cc) ?actKVin // gact_stable ?groupV.
Qed.

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.

Section CompAct.

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

Lemma comp_is_groupAction : is_groupAction R (comp_action to f).
Proof.
move⇒ a /morphpreP[Ba Dfa]; apply: etrans (actperm_Aut to Dfa).
by congr (_ \in Aut R); apply/permP⇒ x; rewrite !actpermE.
Qed.
Canonical comp_groupAction := GroupAction comp_is_groupAction.

Lemma gacent_comp U : 'C_(|comp_groupAction )(U ) = 'C_(|to )(f @* U ).
Proof.
rewrite /gacent afix_comp ?subIset ?subxx //.
by rewrite -(setIC U) (setIC D) morphim_setIpre.
Qed.

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 ?mem_imset // (astabs_act _ nSx).
have [|x D1x _ def_fx] := morphimP (_ : fx \in f @* D1).
  by rewrite defD2 (astabs_dom nSx).
∃ 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) mem_imset.
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).
∃ 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) ?mem_imset.
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 mem_imset.
  by apply/afixP⇒ _ /morphimP[x D1x Ax ->]; rewrite -hfJ ?(afixP cAu).
case⇒ /imsetP[u Su ->] /afixP c_hu_fA; ∃ 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); exact: 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); exact: 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 //; last 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.

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.
move⇒ a _; rewrite /= inE; apply/andP; split.
  by apply/subsetP⇒ x _; rewrite inE.
by apply/morphicP⇒ x y _ _; rewrite !actpermE /= conjMg.
Qed.

Canonical conjg_groupAction := GroupAction conjg_is_groupAction.

Lemma rcoset_is_action : is_action setT (@rcoset gT).
Proof.
by apply: is_total_action ⇒ [A|A x y]; rewrite !rcosetE (mulg1 , rcosetM ).
Qed.

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.
apply: is_total_action ⇒ [G | G x y]; apply: val_inj; rewrite /= ?act1 //.
exact: actM.
Qed.

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.

Lemma orbitR G x : orbit 'R G x = x *: G.
Proof. by rewrite -lcosetE. Qed.

Lemma astab1R x : 'C [x | 'R ] = 1.
Proof.
apply/trivgP/subsetP⇒ y cxy.
by rewrite -(mulKg x y) [x × y](astab1P cxy) mulVg set11.
Qed.

Lemma astabR G : 'C (G | 'R ) = 1.
Proof.
apply/trivgP/subsetP⇒ x cGx.
by rewrite -(mul1g x) [1 × x](astabP cGx) group1.
Qed.

Lemma astabsR G : 'N (G | 'R ) = G.
Proof.
apply/setP⇒ x; rewrite !inE -setactVin ?inE //=.
by rewrite -groupV -{1 3}(mulg1 G) rcoset_sym -sub1set -mulGS -!rcosetE.
Qed.

Lemma atransR G : [transitive G , on G | 'R ].
Proof. by rewrite /atrans -{1}(mul1g G) -orbitR mem_imset. Qed.

Lemma faithfulR G : [faithful G , on G | 'R ].
Proof. by rewrite /faithful astabR subsetIr. Qed.

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

Theorem Cayley_isom G : isom G (Cayley_repr G @* G) (Cayley_repr G).
Proof. exact: faithful_isom (faithfulR G). Qed.

Theorem Cayley_isog G : G \isog Cayley_repr G @* G.
Proof. exact: isom_isog (Cayley_isom G). Qed.

Lemma orbitJ G x : orbit 'J G x = x ^: G. Proof. by []. Qed.

Lemma afixJ A : 'Fix_('J )(A ) = 'C (A ).
Proof.
apply/setP⇒ x; apply/afixP/centP⇒ cAx y Ay /=.
  by rewrite /commute conjgC cAx.
by rewrite conjgE cAx ?mulKg.
Qed.

Lemma astabJ A : 'C (A |'J ) = 'C (A ).
Proof.
apply/setP⇒ x; apply/astabP/centP⇒ cAx y Ay /=.
  by apply: esym; rewrite conjgC cAx.
by rewrite conjgE -cAx ?mulKg.
Qed.

Lemma astab1J x : 'C [x |'J ] = 'C [x ].
Proof. by rewrite astabJ cent_set1. Qed.

Lemma astabsJ A : 'N (A | 'J ) = 'N (A ).
Proof. by apply/setP⇒ x; rewrite -2!groupV !inE -conjg_preim -sub_conjg. Qed.

Lemma setactJ A x : 'J ^*%act A x = A :^ x. Proof. by []. Qed.

Lemma gacentJ A : 'C_(|'J )(A ) = 'C (A ).
Proof. by rewrite gacentE ?setTI ?subsetT ?afixJ. Qed.

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.
rewrite inE /=; apply: eq_subset_r ⇒ a.
rewrite inE rcosetE -(can2_eq (rcosetKV x) (rcosetK x)) -!rcosetM.
rewrite eqEcard card_rcoset leqnn andbT mulgA (conjgCV x) mulgK.
by rewrite -{2 3}(mulGid G) mulGS sub1set -mem_conjg.
Qed.

Lemma sub_afixRs_norm G x : (G :* x \in 'Fix_('Rs )(G )) = (x \in 'N (G )).
Proof. by rewrite sub_afixRs_norms -groupV inE sub_conjgV. Qed.

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; ∃ x; rewrite // inE Ax.
by case/setIP⇒ Ax Nx ->; rewrite -{1}rcosetE mem_imset // sub_afixRs_norm.
Qed.

Lemma astab1Rs G : 'C [G : {set gT } | 'Rs ] = G.
Proof.
apply/setP⇒ x.
by apply/astab1P/idP⇒ /= [<- | Gx]; rewrite rcosetE ?rcoset_refl ?rcoset_id.
Qed.

Lemma actsRs_rcosets H G : [acts G , on rcosets H G | 'Rs ].
Proof. by rewrite -orbitRs acts_orbit ?subsetT. Qed.

Lemma transRs_rcosets H G : [transitive G , on rcosets H G | 'Rs ].
Proof. by rewrite -orbitRs atrans_orbit. Qed.

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.

Lemma orbitJs G A : orbit 'Js G A = A :^: G. Proof. by []. Qed.

Lemma astab1Js A : 'C [A | 'Js ] = 'N (A ).
Proof. by apply/setP⇒ x; apply/astab1P/normP. Qed.

Lemma card_conjugates A G : #|A :^: G| = #|G : 'N_G (A )|.
Proof. by rewrite card_orbit astab1Js. Qed.

Lemma afixJG G A : (G \in 'Fix_('JG )(A )) = (A \subset 'N (G )).
Proof. by apply/afixP/normsP⇒ nG x Ax; apply/eqP; move/eqP: (nG x Ax). Qed.

Lemma astab1JG G : 'C [G | 'JG ] = 'N (G ).
Proof.
by apply/setP⇒ x; apply/astab1P/normP⇒ [/congr_group | /group_inj].
Qed.

Lemma dom_qactJ H : qact_dom 'J H = 'N (H ).
Proof. by rewrite qact_domE ?subsetT ?astabsJ. Qed.

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.
case: (cosetP Hy) ⇒ y Ny ->{Hy}.
by rewrite qactEcond // dom_qactJ; case Nx: (x \in 'N (H)); rewrite ?morphJ.
Qed.

Lemma actsQ A B H :
  A \subset 'N (H ) → A \subset 'N (B ) → [acts A , on B / H | 'Q ].
Proof.
by move⇒ nHA nBA; rewrite acts_quotient // subsetI dom_qactJ nHA astabsJ.
Qed.

Lemma astabsQ G H : H <| G → 'N (G / H | 'Q ) = 'N (H ) :&: 'N (G ).
Proof. by move⇒ nsHG; rewrite astabs_quotient // dom_qactJ astabsJ. Qed.

Lemma astabQ H Abar : 'C (Abar |'Q ) = coset H @*^-1 'C (Abar ).
Proof.
apply/setP⇒ x; rewrite inE /= dom_qactJ morphpreE in_setI /=.
apply: andb_id2l ⇒ Nx; rewrite !inE -sub1set centsC cent_set1.
apply: eq_subset_r ⇒ {Abar} Hy; rewrite inE qactJ Nx (sameP eqP conjg_fixP).
by rewrite (sameP cent1P eqP) (sameP commgP eqP).
Qed.

Lemma sub_astabQ A H Bbar :
  (A \subset 'C (Bbar | 'Q )) = (A \subset 'N (H )) && (A / H \subset 'C (Bbar )).
Proof.
rewrite astabQ -morphpreIdom subsetI; apply: andb_id2l ⇒ nHA.
by rewrite -sub_quotient_pre.
Qed.

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.

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.

Lemma quotient_astabQ H Abar : 'C (Abar | 'Q ) / H = 'C (Abar ).
Proof. by rewrite astabQ cosetpreK. Qed.

Lemma conj_astabQ A H x :
  x \in 'N (H ) → 'C (A / H | 'Q ) :^ x = 'C (A :^ x / H | 'Q ).
Proof.
move⇒ nHx; apply/setP⇒ y; rewrite !astabQ mem_conjg !in_setI -mem_conjg.
rewrite -normJ (normP nHx) quotientJ //; apply/andb_id2l ⇒ nHy.
by rewrite !inE centJ morphJ ?groupV ?morphV // -mem_conjg.
Qed.

Section CardClass.

Variable G : {group gT }.

Lemma index_cent1 x : #|G : 'C_G [x ]| = #|x ^: G|.
Proof. by rewrite -astab1J -card_orbit. Qed.

Lemma classes_partition : partition (classes G) G.
Proof. by apply: orbit_partition; apply/actsP⇒ x Gx y; exact: groupJr. Qed.

Lemma sum_card_class : \sum_(C in classes G ) #|C| = #|G|.
Proof. by apply: acts_sum_card_orbit; apply/actsP⇒ x Gx y; exact: groupJr. Qed.

Lemma class_formula : \sum_(C in classes G ) #|G : 'C_G [repr C]| = #|G|.
Proof.
rewrite -sum_card_class; apply: eq_bigr ⇒ _ /imsetP[x Gx ->].
have: x \in x ^: G by rewrite -{1}(conjg1 x) mem_imset.
by case/mem_repr/imsetP⇒ y Gy ->; rewrite index_cent1 classGidl.
Qed.

Lemma abelian_classP : reflect {in G, ∀ x, x ^: G = [set x ]} (abelian G).
Proof.
rewrite /abelian -astabJ astabC.
by apply: (iffP subsetP) ⇒ cGG x Gx; apply/orbit1P; exact: cGG.
Qed.

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

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.
Proof. by apply/permP⇒ x; rewrite permE. Qed.

Lemma autact_is_groupAction : is_groupAction G aut_action.
Proof. by move⇒ a Aa /=; rewrite autactK. Qed.
Canonical aut_groupAction := GroupAction autact_is_groupAction.

End AutAct.

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