(Joint Center)Library pgroup

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
Require Import fintype bigop finset prime fingroup morphism.
Require Import gfunctor automorphism quotient action gproduct cyclic.

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 Arho.-group A.

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

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

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

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

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

Lemma pi'_p'group p pi A : pi^'.-group Ap \in pip^'.-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 pp %| #|G|p \in pi) (pi.-group G).
Implicit Arguments pgroupP [pi G].

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

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

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

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

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

Lemma properG_ltn_log p G H :
  p.-group GH \proper Glogn 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 Pp_group P.

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

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

Lemma coprime_p'group p K R :
  coprime #|K| #|R|p.-group RR :!=: 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) BB \subset A.

Lemma pHall_pgroup pi A B : pi.-Hall(A) Bpi.-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 = Gpi.-group Kpi^'.-group R
  pi.-Hall(G) K pi^'.-Hall(G) R.

Lemma coprime_mulGp_Hall pi G K R :
    K × R = Gpi^'.-group Kpi.-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 rhopi.-Hall(G) H = rho.-Hall(G) H.

Lemma eq_p'Hall pi rho G H : pi =i rhopi^'.-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) Kpi.-Hall(G) K.

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

Lemma pHall_Hall pi A B : pi.-Hall(A) BHall 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 = GHall G K = Hall G H.

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

Lemma coprime_sdprod_Hall_r G K H : K ><| H = Gcoprime #|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 <| Gpi^'.-Hall(G) Hreflect (K ><| H = G) (pi.-Hall(G) K).

Lemma sdprod_normal_pHallP pi K H G :
  K <| Gpi.-Hall(G) Hreflect (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 Gpi.-Hall(G) (H :^ x) = pi.-Hall(G) H.

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

Lemma psubgroupJ pi G H x :
  x \in Gpi.-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 GSylow G (P :^ x) = Sylow G P.

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

Lemma pHall_subl pi G K H :
  H \subset KK \subset Gpi.-Hall(G) Hpi.-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 Gx \in Gpi.-elt x.

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

Lemma p_eltM pi x y : commute x ypi.-elt xpi.-elt ypi.-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 xpi.-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 xpi2.-elt x.

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

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

Lemma eq_constt pi1 pi2 x : pi1 =i pi2x.`_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 xx.`_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 HH \subset G
  commute H MH \subset M.

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

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

Lemma sub_pHall pi H G K :
  pi.-Hall(G) Hpi.-group KH \subset KK \subset GK :=: 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) Hpi.-group GH :=: G.

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

Lemma Cauchy p G : prime pp %| #|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) HH <| GK \subset G(K \subset H) = pi.-group K.

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

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

End PgroupProps.

Implicit Arguments pgroupP [gT pi G].
Implicit Arguments constt1P [gT pi x].

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 <| Gpi.-Hall(G) H.

Lemma setI_normal_Hall G H K :
  H <| Gpi.-Hall(G) HK \subset Gpi.-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 Gpi.-group (f @* G).

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

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

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

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

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

Lemma morphim_Hall G H : H \subset DHall G HHall (f @* G) (f @* H).

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

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

Lemma morphim_Sylow G P : P \subset DSylow G PSylow (f @* G) (f @* P).

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

Lemma morph_constt pi x : x \in Df 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) Kpi.-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 <| GK <| Hpi.-Hall(G / K) (H / K) = pi.-Hall(G) H.

Lemma ltn_log_quotient :
  p.-group GH :!=: 1 → H \subset Glogn 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.

Local Notation ConsPred p := (@Cons nat_pred p%N) (only parsing).
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 HH <| GH \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) HH <| G'O_pi(G) = H.

Lemma eq_Hall_pcore G H :
   pi.-Hall(G) 'O_pi(G)pi.-Hall(G) HH :=: '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) Hreflect ('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 GH :&: '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 <| Gpi.-group Hpcore_mod G pi H = 'O_pi(G).

Lemma pquotient_pcore pi gT (G H : {group gT}) :
  H <| Gpi.-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) Hreflect ('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.

Implicit Arguments sdprod_Hall_pcoreP [gT pi G H].
Implicit Arguments sdprod_Hall_p'coreP [gT pi G H].

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 Dpi.-group (f @* A) = pi.-group A.

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

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

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

Lemma injm_pseries pis G :
  G \subset Df @* 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 Hpi.-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 Hpseries pis G \isog pseries pis H.

End Isog.