Library pgroup

 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.                                            


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.
Implicit Types A B : {set gT}.
Implicit Type pi : nat_pred.
Implicit Types 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.
Implicit Type p : nat.
Implicit Types x y z : gT.
Implicit Types A B C D : {set gT}.
Implicit Types G H K P Q R : {group gT}.

Lemma trivgVpdiv : forall G, G :=: 1 \/ (exists2 p, prime p & p %| #|G|).

Lemma prime_subgroupVti : forall G H, prime #|G| -> G \subset H \/ H :&: G = 1.

Lemma pgroupE : forall pi A, pi.-group A = pi.-nat #|A|.

Lemma sub_pgroup : forall pi rho A,
  {subset pi <= rho} -> pi.-group A -> rho.-group A.

Lemma eq_pgroup : forall pi rho A, pi =i rho -> pi.-group A = rho.-group A.

Lemma eq_p'group : forall pi rho A, pi =i rho -> pi^'.-group A = rho^'.-group A.

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

Lemma pi_pgroup : forall p pi A, p.-group A -> p \in pi -> pi.-group A.

Lemma pi_p'group : forall p pi A, pi.-group A -> p \in pi^' -> p^'.-group A.

Lemma pi'_p'group : forall p pi A, pi^'.-group A -> p \in pi -> p^'.-group A.

Lemma p'groupEpi : forall p G, p^'.-group G = (p \notin \pi(G)).

Lemma pgroup_pi : forall G, \pi(G).-group G.

Lemma partG_eq1 : forall pi G, (#|G|`_pi == 1%N) = pi^'.-group G.

Lemma pgroupP : forall pi G,
  reflect (forall p, prime p -> p %| #|G| -> p \in pi) (pi.-group G).
Implicit Arguments pgroupP [pi G].

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

Lemma pgroupS : forall pi G H, H \subset G -> pi.-group G -> pi.-group H.

Lemma oddSg : forall G H, H \subset G -> odd #|G| -> odd #|H|.

Lemma odd_pgroup_odd : forall p G, odd p -> p.-group G -> odd #|G|.

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

Lemma properG_ltn_log : forall p G H,
  p.-group G -> H \proper G -> logn p #|H| < logn p #|G|.

Lemma pgroupM : forall pi G H, pi.-group (G * H) = pi.-group G && pi.-group H.

Lemma pgroupJ : forall pi G x, pi.-group (G :^ x) = pi.-group G.

Lemma pgroup_p : forall p P, p.-group P -> p_group P.

Lemma p_groupP : forall P, p_group P -> exists2 p, prime p & p.-group P.

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

Lemma coprime_p'group : forall p K R,
  coprime #|K| #|R| -> p.-group R -> R :!=: 1 -> p^'.-group K.

Lemma card_Hall : forall pi G H, pi.-Hall(G) H -> #|H| = #|G|`_pi.

Lemma pHall_sub : forall pi A B, pi.-Hall(A) B -> B \subset A.

Lemma pHall_pgroup : forall pi A B, pi.-Hall(A) B -> pi.-group B.

Lemma pHallP : forall pi G H,
  reflect (H \subset G /\ #|H| = #|G|`_pi) (pi.-Hall(G) H).

Lemma pHallE : forall pi G H,
  pi.-Hall(G) H = (H \subset G) && (#|H| == #|G|`_pi).

Lemma coprime_mulpG_Hall : forall 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 : forall 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 : forall pi rho G H,
  {in \pi(G), pi =i rho} -> pi.-Hall(G) H = rho.-Hall(G) H.

Lemma eq_pHall : forall pi rho G H, pi =i rho -> pi.-Hall(G) H = rho.-Hall(G) H.

Lemma eq_p'Hall : forall pi rho G H,
  pi =i rho -> pi^'.-Hall(G) H = rho^'.-Hall(G) H.

Lemma pHallNK : forall pi G H, pi^'^'.-Hall(G) H = pi.-Hall(G) H.

Lemma subHall_Hall : forall pi rho G H K,
  rho.-Hall(G) H -> {subset pi <= rho} -> pi.-Hall(H) K -> pi.-Hall(G) K.

Lemma subHall_Sylow : forall pi p G H P,
  pi.-Hall(G) H -> p \in pi -> p.-Sylow(H) P -> p.-Sylow(G) P.

Lemma pHall_Hall : forall pi A B, pi.-Hall(A) B -> Hall A B.

Lemma Hall_pi : forall G H, Hall G H -> \pi(H).-Hall(G) H.

Lemma HallP : forall G H, Hall G H -> exists pi, pi.-Hall(G) H.

Lemma sdprod_Hall : forall G K H, K ><| H = G -> Hall G K = Hall G H.

Lemma coprime_sdprod_Hall : forall G K H,
  K ><| H = G -> coprime #|K| #|H| = Hall G K.

Lemma compl_pHall : forall pi K H G,
  pi.-Hall(G) K -> (H \in [complements to K in G]) = pi^'.-Hall(G) H.

Lemma compl_p'Hall : forall pi K H G,
  pi^'.-Hall(G) K -> (H \in [complements to K in G]) = pi.-Hall(G) H.

Lemma sdprod_normal_p'HallP : forall pi K H G,
  K <| G -> pi^'.-Hall(G) H -> reflect (K ><| H = G) (pi.-Hall(G) K).

Lemma sdprod_normal_pHallP : forall pi K H G,
  K <| G -> pi.-Hall(G) H -> reflect (K ><| H = G) (pi^'.-Hall(G) K).

Lemma pHallJ2 : forall pi G H x,
   pi.-Hall(G :^ x) (H :^ x) = pi.-Hall(G) H.

Lemma pHallJnorm : forall pi G H x,
  x \in 'N(G) -> pi.-Hall(G) (H :^ x) = pi.-Hall(G) H.

Lemma pHallJ : forall pi G H x,
  x \in G -> pi.-Hall(G) (H :^ x) = pi.-Hall(G) H.

Lemma HallJ : forall G H x, x \in G -> Hall G (H :^ x) = Hall G H.

Lemma psubgroupJ : forall pi G H x,
  x \in G -> pi.-subgroup(G) (H :^ x) = pi.-subgroup(G) H.

Lemma p_groupJ : forall P x, p_group (P :^ x) = p_group P.

Lemma SylowJ : forall G P x, x \in G -> Sylow G (P :^ x) = Sylow G P.

Lemma p_Sylow : forall p G P, p.-Sylow(G) P -> Sylow G P.

Lemma pHall_subl : forall pi G K H,
  H \subset K -> K \subset G -> pi.-Hall(G) H -> pi.-Hall(K) H.

Lemma Hall1 : forall G, Hall G 1.

Lemma p_group1 : @p_group gT 1.

Lemma Sylow1 : forall G, Sylow G 1.

Lemma SylowP : forall G P,
  reflect (exists2 p, prime p & p.-Sylow(G) P) (Sylow G P).

Lemma p_elt_exp : forall pi x m, pi.-elt (x ^+ m) = (#[x]`_pi^' %| m).

Lemma mem_p_elt : forall pi x G, pi.-group G -> x \in G -> pi.-elt x.

Lemma p_eltM_norm : forall pi x y, x \in 'N(<[y]>) ->
  pi.-elt x -> pi.-elt y -> pi.-elt (x * y).

Lemma p_eltM : forall pi x y, commute x y ->
  pi.-elt x -> pi.-elt y -> pi.-elt (x * y).

Lemma p_elt1 : forall pi, pi.-elt (1 : gT).

Lemma p_eltV : forall pi x, pi.-elt x^-1 = pi.-elt x.

Lemma p_eltX : forall pi x n, pi.-elt x -> pi.-elt (x ^+ n).

Lemma p_eltJ : forall pi x y, pi.-elt (x ^ y) = pi.-elt x.

Lemma sub_p_elt : forall pi1 pi2 x,
  {subset pi1 <= pi2} -> pi1.-elt x -> pi2.-elt x.

Lemma eq_p_elt : forall pi1 pi2 x, pi1 =i pi2 -> pi1.-elt x = pi2.-elt x.

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

Lemma eq_constt : forall pi1 pi2 x, pi1 =i pi2 -> x.`_pi1 = x.`_pi2.

Lemma consttNK : forall pi x, x.`_pi^'^' = x.`_pi.

Lemma cycle_constt : forall pi (x : gT), x.`_pi \in <[x]>.

Lemma consttV : forall pi x, (x^-1).`_pi = (x.`_pi)^-1.

Lemma constt1 : forall pi, 1.`_pi = 1 :> gT.

Lemma consttJ : forall pi x y, (x ^ y).`_pi = x.`_pi ^ y.

Lemma p_elt_constt : forall pi x, pi.-elt x.`_pi.

Lemma consttC : forall pi x, x.`_pi * x.`_pi^' = x.

Lemma p'_elt_constt : forall pi x, pi^'.-elt (x * (x.`_pi)^-1).

Lemma order_constt : forall pi (x : gT), #[x.`_pi] = #[x]`_pi.

Lemma consttM : forall pi x y, commute x y -> (x * y).`_pi = x.`_pi * y.`_pi.

Lemma consttX : forall pi x n, (x ^+ n).`_pi = x.`_pi ^+ n.

Lemma constt1P : forall pi x, reflect (x.`_pi = 1) (pi^'.-elt x).

Lemma constt_p_elt : forall pi x, pi.-elt x -> x.`_pi = x.

Lemma sub_in_constt : forall pi1 pi2 x,
  {in \pi(#[x]), {subset pi1 <= pi2}} -> x.`_pi2.`_pi1 = x.`_pi1.

Lemma prod_constt : forall x, \prod_(0 <= p < #[x].+1) x.`_p = x.

Lemma max_pgroupJ : forall 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 : forall 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 : forall pi H M G,
  [max M | pi.-subgroup(G) M] -> pi.-group H -> H <| G -> H \subset M.

Lemma norm_sub_max_pgroup : forall 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 : forall pi H G K,
  pi.-Hall(G) H -> pi.-group K -> H \subset K -> K \subset G -> K :=: H.

Lemma Hall_max : forall pi H G, pi.-Hall(G) H -> [max H | pi.-subgroup(G) H].

Lemma pHall_id : forall pi H G, pi.-Hall(G) H -> pi.-group G -> H :=: G.

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

Lemma Cauchy : forall 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 : forall pi G H K,
  pi.-Hall(G) H -> H <| G -> K \subset G -> (K \subset H) = pi.-group K.

Lemma mem_normal_Hall : forall pi H G x,
  pi.-Hall(G) H -> H <| G -> x \in G -> (x \in H) = pi.-elt x.

Lemma uniq_normal_Hall : forall 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 : forall G H : {group gT},
  [max H | pi.-subgroup(G) H] -> H <| G -> pi.-Hall(G) H.

Lemma setI_normal_Hall : forall G H K : {group gT},
  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 Type pi : nat_pred.
Implicit Types G H P : {group aT}.

Lemma morphim_pgroup : forall pi G, pi.-group G -> pi.-group (f @* G).

Lemma morphim_odd : forall G, odd #|G| -> odd #|f @* G|.

Lemma pmorphim_pgroup : forall pi G,
   pi.-group ('ker f) -> G \subset D -> pi.-group (f @* G) = pi.-group G.

Lemma morphim_p_index : forall pi G H,
  H \subset D -> pi.-nat #|G : H| -> pi.-nat #|f @* G : f @* H|.

Lemma morphim_pHall : forall pi G H,
  H \subset D -> pi.-Hall(G) H -> pi.-Hall(f @* G) (f @* H).

Lemma pmorphim_pHall : forall 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 : forall G H,
   H \subset D -> Hall G H -> Hall (f @* G) (f @* H).

Lemma morphim_pSylow : forall p G P,
  P \subset D -> p.-Sylow(G) P -> p.-Sylow(f @* G) (f @* P).

Lemma morphim_p_group : forall P, p_group P -> p_group (f @* P).

Lemma morphim_Sylow : forall G P,
  P \subset D -> Sylow G P -> Sylow (f @* G) (f @* P).

Lemma morph_p_elt : forall pi x, x \in D -> pi.-elt x -> pi.-elt (f x).

Lemma morph_constt : forall 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 Structure 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) : subgroup_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 Structure 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 Structure pseries_group : {group gT} := group pseries_group_set.

End PseriesDefs.

Notation Local ConsPred := (@Cons nat_pred) (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) : subgroup_scope.

Section PCoreProps.

Variables (pi : nat_pred) (gT : finGroupType).
Implicit Type A : {set gT}.
Implicit Types G H M K : {group gT}.

Lemma pcore_psubgroup : forall G, pi.-subgroup(G) 'O_pi(G).

Lemma pcore_pgroup : forall G, pi.-group 'O_pi(G).

Lemma pcore_sub : forall G, 'O_pi(G) \subset G.

Lemma pcore_sub_Hall : forall G H, pi.-Hall(G) H -> 'O_pi(G) \subset H.

Lemma pcore_max : forall G H, pi.-group H -> H <| G -> H \subset 'O_pi(G).

Lemma pcore_pgroup_id : forall G, pi.-group G -> 'O_pi(G) = G.

Lemma pcore_normal : forall G, 'O_pi(G) <| G.

Lemma normal_Hall_pcore : forall H G, pi.-Hall(G) H -> H <| G -> 'O_pi(G) = H.

Lemma eq_Hall_pcore : forall G H,
  pi.-Hall(G) 'O_pi(G) -> pi.-Hall(G) H -> H :=: 'O_pi(G).

Lemma sub_Hall_pcore : forall G K,
  pi.-Hall(G) 'O_pi(G) -> K \subset G -> (K \subset 'O_pi(G)) = pi.-group K.

Lemma mem_Hall_pcore : forall G x,
  pi.-Hall(G) 'O_pi(G) -> x \in G -> (x \in 'O_pi(G)) = pi.-elt x.

Lemma sdprod_Hall_pcoreP : forall H G,
  pi.-Hall(G) 'O_pi(G) -> reflect ('O_pi(G) ><| H = G) (pi^'.-Hall(G) H).

Lemma sdprod_pcore_HallP : forall H G,
  pi^'.-Hall(G) H -> reflect ('O_pi(G) ><| H = G) (pi.-Hall(G) 'O_pi(G)).

Lemma pcoreJ : forall G x, 'O_pi(G :^ x) = 'O_pi(G) :^ x.

End PCoreProps.

Section MorphPcore.

Implicit Type pi : nat_pred.
Implicit Types gT rT : finGroupType.

Lemma morphim_pcore : forall pi, GFunctor.pcontinuous (pcore pi).

Lemma pcoreS : forall pi gT (G H : {group gT}),
  H \subset G -> H :&: 'O_pi(G) \subset 'O_pi(H).

Canonical Structure pcore_igFun pi :=
  [igFun by pcore_sub pi & morphim_pcore pi].
Canonical Structure pcore_gFun pi := [gFun by morphim_pcore pi].
Canonical Structure pcore_pgFun pi := [pgFun by morphim_pcore pi].

Lemma pcore_char : forall pi gT (G : {group gT}), 'O_pi(G) \char G.

Section PcoreMod.

Variable F : GFunctor.pmap.

Lemma pcore_mod_sub : forall pi gT (G : {group gT}),
  pcore_mod G pi (F _ G) \subset G.

Lemma quotient_pcore_mod : forall pi gT (G : {group gT}) (B : {set gT}),
  pcore_mod G pi B / B = 'O_pi(G / B).

Lemma morphim_pcore_mod : forall pi gT rT (D G : {group gT}),
  forall f : {morphism D >-> rT},
  f @* pcore_mod G pi (F _ G) \subset pcore_mod (f @* G) pi (F _ (f @* G)).

Lemma pcore_mod_res : forall pi gT rT (D : {group gT}),
  forall f : {morphism D >-> rT},
  f @* pcore_mod D pi (F _ D) \subset pcore_mod (f @* D) pi (F _ (f @* D)).

Lemma pcore_mod1 : forall pi gT (G : {group gT}), pcore_mod G pi 1 = 'O_pi(G).

End PcoreMod.

Lemma pseries_rcons : forall pi pis gT (A : {set gT}),
  pseries (rcons pis pi) A = pcore_mod A pi (pseries pis A).

Lemma pseries_subfun : forall pis,
   GFunctor.closed (pseries pis) /\ GFunctor.pcontinuous (pseries pis).

Lemma pseries_sub : forall pis, GFunctor.closed (pseries pis).

Lemma morphim_pseries : forall pis, GFunctor.pcontinuous (pseries pis).

Lemma pseriesS : forall pis, GFunctor.hereditary (pseries pis).

Canonical Structure pseries_igFun pis :=
  [igFun by pseries_sub pis & morphim_pseries pis].
Canonical Structure pseries_gFun pis := [gFun by morphim_pseries pis].
Canonical Structure pseries_pgFun pis := [pgFun by morphim_pseries pis].

Lemma pseries_char : forall pis gT (G : {group gT}), pseries pis G \char G.

Lemma pseries_normal : forall pis gT (G : {group gT}), pseries pis G <| G.

Lemma pseriesJ : forall pis gT (G : {group gT}) x,
  pseries pis (G :^ x) = pseries pis G :^ x.

Lemma pseries1 : forall pi gT (G : {group gT}), 'O_{pi}(G) = 'O_pi(G).

Lemma pseries_pop : forall pi pis gT (G : {group gT}),
  'O_pi(G) = 1 -> pseries (pi :: pis) G = pseries pis G.

Lemma pseries_pop2 : forall pi1 pi2 gT (G : {group gT}),
  'O_pi1(G) = 1 -> 'O_{pi1, pi2}(G) = 'O_pi2(G).

Lemma pseries_sub_catl : forall pi1s pi2s gT (G : {group gT}),
  pseries pi1s G \subset pseries (pi1s ++ pi2s) G.

Lemma quotient_pseries : forall pis pi gT (G : {group gT}),
  pseries (rcons pis pi) G / pseries pis G = 'O_pi(G / pseries pis G).

Lemma pseries_norm2 : forall pi1s pi2s gT (G : {group gT}),
  pseries pi2s G \subset 'N(pseries pi1s G).

Lemma pseries_sub_catr : forall pi1s pi2s gT (G : {group gT}),
  pseries pi2s G \subset pseries (pi1s ++ pi2s) G.

Lemma quotient_pseries2 : forall pi1 pi2 gT (G : {group gT}),
  'O_{pi1, pi2}(G) / 'O_pi1(G) = 'O_pi2(G / 'O_pi1(G)).

Lemma quotient_pseries_cat : forall pi1s pi2s gT (G : {group gT}),
  pseries (pi1s ++ pi2s) G / pseries pi1s G
    = pseries pi2s (G / pseries pi1s G).

Lemma pseries_catl_id : forall pi1s pi2s gT (G : {group gT}),
  pseries pi1s (pseries (pi1s ++ pi2s) G) = pseries pi1s G.

Lemma pseries_char_catl : forall pi1s pi2s gT (G : {group gT}),
  pseries pi1s G \char pseries (pi1s ++ pi2s) G.

Lemma pseries_catr_id : forall pi1s pi2s gT (G : {group gT}),
  pseries pi2s (pseries (pi1s ++ pi2s) G) = pseries pi2s G.

Lemma pseries_char_catr : forall pi1s pi2s gT (G : {group gT}),
  pseries pi2s G \char pseries (pi1s ++ pi2s) G.

Lemma pcore_modp : forall pi gT (G H : {group gT}),
  H <| G -> pi.-group H -> pcore_mod G pi H = 'O_pi(G).

Lemma pquotient_pcore : forall pi gT (G H : {group gT}),
  H <| G -> pi.-group H -> 'O_pi(G / H) = 'O_pi(G) / H.

Lemma trivg_pcore_quotient : forall pi gT (G : {group gT}),
  'O_pi(G / 'O_pi(G)) = 1.

Lemma pseries_rcons_id : forall 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.
Implicit Types G H : {group gT}.

Lemma sub_in_pcore : forall pi rho G,
  {in \pi(G), {subset pi <= rho}} -> 'O_pi(G) \subset 'O_rho(G).

Lemma sub_pcore : forall pi rho G,
  {subset pi <= rho} -> 'O_pi(G) \subset 'O_rho(G).

Lemma eq_in_pcore : forall pi rho G,
  {in \pi(G), pi =i rho} -> 'O_pi(G) = 'O_rho(G).

Lemma eq_pcore : forall pi rho G, pi =i rho -> 'O_pi(G) = 'O_rho(G).

Lemma pcoreNK : forall pi G, 'O_pi^'^'(G) = 'O_pi(G).

Lemma eq_p'core : forall pi rho G, pi =i rho -> 'O_pi^'(G) = 'O_rho^'(G).

Lemma sdprod_Hall_p'coreP : forall pi H G,
  pi^'.-Hall(G) 'O_pi^'(G) -> reflect ('O_pi^'(G) ><| H = G) (pi.-Hall(G) H).

Lemma sdprod_p'core_HallP : forall pi H G,
  pi.-Hall(G) H -> reflect ('O_pi^'(G) ><| H = G) (pi^'.-Hall(G) 'O_pi^'(G)).

Lemma pcoreI : forall pi rho G, 'O_[predI pi & rho](G) = 'O_pi('O_rho(G)).

Lemma bigcap_p'core : forall pi G,
  G :&: \bigcap_(p < #|G|.+1 | (p : nat) \in pi) 'O_p^'(G) = 'O_pi^'(G).

Lemma coprime_pcoreC : forall (rT : finGroupType) pi G (R : {group rT}),
  coprime #|'O_pi(G)| #|'O_pi^'(R)|.

Lemma TI_pcoreC : forall pi G H, 'O_pi(G) :&: 'O_pi^'(H) = 1.

Lemma pcore_setI_normal : forall 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}.
Implicit Types G H : {group aT}.

Lemma injm_pgroup : forall pi A,
  A \subset D -> pi.-group (f @* A) = pi.-group A.

Lemma injm_pelt : forall pi x, x \in D -> pi.-elt (f x) = pi.-elt x.

Lemma injm_pHall : forall pi G H,
  G \subset D -> H \subset D -> pi.-Hall(f @* G) (f @* H) = pi.-Hall(G) H.

Lemma injm_pcore : forall pi G, G \subset D -> f @* 'O_pi(G) = 'O_pi(f @* G).

Lemma injm_pseries : forall 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 : forall pi, G \isog H -> pi.-group G = pi.-group H.

Lemma isog_pcore : forall pi, G \isog H -> 'O_pi(G) \isog 'O_pi(H).

Lemma isog_pseries : forall pis, G \isog H -> pseries pis G \isog pseries pis H.

End Isog.