Library mathcomp.solvable.pgroup

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


Standard group notions and constructions based on the prime decomposition of the order of the group or its elements: pi.-group G <=> G is a pi-group, i.e., pi.-nat #|G|.
  • > Recall that here and in the sequel pi can be a single prime p.
pi.-subgroup(H) G <=> H is a pi-subgroup of G. := (H \subset G) && pi.-group H.
  • > This is provided mostly as a shorhand, with few associated lemmas. However, we do establish some results on maximal pi-subgroups. pi.-elt x <=> x is a pi-element. := pi.-nat # [x] or pi.-group < [x]>. x.`pi == the pi-constituent of x: the (unique) pi-element y \in < [x]> such that x * y^-1 is a pi'-element. pi.-Hall(G) H <=> H is a Hall pi-subgroup of G. := [&& H \subset G, pi.-group H & pi^'.-nat #|G : H| ].
  • > This is also eqivalent to H \subset G /\ #|H| = #|G|`pi. p.-Sylow(G) P <=> P is a Sylow p-subgroup of G.
  • > This is the display and preferred input notation for p.-Hall(G) P. 'Syl_p(G) == the set of the p-Sylow subgroups of G. := [set P : {group _} | p.-Sylow(G) P]. p_group P <=> P is a p-group for some prime p. Hall G H <=> H is a Hall pi-subgroup of G for some pi. := coprime #|H| #|G : H| && (H \subset G). Sylow G P <=> P is a Sylow p-subgroup of G for some p. := p_group P && Hall G P. 'O_pi(G) == the pi-core (largest normal pi-subgroup) of G.
pcore_mod pi G H == the pi-core of G mod H. := G :&: (coset H @*^-1 'O_pi(G / H)). 'O{pi2, pi1}(G) == the pi1,pi2-core of G. := the pi1-core of G mod 'O_pi2(G).
  • > We have 'O{pi2, pi1}(G) / 'O_pi2(G) = 'O_pi1(G / 'O_pi2(G)) with 'O_pi2(G) <| 'O{pi2, pi1}(G) <| G.
'O{pn, ..., p1}(G) == the p1, ..., pn-core of G. := the p1-core of G mod 'O{pn, ..., p2}(G). Note that notions are always defined on sets even though their name indicates "group" properties; the actual definition of the notion never tests for the group property, since this property will always be provided by a (canonical) group structure. Similarly, p-group properties assume without test that p is a prime.

Set Implicit Arguments.

Import GroupScope.

Section PgroupDefs.

We defer the definition of the functors ('0_p(G), etc) because they need to quantify over the finGroupType explicitly.

Variable gT : finGroupType.
Implicit Type (x : gT) (A B : {set gT}) (pi : nat_pred) (p n : nat).

Definition pgroup pi A := pi.-nat #|A|.

Definition psubgroup pi A B := (B \subset A) && pgroup pi B.

Definition p_group A := pgroup (pdiv #|A|) A.

Definition p_elt pi x := pi.-nat #[x].

Definition constt x pi := x ^+ (chinese #[x]`_pi #[x]`_pi^' 1 0).

Definition Hall A B := (B \subset A) && coprime #|B| #|A : B|.

Definition pHall pi A B := [&& B \subset A, pgroup pi B & pi^'.-nat #|A : B|].

Definition Syl p A := [set P : {group gT} | pHall p A P].

Definition Sylow A B := p_group B && Hall A B.

End PgroupDefs.


Notation "pi .-group" := (pgroup pi)
  (at level 2, format "pi .-group") : group_scope.

Notation "pi .-subgroup ( A )" := (psubgroup pi A)
  (at level 8, format "pi .-subgroup ( A )") : group_scope.

Notation "pi .-elt" := (p_elt pi)
  (at level 2, format "pi .-elt") : group_scope.

Notation "x .`_ pi" := (constt x pi)
  (at level 3, format "x .`_ pi") : group_scope.

Notation "pi .-Hall ( G )" := (pHall pi G)
  (at level 8, format "pi .-Hall ( G )") : group_scope.

Notation "p .-Sylow ( G )" := (nat_pred_of_nat p).-Hall(G)
  (at level 8, format "p .-Sylow ( G )") : group_scope.

Notation "''Syl_' p ( G )" := (Syl p G)
  (at level 8, p at level 2, format "''Syl_' p ( G )") : group_scope.

Section PgroupProps.

Variable gT : finGroupType.
Implicit Types (pi rho : nat_pred) (p : nat).
Implicit Types (x y z : gT) (A B C D : {set gT}) (G H K P Q R : {group gT}).

Lemma trivgVpdiv G : G :=: 1 (exists2 p, prime p & p %| #|G|).

Lemma prime_subgroupVti G H : prime #|G| G \subset H H :&: G = 1.

Lemma pgroupE pi A : pi.-group A = pi.-nat #|A|.

Lemma sub_pgroup pi rho A : {subset pi rho} pi.-group A rho.-group A.

Lemma eq_pgroup pi rho A : pi =i rho pi.-group A = rho.-group A.

Lemma eq_p'group pi rho A : pi =i rho pi^'.-group A = rho^'.-group A.

Lemma pgroupNK pi A : pi^'^'.-group A = pi.-group A.

Lemma pi_pgroup p pi A : p.-group A p \in pi pi.-group A.

Lemma pi_p'group p pi A : pi.-group A p \in pi^' p^'.-group A.

Lemma pi'_p'group p pi A : pi^'.-group A p \in pi p^'.-group A.

Lemma p'groupEpi p G : p^'.-group G = (p \notin \pi(G)).

Lemma pgroup_pi G : \pi(G).-group G.

Lemma partG_eq1 pi G : (#|G|`_pi == 1%N) = pi^'.-group G.

Lemma pgroupP pi G :
  reflect ( p, prime p p %| #|G| p \in pi) (pi.-group G).

Lemma pgroup1 pi : pi.-group [1 gT].

Lemma pgroupS pi G H : H \subset G pi.-group G pi.-group H.

Lemma oddSg G H : H \subset G odd #|G| odd #|H|.

Lemma odd_pgroup_odd p G : odd p p.-group G odd #|G|.

Lemma card_pgroup p G : p.-group G #|G| = (p ^ logn p #|G|)%N.

Lemma properG_ltn_log p G H :
  p.-group G H \proper G logn p #|H| < logn p #|G|.

Lemma pgroupM pi G H : pi.-group (G × H) = pi.-group G && pi.-group H.

Lemma pgroupJ pi G x : pi.-group (G :^ x) = pi.-group G.

Lemma pgroup_p p P : p.-group P p_group P.

Lemma p_groupP P : p_group P exists2 p, prime p & p.-group P.

Lemma pgroup_pdiv p G :
    p.-group G G :!=: 1
  [/\ prime p, p %| #|G| & m, #|G| = p ^ m.+1]%N.

Lemma coprime_p'group p K R :
  coprime #|K| #|R| p.-group R R :!=: 1 p^'.-group K.

Lemma card_Hall pi G H : pi.-Hall(G) H #|H| = #|G|`_pi.

Lemma pHall_sub pi A B : pi.-Hall(A) B B \subset A.

Lemma pHall_pgroup pi A B : pi.-Hall(A) B pi.-group B.

Lemma pHallP pi G H : reflect (H \subset G #|H| = #|G|`_pi) (pi.-Hall(G) H).

Lemma pHallE pi G H : pi.-Hall(G) H = (H \subset G) && (#|H| == #|G|`_pi).

Lemma coprime_mulpG_Hall pi G K R :
    K × R = G pi.-group K pi^'.-group R
  pi.-Hall(G) K pi^'.-Hall(G) R.

Lemma coprime_mulGp_Hall pi G K R :
    K × R = G pi^'.-group K pi.-group R
  pi^'.-Hall(G) K pi.-Hall(G) R.

Lemma eq_in_pHall pi rho G H :
  {in \pi(G), pi =i rho} pi.-Hall(G) H = rho.-Hall(G) H.

Lemma eq_pHall pi rho G H : pi =i rho pi.-Hall(G) H = rho.-Hall(G) H.

Lemma eq_p'Hall pi rho G H : pi =i rho pi^'.-Hall(G) H = rho^'.-Hall(G) H.

Lemma pHallNK pi G H : pi^'^'.-Hall(G) H = pi.-Hall(G) H.

Lemma subHall_Hall pi rho G H K :
  rho.-Hall(G) H {subset pi rho} pi.-Hall(H) K pi.-Hall(G) K.

Lemma subHall_Sylow pi p G H P :
  pi.-Hall(G) H p \in pi p.-Sylow(H) P p.-Sylow(G) P.

Lemma pHall_Hall pi A B : pi.-Hall(A) B Hall A B.

Lemma Hall_pi G H : Hall G H \pi(H).-Hall(G) H.

Lemma HallP G H : Hall G H pi, pi.-Hall(G) H.

Lemma sdprod_Hall G K H : K ><| H = G Hall G K = Hall G H.

Lemma coprime_sdprod_Hall_l G K H : K ><| H = G coprime #|K| #|H| = Hall G K.

Lemma coprime_sdprod_Hall_r G K H : K ><| H = G coprime #|K| #|H| = Hall G H.

Lemma compl_pHall pi K H G :
  pi.-Hall(G) K (H \in [complements to K in G]) = pi^'.-Hall(G) H.

Lemma compl_p'Hall pi K H G :
  pi^'.-Hall(G) K (H \in [complements to K in G]) = pi.-Hall(G) H.

Lemma sdprod_normal_p'HallP pi K H G :
  K <| G pi^'.-Hall(G) H reflect (K ><| H = G) (pi.-Hall(G) K).

Lemma sdprod_normal_pHallP pi K H G :
  K <| G pi.-Hall(G) H reflect (K ><| H = G) (pi^'.-Hall(G) K).

Lemma pHallJ2 pi G H x : pi.-Hall(G :^ x) (H :^ x) = pi.-Hall(G) H.

Lemma pHallJnorm pi G H x : x \in 'N(G) pi.-Hall(G) (H :^ x) = pi.-Hall(G) H.

Lemma pHallJ pi G H x : x \in G pi.-Hall(G) (H :^ x) = pi.-Hall(G) H.

Lemma HallJ G H x : x \in G Hall G (H :^ x) = Hall G H.

Lemma psubgroupJ pi G H x :
  x \in G pi.-subgroup(G) (H :^ x) = pi.-subgroup(G) H.

Lemma p_groupJ P x : p_group (P :^ x) = p_group P.

Lemma SylowJ G P x : x \in G Sylow G (P :^ x) = Sylow G P.

Lemma p_Sylow p G P : p.-Sylow(G) P Sylow G P.

Lemma pHall_subl pi G K H :
  H \subset K K \subset G pi.-Hall(G) H pi.-Hall(K) H.

Lemma Hall1 G : Hall G 1.

Lemma p_group1 : @p_group gT 1.

Lemma Sylow1 G : Sylow G 1.

Lemma SylowP G P : reflect (exists2 p, prime p & p.-Sylow(G) P) (Sylow G P).

Lemma p_elt_exp pi x m : pi.-elt (x ^+ m) = (#[x]`_pi^' %| m).

Lemma mem_p_elt pi x G : pi.-group G x \in G pi.-elt x.

Lemma p_eltM_norm pi x y :
  x \in 'N(<[y]>) pi.-elt x pi.-elt y pi.-elt (x × y).

Lemma p_eltM pi x y : commute x y pi.-elt x pi.-elt y pi.-elt (x × y).

Lemma p_elt1 pi : pi.-elt (1 : gT).

Lemma p_eltV pi x : pi.-elt x^-1 = pi.-elt x.

Lemma p_eltX pi x n : pi.-elt x pi.-elt (x ^+ n).

Lemma p_eltJ pi x y : pi.-elt (x ^ y) = pi.-elt x.

Lemma sub_p_elt pi1 pi2 x : {subset pi1 pi2} pi1.-elt x pi2.-elt x.

Lemma eq_p_elt pi1 pi2 x : pi1 =i pi2 pi1.-elt x = pi2.-elt x.

Lemma p_eltNK pi x : pi^'^'.-elt x = pi.-elt x.

Lemma eq_constt pi1 pi2 x : pi1 =i pi2 x.`_pi1 = x.`_pi2.

Lemma consttNK pi x : x.`_pi^'^' = x.`_pi.

Lemma cycle_constt pi x : x.`_pi \in <[x]>.

Lemma consttV pi x : (x^-1).`_pi = (x.`_pi)^-1.

Lemma constt1 pi : 1.`_pi = 1 :> gT.

Lemma consttJ pi x y : (x ^ y).`_pi = x.`_pi ^ y.

Lemma p_elt_constt pi x : pi.-elt x.`_pi.

Lemma consttC pi x : x.`_pi × x.`_pi^' = x.

Lemma p'_elt_constt pi x : pi^'.-elt (x × (x.`_pi)^-1).

Lemma order_constt pi (x : gT) : #[x.`_pi] = #[x]`_pi.

Lemma consttM pi x y : commute x y (x × y).`_pi = x.`_pi × y.`_pi.

Lemma consttX pi x n : (x ^+ n).`_pi = x.`_pi ^+ n.

Lemma constt1P pi x : reflect (x.`_pi = 1) (pi^'.-elt x).

Lemma constt_p_elt pi x : pi.-elt x x.`_pi = x.

Lemma sub_in_constt pi1 pi2 x :
  {in \pi(#[x]), {subset pi1 pi2}} x.`_pi2.`_pi1 = x.`_pi1.

Lemma prod_constt x : \prod_(0 p < #[x].+1) x.`_p = x.

Lemma max_pgroupJ pi M G x :
    x \in G [max M | pi.-subgroup(G) M]
  [max M :^ x of M | pi.-subgroup(G) M].

Lemma comm_sub_max_pgroup pi H M G :
    [max M | pi.-subgroup(G) M] pi.-group H H \subset G
  commute H M H \subset M.

Lemma normal_sub_max_pgroup pi H M G :
  [max M | pi.-subgroup(G) M] pi.-group H H <| G H \subset M.

Lemma norm_sub_max_pgroup pi H M G :
    [max M | pi.-subgroup(G) M] pi.-group H H \subset G
  H \subset 'N(M) H \subset M.

Lemma sub_pHall pi H G K :
  pi.-Hall(G) H pi.-group K H \subset K K \subset G K :=: H.

Lemma Hall_max pi H G : pi.-Hall(G) H [max H | pi.-subgroup(G) H].

Lemma pHall_id pi H G : pi.-Hall(G) H pi.-group G H :=: G.

Lemma psubgroup1 pi G : pi.-subgroup(G) 1.

Lemma Cauchy p G : prime p p %| #|G| {x | x \in G & #[x] = p}.

These lemmas actually hold for maximal pi-groups, but below we'll derive from the Cauchy lemma that a normal max pi-group is Hall.

Lemma sub_normal_Hall pi G H K :
  pi.-Hall(G) H H <| G K \subset G (K \subset H) = pi.-group K.

Lemma mem_normal_Hall pi H G x :
  pi.-Hall(G) H H <| G x \in G (x \in H) = pi.-elt x.

Lemma uniq_normal_Hall pi H G K :
  pi.-Hall(G) H H <| G [max K | pi.-subgroup(G) K] K :=: H.

End PgroupProps.


Section NormalHall.

Variables (gT : finGroupType) (pi : nat_pred).
Implicit Types G H K : {group gT}.

Lemma normal_max_pgroup_Hall G H :
  [max H | pi.-subgroup(G) H] H <| G pi.-Hall(G) H.

Lemma setI_normal_Hall G H K :
  H <| G pi.-Hall(G) H K \subset G pi.-Hall(K) (H :&: K).

End NormalHall.

Section Morphim.

Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
Implicit Types (pi : nat_pred) (G H P : {group aT}).

Lemma morphim_pgroup pi G : pi.-group G pi.-group (f @* G).

Lemma morphim_odd G : odd #|G| odd #|f @* G|.

Lemma pmorphim_pgroup pi G :
   pi.-group ('ker f) G \subset D pi.-group (f @* G) = pi.-group G.

Lemma morphim_p_index pi G H :
  H \subset D pi.-nat #|G : H| pi.-nat #|f @* G : f @* H|.

Lemma morphim_pHall pi G H :
  H \subset D pi.-Hall(G) H pi.-Hall(f @* G) (f @* H).

Lemma pmorphim_pHall pi G H :
    G \subset D H \subset D pi.-subgroup(H :&: G) ('ker f)
  pi.-Hall(f @* G) (f @* H) = pi.-Hall(G) H.

Lemma morphim_Hall G H : H \subset D Hall G H Hall (f @* G) (f @* H).

Lemma morphim_pSylow p G P :
  P \subset D p.-Sylow(G) P p.-Sylow(f @* G) (f @* P).

Lemma morphim_p_group P : p_group P p_group (f @* P).

Lemma morphim_Sylow G P : P \subset D Sylow G P Sylow (f @* G) (f @* P).

Lemma morph_p_elt pi x : x \in D pi.-elt x pi.-elt (f x).

Lemma morph_constt pi x : x \in D f x.`_pi = (f x).`_pi.

End Morphim.

Section Pquotient.

Variables (pi : nat_pred) (gT : finGroupType) (p : nat) (G H K : {group gT}).
Hypothesis piK : pi.-group K.

Lemma quotient_pgroup : pi.-group (K / H).

Lemma quotient_pHall :
  K \subset 'N(H) pi.-Hall(G) K pi.-Hall(G / H) (K / H).

Lemma quotient_odd : odd #|K| odd #|K / H|.

Lemma pquotient_pgroup : G \subset 'N(K) pi.-group (G / K) = pi.-group G.

Lemma pquotient_pHall :
  K <| G K <| H pi.-Hall(G / K) (H / K) = pi.-Hall(G) H.

Lemma ltn_log_quotient :
  p.-group G H :!=: 1 H \subset G logn p #|G / H| < logn p #|G|.

End Pquotient.

Application of card_Aut_cyclic to internal faithful action on cyclic p-subgroups.
A functor needs to quantify over the finGroupType just beore the set.

Variables (pi : nat_pred) (gT : finGroupType) (A : {set gT}).

Definition pcore := \bigcap_(G | [max G | pi.-subgroup(A) G]) G.

Canonical pcore_group : {group gT} := Eval hnf in [group of pcore].

End PcoreDef.

Notation "''O_' pi ( G )" := (pcore pi G)
  (at level 8, pi at level 2, format "''O_' pi ( G )") : group_scope.
Notation "''O_' pi ( G )" := (pcore_group pi G) : Group_scope.

Section PseriesDefs.

Variables (pis : seq nat_pred) (gT : finGroupType) (A : {set gT}).

Definition pcore_mod pi B := coset B @*^-1 'O_pi(A / B).
Canonical pcore_mod_group pi B : {group gT} :=
  Eval hnf in [group of pcore_mod pi B].

Definition pseries := foldr pcore_mod 1 (rev pis).

Lemma pseries_group_set : group_set pseries.

Canonical pseries_group : {group gT} := group pseries_group_set.

End PseriesDefs.

Notation "''O_{' p1 , .. , pn } ( A )" :=
  (pseries (ConsPred p1 .. (ConsPred pn [::]) ..) A)
  (at level 8, format "''O_{' p1 , .. , pn } ( A )") : group_scope.
Notation "''O_{' p1 , .. , pn } ( A )" :=
  (pseries_group (ConsPred p1 .. (ConsPred pn [::]) ..) A) : Group_scope.

Section PCoreProps.

Variables (pi : nat_pred) (gT : finGroupType).
Implicit Types (A : {set gT}) (G H M K : {group gT}).

Lemma pcore_psubgroup G : pi.-subgroup(G) 'O_pi(G).

Lemma pcore_pgroup G : pi.-group 'O_pi(G).

Lemma pcore_sub G : 'O_pi(G) \subset G.

Lemma pcore_sub_Hall G H : pi.-Hall(G) H 'O_pi(G) \subset H.

Lemma pcore_max G H : pi.-group H H <| G H \subset 'O_pi(G).

Lemma pcore_pgroup_id G : pi.-group G 'O_pi(G) = G.

Lemma pcore_normal G : 'O_pi(G) <| G.

Lemma normal_Hall_pcore H G : pi.-Hall(G) H H <| G 'O_pi(G) = H.

Lemma eq_Hall_pcore G H :
   pi.-Hall(G) 'O_pi(G) pi.-Hall(G) H H :=: 'O_pi(G).

Lemma sub_Hall_pcore G K :
  pi.-Hall(G) 'O_pi(G) K \subset G (K \subset 'O_pi(G)) = pi.-group K.

Lemma mem_Hall_pcore G x :
  pi.-Hall(G) 'O_pi(G) x \in G (x \in 'O_pi(G)) = pi.-elt x.

Lemma sdprod_Hall_pcoreP H G :
  pi.-Hall(G) 'O_pi(G) reflect ('O_pi(G) ><| H = G) (pi^'.-Hall(G) H).

Lemma sdprod_pcore_HallP H G :
  pi^'.-Hall(G) H reflect ('O_pi(G) ><| H = G) (pi.-Hall(G) 'O_pi(G)).

Lemma pcoreJ G x : 'O_pi(G :^ x) = 'O_pi(G) :^ x.

End PCoreProps.

Section MorphPcore.

Implicit Types (pi : nat_pred) (gT rT : finGroupType).

Lemma morphim_pcore pi : GFunctor.pcontinuous (@pcore pi).

Lemma pcoreS pi gT (G H : {group gT}) :
  H \subset G H :&: 'O_pi(G) \subset 'O_pi(H).

Canonical pcore_igFun pi := [igFun by pcore_sub pi & morphim_pcore pi].
Canonical pcore_gFun pi := [gFun by morphim_pcore pi].
Canonical pcore_pgFun pi := [pgFun by morphim_pcore pi].

Lemma pcore_char pi gT (G : {group gT}) : 'O_pi(G) \char G.

Section PcoreMod.

Variable F : GFunctor.pmap.

Lemma pcore_mod_sub pi gT (G : {group gT}) : pcore_mod G pi (F _ G) \subset G.

Lemma quotient_pcore_mod pi gT (G : {group gT}) (B : {set gT}) :
  pcore_mod G pi B / B = 'O_pi(G / B).

Lemma morphim_pcore_mod pi gT rT (D G : {group gT}) (f : {morphism D >-> rT}) :
  f @* pcore_mod G pi (F _ G) \subset pcore_mod (f @* G) pi (F _ (f @* G)).

Lemma pcore_mod_res pi gT rT (D : {group gT}) (f : {morphism D >-> rT}) :
  f @* pcore_mod D pi (F _ D) \subset pcore_mod (f @* D) pi (F _ (f @* D)).

Lemma pcore_mod1 pi gT (G : {group gT}) : pcore_mod G pi 1 = 'O_pi(G).

End PcoreMod.

Lemma pseries_rcons pi pis gT (A : {set gT}) :
  pseries (rcons pis pi) A = pcore_mod A pi (pseries pis A).

Lemma pseries_subfun pis :
   GFunctor.closed (@pseries pis) GFunctor.pcontinuous (@pseries pis).

Lemma pseries_sub pis : GFunctor.closed (@pseries pis).

Lemma morphim_pseries pis : GFunctor.pcontinuous (@pseries pis).

Lemma pseriesS pis : GFunctor.hereditary (@pseries pis).

Canonical pseries_igFun pis := [igFun by pseries_sub pis & morphim_pseries pis].
Canonical pseries_gFun pis := [gFun by morphim_pseries pis].
Canonical pseries_pgFun pis := [pgFun by morphim_pseries pis].

Lemma pseries_char pis gT (G : {group gT}) : pseries pis G \char G.

Lemma pseries_normal pis gT (G : {group gT}) : pseries pis G <| G.

Lemma pseriesJ pis gT (G : {group gT}) x :
  pseries pis (G :^ x) = pseries pis G :^ x.

Lemma pseries1 pi gT (G : {group gT}) : 'O_{pi}(G) = 'O_pi(G).

Lemma pseries_pop pi pis gT (G : {group gT}) :
  'O_pi(G) = 1 pseries (pi :: pis) G = pseries pis G.

Lemma pseries_pop2 pi1 pi2 gT (G : {group gT}) :
  'O_pi1(G) = 1 'O_{pi1, pi2}(G) = 'O_pi2(G).

Lemma pseries_sub_catl pi1s pi2s gT (G : {group gT}) :
  pseries pi1s G \subset pseries (pi1s ++ pi2s) G.

Lemma quotient_pseries pis pi gT (G : {group gT}) :
  pseries (rcons pis pi) G / pseries pis G = 'O_pi(G / pseries pis G).

Lemma pseries_norm2 pi1s pi2s gT (G : {group gT}) :
  pseries pi2s G \subset 'N(pseries pi1s G).

Lemma pseries_sub_catr pi1s pi2s gT (G : {group gT}) :
  pseries pi2s G \subset pseries (pi1s ++ pi2s) G.

Lemma quotient_pseries2 pi1 pi2 gT (G : {group gT}) :
  'O_{pi1, pi2}(G) / 'O_pi1(G) = 'O_pi2(G / 'O_pi1(G)).

Lemma quotient_pseries_cat pi1s pi2s gT (G : {group gT}) :
  pseries (pi1s ++ pi2s) G / pseries pi1s G
    = pseries pi2s (G / pseries pi1s G).

Lemma pseries_catl_id pi1s pi2s gT (G : {group gT}) :
  pseries pi1s (pseries (pi1s ++ pi2s) G) = pseries pi1s G.

Lemma pseries_char_catl pi1s pi2s gT (G : {group gT}) :
  pseries pi1s G \char pseries (pi1s ++ pi2s) G.

Lemma pseries_catr_id pi1s pi2s gT (G : {group gT}) :
  pseries pi2s (pseries (pi1s ++ pi2s) G) = pseries pi2s G.

Lemma pseries_char_catr pi1s pi2s gT (G : {group gT}) :
  pseries pi2s G \char pseries (pi1s ++ pi2s) G.

Lemma pcore_modp pi gT (G H : {group gT}) :
  H <| G pi.-group H pcore_mod G pi H = 'O_pi(G).

Lemma pquotient_pcore pi gT (G H : {group gT}) :
  H <| G pi.-group H 'O_pi(G / H) = 'O_pi(G) / H.

Lemma trivg_pcore_quotient pi gT (G : {group gT}) : 'O_pi(G / 'O_pi(G)) = 1.

Lemma pseries_rcons_id pis pi gT (G : {group gT}) :
  pseries (rcons (rcons pis pi) pi) G = pseries (rcons pis pi) G.

End MorphPcore.

Section EqPcore.

Variables gT : finGroupType.
Implicit Types (pi rho : nat_pred) (G H : {group gT}).

Lemma sub_in_pcore pi rho G :
  {in \pi(G), {subset pi rho}} 'O_pi(G) \subset 'O_rho(G).

Lemma sub_pcore pi rho G : {subset pi rho} 'O_pi(G) \subset 'O_rho(G).

Lemma eq_in_pcore pi rho G : {in \pi(G), pi =i rho} 'O_pi(G) = 'O_rho(G).

Lemma eq_pcore pi rho G : pi =i rho 'O_pi(G) = 'O_rho(G).

Lemma pcoreNK pi G : 'O_pi^'^'(G) = 'O_pi(G).

Lemma eq_p'core pi rho G : pi =i rho 'O_pi^'(G) = 'O_rho^'(G).

Lemma sdprod_Hall_p'coreP pi H G :
  pi^'.-Hall(G) 'O_pi^'(G) reflect ('O_pi^'(G) ><| H = G) (pi.-Hall(G) H).

Lemma sdprod_p'core_HallP pi H G :
  pi.-Hall(G) H reflect ('O_pi^'(G) ><| H = G) (pi^'.-Hall(G) 'O_pi^'(G)).

Lemma pcoreI pi rho G : 'O_[predI pi & rho](G) = 'O_pi('O_rho(G)).

Lemma bigcap_p'core pi G :
  G :&: \bigcap_(p < #|G|.+1 | (p : nat) \in pi) 'O_p^'(G) = 'O_pi^'(G).

Lemma coprime_pcoreC (rT : finGroupType) pi G (R : {group rT}) :
  coprime #|'O_pi(G)| #|'O_pi^'(R)|.

Lemma TI_pcoreC pi G H : 'O_pi(G) :&: 'O_pi^'(H) = 1.

Lemma pcore_setI_normal pi G H : H <| G 'O_pi(G) :&: H = 'O_pi(H).

End EqPcore.


Section Injm.

Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
Hypothesis injf : 'injm f.
Implicit Types (A : {set aT}) (G H : {group aT}).

Lemma injm_pgroup pi A : A \subset D pi.-group (f @* A) = pi.-group A.

Lemma injm_pelt pi x : x \in D pi.-elt (f x) = pi.-elt x.

Lemma injm_pHall pi G H :
  G \subset D H \subset D pi.-Hall(f @* G) (f @* H) = pi.-Hall(G) H.

Lemma injm_pcore pi G : G \subset D f @* 'O_pi(G) = 'O_pi(f @* G).

Lemma injm_pseries pis G :
  G \subset D f @* pseries pis G = pseries pis (f @* G).

End Injm.

Section Isog.

Variables (aT rT : finGroupType) (G : {group aT}) (H : {group rT}).

Lemma isog_pgroup pi : G \isog H pi.-group G = pi.-group H.

Lemma isog_pcore pi : G \isog H 'O_pi(G) \isog 'O_pi(H).

Lemma isog_pseries pis : G \isog H pseries pis G \isog pseries pis H.

End Isog.