- -

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