Library mathcomp.solvable.pgroup

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import fintype bigop finset prime fingroup morphism.
From mathcomp Require Import gfunctor automorphism quotient action gproduct.
From mathcomp Require Import 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 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.