+ +

Library mathcomp.solvable.pgroup

+ +

+(* (c) Copyright 2006-2016 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).
+ +
+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. +
+
+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.
+ +
+ +
+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.
+
+