Library mathcomp.solvable.pgroup

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.

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).
Implicit Arguments pgroupP [pi 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.

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

Section InnerAutCyclicPgroup.

Variables (gT : finGroupType) (p : nat) (G C : {group gT }).
Hypothesis nCG : G \subset 'N (C ).

Lemma logn_quotient_cent_cyclic_pgroup :
  p .-group C → cyclic C → logn p #|G / 'C_G (C )| ≤ (logn p #|C |).-1.

Lemma p'group_quotient_cent_prime :
  prime p → #|C | %| p → p ^'.-group (G / 'C_G (C )).

End InnerAutCyclicPgroup.

Section PcoreDef.

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.

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