Library abelian

 Constructions based on abelian groups and their structure, with some       
 emphasis on elementary abelian p-groups.                                   
          'Ldiv_n() == the set of all x that satisfy x ^+ n = 1, or,        
                       equivalently the set of x whose order divides n.     
         'Ldiv_n(G) == the set of x in G that satisfy x ^+ n = 1.           
                    := G :&: 'Ldiv_n() (pure Notation)                      
         exponent G == the exponent of G: the least e such that x ^+ e = 1  
                       for all x in G (the LCM of the orders of x \in G).   
                       If G is nilpotent its exponent is reached. Note that 
                       `exponent G %| m' reads as `G has exponent m'.       
              'm(G) == the generator rank of G: the size of a smallest      
                       generating set for G (this is a basis for G if G     
                       abelian).                                            
     abelian_type G == the abelian type of G : if G is abelian, a lexico-   
                       graphically maximal sequence of the orders of the    
                       elements of a minimal basis of G (if G is a p-group  
                       this is the sequence of orders for any basis of G,   
                       sorted in decending order).                          
       homocyclic G == G is the direct product of cycles of equal order,    
                       i.e., G is abelian with constant abelian type.       
        p.-abelem G == G is an elementary abelian p-group, i.e., it is      
                       an abelian p-group of exponent p, and thus of order  
                       p ^ 'm(G) and rank (logn p #|G|).                    
        is_abelem G == G is an elementary abelian p-group for some prime p. 
            'E_p(G) == the set of elementary abelian p-subgroups of G.      
                    := [set E : {group _} | p.-abelem E && (E \subset G)]   
          'E_p^n(G) == the set of elementary abelian p-subgroups of G of    
                       order p ^ n (or, equivalently, of rank n).           
                    := [set E \in 'E_p(G) | logn p #|E| == n]               
                    := [set E \in 'E_p(G) | #|E| == p ^ n]%N if p is prime  
           'E*_p(G) == the set of maximal elementary abelian p-subgroups    
                       of G.                                                
                    := [set E | [max E | E \in 'E_p(G)]]                    
            'E^n(G) == the set of elementary abelian subgroups of G that    
                       have gerank n (i.e., p-rank n for some prime p).     
                    := \bigcup_(0 <= p < #|G|.+1) 'E_p^n(G)                 
            'r_p(G) == the p-rank of G: the maximal rank of an elementary   
                       subgroup of G.                                       
                    := \max_(E \in 'E_p(G)) logn p #|E|.                    
              'r(G) == the rank of G.                                       
                    := \max_(0 <= p < #|G|.+1) 'm_p(G).                     
 Note that 'r(G) coincides with 'r_p(G) if G is a p-group, and with 'm(G)   
 if G is abelian, but is much more useful than 'm(G) in the proof of the    
 Odd Order Theorem.                                                         
          'Ohm_n(G) == the group generated by the x in G with order p ^ m   
                       for some prime p and some m <= n. Usually, G will be 
                       a p-group, so 'Ohm_n(G) will be generated by         
                       'Ldiv_(p ^ n)(G), set of elements of G of order at   
                       most p ^ n. If G is also abelian then 'Ohm_n(G)      
                       consists exactly of those element, and the abelian   
                       type of G can be computed from the orders of the     
                       'Ohm_n(G) subgroups.                                 
          'Mho^n(G) == the group generated by the x ^+ (p ^ n) for x a      
                       p-element of G for some prime p. Usually G is a      
                       p-group, and 'Mho^n(G) is generated by all such      
                       x ^+ (p ^ n); it consists of exactly these if G is   
                       also abelian.                                        


Import GroupScope.

Section AbelianDefs.

 We defer the definition of the functors ('Omh_n(G), 'Mho^n(G)) because     
 they must 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 Ldiv n := [set x : gT | x ^+ n == 1].

Definition exponent A := \big[lcmn/1%N]_(x \in A) #[x].

Definition abelem p A := [&& p.-group A, abelian A & exponent A %| p].

Definition is_abelem A := abelem (pdiv #|A|) A.

Definition pElem p A := [set E : {group gT} | (E \subset A) && abelem p E].

Definition pnElem p n A := [set E \in pElem p A | logn p #|E| == n].

Definition nElem n A := \bigcup_(0 <= p < #|A|.+1) pnElem p n A.

Definition pmaxElem p A := [set E | [max E | E \in pElem p A]].

Definition p_rank p A := \max_(E \in pElem p A) logn p #|E|.

Definition rank A := \max_(0 <= p < #|A|.+1) p_rank p A.

Definition gen_rank A := #|[arg min_(B < A | <<B>> == A) #|B|]|.

 The definition of abelian_type depends on an existence lemma. 
 The definition of homocyclic depends on abelian_type. 

End AbelianDefs.

Notation "''Ldiv_' n ()" := (Ldiv _ n)
  (at level 8, n at level 2, format "''Ldiv_' n ()") : group_scope.

Notation "''Ldiv_' n ( G )" := (G :&: 'Ldiv_n())
  (at level 8, n at level 2, format "''Ldiv_' n ( G )") : group_scope.


Notation "p .-abelem" := (abelem p)
  (at level 2, format "p .-abelem") : group_scope.

Notation "''E_' p ( G )" := (pElem p G)
  (at level 8, p at level 2, format "''E_' p ( G )") : group_scope.

Notation "''E_' p ^ n ( G )" := (pnElem p n G)
  (at level 8, p, n at level 2, format "''E_' p ^ n ( G )") : group_scope.

Notation "''E' ^ n ( G )" := (nElem n G)
  (at level 8, n at level 2, format "''E' ^ n ( G )") : group_scope.

Notation "''E*_' p ( G )" := (pmaxElem p G)
  (at level 8, p at level 2, format "''E*_' p ( G )") : group_scope.

Notation "''m' ( A )" := (gen_rank A)
  (at level 8, format "''m' ( A )") : group_scope.

Notation "''r' ( A )" := (rank A)
  (at level 8, format "''r' ( A )") : group_scope.

Notation "''r_' p ( A )" := (p_rank p A)
  (at level 8, p at level 2, format "''r_' p ( A )") : group_scope.

Section Functors.

 A functor needs to quantify over the finGroupType just beore the set. 

Variables (n : nat) (gT : finGroupType) (A : {set gT}).

Definition Ohm := <<[set x \in A | x ^+ (pdiv #[x] ^ n) == 1]>>.

Definition Mho := <<[set x ^+ (pdiv #[x] ^ n) | x <- A, (pdiv #[x]).-elt x]>>.

Canonical Structure Ohm_group : {group gT} := Eval hnf in [group of Ohm].
Canonical Structure Mho_group : {group gT} := Eval hnf in [group of Mho].

Lemma pdiv_p_elt : forall (p : nat) (x : gT),
  p.-elt x -> x != 1 -> pdiv #[x] = p.

Lemma OhmPredP : forall x : gT,
  reflect (exists2 p, prime p & x ^+ (p ^ n) = 1) (x ^+ (pdiv #[x] ^ n) == 1).

Lemma Mho_p_elt : forall (p : nat) x,
  x \in A -> p.-elt x -> x ^+ (p ^ n) \in Mho.

End Functors.

Implicit Arguments OhmPredP [n gT x].

Notation "''Ohm_' n ( G )" := (Ohm n G)
  (at level 8, n at level 2, format "''Ohm_' n ( G )") : group_scope.
Notation "''Ohm_' n ( G )" := (Ohm_group n G) : subgroup_scope.

Notation "''Mho^' n ( G )" := (Mho n G)
  (at level 8, n at level 2, format "''Mho^' n ( G )") : group_scope.
Notation "''Mho^' n ( G )" := (Mho_group n G) : subgroup_scope.

Section ExponentAbelem.

Variable gT : finGroupType.
Implicit Types p n : nat.
Implicit Type pi : nat_pred.
Implicit Type x : gT.
Implicit Types A B C : {set gT}.
Implicit Types E G H K P X Y : {group gT}.

Lemma LdivP : forall A n x, reflect (x \in A /\ x ^+ n = 1) (x \in 'Ldiv_n(A)).

Lemma dvdn_exponent : forall x A, x \in A -> #[x] %| exponent A.

Lemma expg_exponent : forall x A, x \in A -> x ^+ exponent A = 1.

Lemma exponentS : forall A B, A \subset B -> exponent A %| exponent B.

Lemma exponentP : forall A n,
  reflect (forall x, x \in A -> x ^+ n = 1) (exponent A %| n).
Implicit Arguments exponentP [A n].

Lemma trivg_exponent : forall G, (G :==: 1) = (exponent G %| 1).

Lemma exponent1 : exponent [1 gT] = 1%N.

Lemma exponent_dvdn : forall G, exponent G %| #|G|.

Lemma exponent_gt0 : forall G, 0 < exponent G.
Hint Resolve exponent_gt0.

Lemma pnat_exponent : forall pi G, pi.-nat (exponent G) = pi.-group G.

Lemma exponentJ : forall A x, exponent (A :^ x) = exponent A.

Lemma exponent_witness : forall G,
  nilpotent G -> {x | x \in G & exponent G = #[x]}.

Lemma exponent_cycle : forall x, exponent <[x]> = #[x].

Lemma exponent_cyclic : forall X, cyclic X -> exponent X = #|X|.

Lemma primes_exponent : forall G, primes (exponent G) = primes (#|G|).

Lemma pi_of_exponent : forall G, \pi(exponent G) = \pi(G).

Lemma partn_exponentS : forall pi H G,
  H \subset G -> #|G|`_pi %| #|H| -> (exponent H)`_pi = (exponent G)`_pi.

Lemma exponent_Hall : forall pi G H,
  pi.-Hall(G) H -> exponent H = (exponent G)`_pi.

Lemma cprod_exponent : forall A B G,
  A \* B = G -> lcmn (exponent A) (exponent B) = (exponent G).

Lemma dprod_exponent : forall A B G,
  A \x B = G -> lcmn (exponent A) (exponent B) = (exponent G).

Lemma sub_LdivT : forall A n, (A \subset 'Ldiv_n()) = (exponent A %| n).

Lemma LdivT_J : forall n x, 'Ldiv_n() :^ x = 'Ldiv_n().

Lemma LdivJ : forall n A x, 'Ldiv_n(A :^ x) = 'Ldiv_n(A) :^ x.

Lemma sub_Ldiv : forall A n, (A \subset 'Ldiv_n(A)) = (exponent A %| n).

Lemma group_Ldiv : forall G n, abelian G -> group_set 'Ldiv_n(G).

Lemma abelian_exponent_gen : forall A, abelian A -> exponent <<A>> = exponent A.

Lemma abelem_pgroup : forall p A, p.-abelem A -> p.-group A.

Lemma abelem_abelian : forall p A, p.-abelem A -> abelian A.

Lemma abelem1 : forall p, p.-abelem [1 gT].

Lemma abelemE : forall p G,
  prime p -> p.-abelem G = abelian G && (exponent G %| p).

Lemma abelemP : forall p G, prime p ->
  reflect (abelian G /\ forall x, x \in G -> x ^+ p = 1) (p.-abelem G).

Lemma abelem_order_p : forall p G x,
  p.-abelem G -> x \in G -> x != 1 -> #[x] = p.

Lemma cyclic_abelem_prime : forall p X,
  p.-abelem X -> cyclic X -> X :!=: 1 -> #|X| = p.

Lemma cycle_abelem : forall p x,
  p.-elt x || prime p -> p.-abelem <[x]> = (#[x] %| p).

Lemma exponent2_abelem : forall G, exponent G %| 2 -> 2.-abelem G.

Lemma prime_abelem : forall p G, prime p -> #|G| = p -> p.-abelem G.

Lemma abelem_cyclic : forall p G,
  p.-abelem G -> cyclic G = (logn p #|G| <= 1).

Lemma abelemS : forall p H G, H \subset G -> p.-abelem G -> p.-abelem H.

Lemma abelemJ : forall p G x, p.-abelem (G :^ x) = p.-abelem G.

Lemma cprod_abelem : forall p A B G,
  A \* B = G -> p.-abelem G = p.-abelem A && p.-abelem B.

Lemma dprod_abelem : forall p A B G,
  A \x B = G -> p.-abelem G = p.-abelem A && p.-abelem B.

Lemma is_abelem_pgroup : forall p G, p.-group G -> is_abelem G = p.-abelem G.

Lemma is_abelemP : forall G,
  reflect (exists2 p, prime p & p.-abelem G) (is_abelem G).

Lemma pElemP : forall p A E,
  reflect (E \subset A /\ p.-abelem E) (E \in 'E_p(A)).
Implicit Arguments pElemP [p A E].

Lemma pElemS : forall p A B, A \subset B -> 'E_p(A) \subset 'E_p(B).

Lemma pElemI : forall p A B, 'E_p(A :&: B) = 'E_p(A) :&: subgroups B.

Lemma pElemJ : forall x p A E, ((E :^ x)%G \in 'E_p(A :^ x)) = (E \in 'E_p(A)).

Lemma pnElemP : forall p n A E,
  reflect [/\ E \subset A, p.-abelem E & logn p #|E| = n] (E \in 'E_p^n(A)).
Implicit Arguments pnElemP [p n A E].

Lemma pnElemPcard : forall p n A E,
  E \in 'E_p^n(A) -> [/\ E \subset A, p.-abelem E & #|E| = p ^ n]%N.

Lemma card_pnElem : forall p n A E, E \in 'E_p^n(A) -> #|E| = (p ^ n)%N.

Lemma pnElem0 : forall p G, 'E_p^0(G) = [set 1%G].

Lemma pnElem_prime : forall p n A E, E \in 'E_p^n.+1(A) -> prime p.

Lemma pnElemE : forall p n A,
  prime p -> 'E_p^n(A) = [set E \in 'E_p(A) | #|E| == (p ^ n)%N].

Lemma pnElemS : forall p n A B, A \subset B -> 'E_p^n(A) \subset 'E_p^n(B).

Lemma pnElemI : forall p n A B, 'E_p^n(A :&: B) = 'E_p^n(A) :&: subgroups B.

Lemma pnElemJ : forall x p n A E,
  ((E :^ x)%G \in 'E_p^n(A :^ x)) = (E \in 'E_p^n(A)).

Lemma abelem_pnElem : forall p n G,
  p.-abelem G -> n <= logn p #|G| -> exists E, E \in 'E_p^n(G).

Lemma card_p1Elem : forall p A X, X \in 'E_p^1(A) -> #|X| = p.

Lemma p1ElemE : forall p A,
  prime p -> 'E_p^1(A) = [set X \in subgroups A | #|X| == p].

Lemma TIp1ElemP : forall p A X Y,
  X \in 'E_p^1(A) -> Y \in 'E_p^1(A) -> reflect (X :&: Y = 1) (X :!=: Y).

Lemma card_p1Elem_pnElem : forall p n A E,
  E \in 'E_p^n(A) -> #|'E_p^1(E)| = (\sum_(i < n) p ^ i)%N.

Lemma card_p1Elem_p2Elem : forall p A E, E \in 'E_p^2(A) -> #|'E_p^1(E)| = p.+1.

Lemma p2Elem_dprodP : forall p A E X Y,
    E \in 'E_p^2(A) -> X \in 'E_p^1(E) -> Y \in 'E_p^1(E) ->
  reflect (X \x Y = E) (X :!=: Y).

Lemma nElemP : forall n G E,
  reflect (exists p, E \in 'E_p^n(G)) (E \in 'E^n(G)).
Implicit Arguments nElemP [n G E].

Lemma nElem0 : forall G, 'E^0(G) = [set 1%G].

Lemma nElem1P : forall G E,
  reflect (E \subset G /\ exists2 p, prime p & #|E| = p) (E \in 'E^1(G)).

Lemma nElemS : forall n G H, G \subset H -> 'E^n(G) \subset 'E^n(H).

Lemma nElemI : forall n G H, 'E^n(G :&: H) = 'E^n(G) :&: subgroups H.

Lemma def_pnElem : forall p n G, 'E_p^n(G) = 'E_p(G) :&: 'E^n(G).

Lemma pmaxElemP : forall p A E,
  reflect (E \in 'E_p(A) /\ forall H, H \in 'E_p(A) -> E \subset H -> H :=: E)
          (E \in 'E*_p(A)).

Lemma pmaxElem_exists : forall p A D,
  D \in 'E_p(A) -> {E | E \in 'E*_p(A) & D \subset E}.

Lemma pmaxElem_LdivP : forall p G E,
  prime p -> reflect ('Ldiv_p('C_G(E)) = E) (E \in 'E*_p(G)).

Lemma pmaxElemS : forall p A B,
  A \subset B -> 'E*_p(B) :&: subgroups A \subset 'E*_p(A).

Lemma pmaxElemJ : forall p A E x,
  ((E :^ x)%G \in 'E*_p(A :^ x)) = (E \in 'E*_p(A)).

Lemma grank_min : forall B, 'm(<<B>>) <= #|B|.

Lemma grank_witness : forall G, {B | <<B>> = G & #|B| = 'm(G)}.

Lemma p_rank_witness : forall p G, {E | E \in 'E_p^('r_p(G))(G)}.

Lemma p_rank_geP : forall p n G,
  reflect (exists E, E \in 'E_p^n(G)) (n <= 'r_p(G)).

Lemma p_rank_gt0 : forall p H, ('r_p(H) > 0) = (p \in \pi(H)).

Lemma p_rank1 : forall p, 'r_p([1 gT]) = 0.

Lemma logn_le_p_rank : forall p A E, E \in 'E_p(A) -> logn p #|E| <= 'r_p(A).

Lemma p_rank_le_logn : forall p G, 'r_p(G) <= logn p #|G|.

Lemma p_rank_abelem : forall p G, p.-abelem G -> 'r_p(G) = logn p #|G|.

Lemma p_rankS : forall p A B, A \subset B -> 'r_p(A) <= 'r_p(B).

Lemma p_rankElem_max : forall p A, 'E_p^('r_p(A))(A) \subset 'E*_p(A).

Lemma p_rankJ : forall p A x, 'r_p(A :^ x) = 'r_p(A).

Lemma p_rank_Sylow : forall p G H, p.-Sylow(G) H -> 'r_p(H) = 'r_p(G).

Lemma p_rank_Hall : forall pi p G H,
  pi.-Hall(G) H -> p \in pi -> 'r_p(H) = 'r_p(G).

Lemma p_rank_pmaxElem_exists : forall p r G,
   'r_p(G) >= r -> exists2 E, E \in 'E*_p(G) & 'r_p(E) >= r.

Lemma rank1 : 'r([1 gT]) = 0.

Lemma p_rank_le_rank : forall p G, 'r_p(G) <= 'r(G).

Lemma rank_gt0 : forall G, ('r(G) > 0) = (G :!=: 1).

Lemma rank_witness : forall G, {p | prime p & 'r(G) = 'r_p(G)}.

Lemma rank_pgroup : forall p G, p.-group G -> 'r(G) = 'r_p(G).

Lemma rank_Sylow : forall p G P, p.-Sylow(G) P -> 'r(P) = 'r_p(G).

Lemma rank_abelem : forall p G, p.-abelem G -> 'r(G) = logn p #|G|.

Lemma nt_pnElem : forall p n E A, E \in 'E_p^n(A) -> n > 0 -> E :!=: 1.

Lemma rankJ : forall A x, 'r(A :^ x) = 'r(A).

Lemma rankS : forall A B, A \subset B -> 'r(A) <= 'r(B).

Lemma rank_geP : forall n G, reflect (exists E, E \in 'E^n(G)) (n <= 'r(G)).

End ExponentAbelem.

Implicit Arguments LdivP [gT A n x].
Implicit Arguments exponentP [gT A n].
Implicit Arguments abelemP [gT p G].
Implicit Arguments is_abelemP [gT G].
Implicit Arguments pElemP [gT p A E].
Implicit Arguments pnElemP [gT p n A E].
Implicit Arguments nElemP [gT n G E].
Implicit Arguments nElem1P [gT G E].
Implicit Arguments pmaxElemP [gT p A E].
Implicit Arguments pmaxElem_LdivP [gT p G E].
Implicit Arguments p_rank_geP [gT p n G].
Implicit Arguments rank_geP [gT n G].

Section MorphAbelem.

Variables (aT rT : finGroupType) (D : {group aT}) (f : {morphism D >-> rT}).
Implicit Types G H E : {group aT}.
Implicit Types A B : {set aT}.

Lemma exponent_morphim : forall G, exponent (f @* G) %| exponent G.

Lemma morphim_LdivT : forall n, f @* 'Ldiv_n() \subset 'Ldiv_n().

Lemma morphim_Ldiv : forall n A, f @* 'Ldiv_n(A) \subset 'Ldiv_n(f @* A).

Lemma morphim_abelem : forall p G, p.-abelem G -> p.-abelem (f @* G).

Lemma morphim_pElem : forall p G E,
  E \in 'E_p(G) -> (f @* E)%G \in 'E_p(f @* G).

Lemma morphim_pnElem : forall p n G E,
  E \in 'E_p^n(G) -> {m | m <= n & (f @* E)%G \in 'E_p^m(f @* G)}.

Lemma morphim_grank : forall G, G \subset D -> 'm(f @* G) <= 'm(G).

 There are no general morphism relations for the p-rank. We later prove     
 some relations for the p-rank of a quotient in the QuotientAbelem section. 

End MorphAbelem.

Section InjmAbelem.

Variables (aT rT : finGroupType) (D G : {group aT}) (f : {morphism D >-> rT}).
Hypotheses (injf : 'injm f) (sGD : G \subset D).
Let defG : invm injf @* (f @* G) = G := morphim_invm injf sGD.

Lemma exponent_injm : exponent (f @* G) = exponent G.

Lemma injm_Ldiv : forall n A, f @* 'Ldiv_n(A) = 'Ldiv_n(f @* A).

Lemma injm_abelem : forall p, p.-abelem (f @* G) = p.-abelem G.

Lemma injm_pElem : forall p (E : {group aT}),
  E \subset D -> ((f @* E)%G \in 'E_p(f @* G)) = (E \in 'E_p(G)).

Lemma injm_pnElem : forall p n (E : {group aT}),
  E \subset D -> ((f @* E)%G \in 'E_p^n(f @* G)) = (E \in 'E_p^n(G)).

Lemma injm_nElem : forall n (E : {group aT}),
  E \subset D -> ((f @* E)%G \in 'E^n(f @* G)) = (E \in 'E^n(G)).

Lemma injm_pmaxElem : forall p (E : {group aT}),
  E \subset D -> ((f @* E)%G \in 'E*_p(f @* G)) = (E \in 'E*_p(G)).

Lemma injm_grank : 'm(f @* G) = 'm(G).

Lemma injm_p_rank : forall p, 'r_p(f @* G) = 'r_p(G).

Lemma injm_rank : 'r(f @* G) = 'r(G).

End InjmAbelem.

Section IsogAbelem.

Variables (aT rT : finGroupType) (G : {group aT}) (H : {group rT}).
Hypothesis isoGH : G \isog H.

Lemma exponent_isog : exponent G = exponent H.

Lemma isog_abelem : forall p, p.-abelem G = p.-abelem H.

Lemma isog_grank : 'm(G) = 'm(H).

Lemma isog_p_rank : forall p, 'r_p(G) = 'r_p(H).

Lemma isog_rank : 'r(G) = 'r(H).

End IsogAbelem.

Section QuotientAbelem.

Variables (gT : finGroupType) (p : nat).
Implicit Types E G K H : {group gT}.

Lemma exponent_quotient : forall G H, exponent (G / H) %| exponent G.

Lemma quotient_LdivT : forall n H, 'Ldiv_n() / H \subset 'Ldiv_n().

Lemma quotient_Ldiv : forall n A H, 'Ldiv_n(A) / H \subset 'Ldiv_n(A / H).

Lemma quotient_abelem : forall G H, p.-abelem G -> p.-abelem (G / H).

Lemma quotient_pElem : forall G H E, E \in 'E_p(G) -> (E / H)%G \in 'E_p(G / H).

Lemma logn_quotient : forall G H, logn p #|G / H| <= logn p #|G|.

Lemma logn_quotient_pnElem : forall G H n E,
  E \in 'E_p^n(G) -> {m | m <= n & (E / H)%G \in 'E_p^m(G / H)}.

Lemma quotient_grank : forall G H, G \subset 'N(H) -> 'm(G / H) <= 'm(G).

Lemma p_rank_quotient : forall G H,
  G \subset 'N(H) -> 'r_p(G) - 'r_p(H) <= 'r_p(G / H).

Lemma p_rank_dprod : forall K H G, K \x H = G -> 'r_p(K) + 'r_p(H) = 'r_p(G).

Lemma p_rank_p'quotient : forall G H,
  (p : nat)^'.-group H -> G \subset 'N(H) -> 'r_p(G / H) = 'r_p(G).

End QuotientAbelem.

Section OhmProps.

Section Generic.

Variables (n : nat) (gT : finGroupType).
Implicit Type p : nat.
Implicit Type x : gT.
Implicit Type rT : finGroupType.
Implicit Types A B : {set gT}.
Implicit Types D G H : {group gT}.

Lemma Ohm_sub : forall G, 'Ohm_n(G) \subset G.

Lemma Ohm1 : 'Ohm_n([1 gT]) = 1.

Lemma Ohm_id : forall G, 'Ohm_n('Ohm_n(G)) = 'Ohm_n(G).

Lemma Ohm_cont : forall rT G (f : {morphism G >-> rT}),
  f @* 'Ohm_n(G) \subset 'Ohm_n(f @* G).

Lemma OhmS : forall H G, H \subset G -> 'Ohm_n(H) \subset 'Ohm_n(G).

Lemma OhmE : forall p G, p.-group G -> 'Ohm_n(G) = <<'Ldiv_(p ^ n)(G)>>.

Lemma OhmEabelian : forall p G, p.-group G -> abelian 'Ohm_n(G) ->
  'Ohm_n(G) = 'Ldiv_(p ^ n)(G).

Lemma Ohm_p_cycle : forall p x,
  p.-elt x -> 'Ohm_n(<[x]>) = <[x ^+ (p ^ (logn p #[x] - n))]>.

Lemma Ohm_dprod : forall A B G,
  A \x B = G -> 'Ohm_n(A) \x 'Ohm_n(B) = 'Ohm_n(G).

Lemma Mho_sub : forall G, 'Mho^n(G) \subset G.

Lemma Mho1 : 'Mho^n([1 gT]) = 1.

Lemma morphim_Mho : forall rT D G (f : {morphism D >-> rT}),
  G \subset D -> f @* 'Mho^n(G) = 'Mho^n(f @* G).

Lemma Mho_cont : forall rT G (f : {morphism G >-> rT}),
  f @* 'Mho^n(G) \subset 'Mho^n(f @* G).

Lemma MhoS : forall H G, H \subset G -> 'Mho^n(H) \subset 'Mho^n(G).

Lemma MhoE : forall p G,
  p.-group G -> 'Mho^n(G) = <<[set x ^+ (p ^ n) | x <- G]>>.

Lemma MhoEabelian : forall p G,
  p.-group G -> abelian G -> 'Mho^n(G) = [set x ^+ (p ^ n) | x <- G].

Lemma trivg_Mho : forall G, 'Mho^n(G) == 1 -> 'Ohm_n(G) == G.

Lemma Mho_p_cycle : forall p x, p.-elt x -> 'Mho^n(<[x]>) = <[x ^+ (p ^ n)]>.

Lemma Mho_cprod : forall A B G,
  A \* B = G -> 'Mho^n(A) \* 'Mho^n(B) = 'Mho^n(G).

Lemma Mho_dprod : forall A B G,
  A \x B = G -> 'Mho^n(A) \x 'Mho^n(B) = 'Mho^n(G).

End Generic.

Canonical Structure Ohm_igFun i := [igFun by Ohm_sub i & Ohm_cont i].
Canonical Structure Ohm_gFun i := [gFun by Ohm_cont i].
Canonical Structure Ohm_mgFun i := [mgFun by OhmS i].

Canonical Structure Mho_igFun i := [igFun by Mho_sub i & Mho_cont i].
Canonical Structure Mho_gFun i := [gFun by Mho_cont i].
Canonical Structure Mho_mgFun i := [mgFun by MhoS i].

Section char.

Variables (n : nat) (gT rT : finGroupType) (D G : {group gT}).

Lemma Ohm_char : 'Ohm_n(G) \char G.

Lemma Ohm_normal : 'Ohm_n(G) <| G.

Lemma Mho_char : 'Mho^n(G) \char G.

Lemma Mho_normal : 'Mho^n(G) <| G.

Lemma morphim_Ohm : forall f : {morphism D >-> rT},
  G \subset D -> f @* 'Ohm_n(G) \subset 'Ohm_n(f @* G).

Lemma injm_Ohm : forall f : {morphism D >-> rT},
  'injm f -> G \subset D -> f @* 'Ohm_n(G) = 'Ohm_n(f @* G).

Lemma isog_Ohm : forall H : {group rT}, G \isog H -> 'Ohm_n(G) \isog 'Ohm_n(H).

Lemma isog_Mho : forall H : {group rT}, G \isog H -> 'Mho^n(G) \isog 'Mho^n(H).

End char.

Variable gT : finGroupType.

Implicit Types A B C : {set gT}.
Implicit Types D G H E : {group gT}.
Implicit Type pi : nat_pred.
Implicit Type p : nat.

Lemma Ohm0 : forall G, 'Ohm_0(G) = 1.

Lemma Ohm_leq : forall m n G, m <= n -> 'Ohm_m(G) \subset 'Ohm_n(G).

Lemma OhmJ : forall n G x, 'Ohm_n(G :^ x) = 'Ohm_n(G) :^ x.

Lemma Mho0 : forall G, 'Mho^0(G) = G.

Lemma Mho_leq : forall m n G, m <= n -> 'Mho^n(G) \subset 'Mho^m(G).

Lemma MhoJ : forall n G x, 'Mho^n(G :^ x) = 'Mho^n(G) :^ x.

Lemma extend_cyclic_Mho : forall G p x,
    p.-group G -> x \in G -> 'Mho^1(G) = <[x ^+ p]> ->
  forall k, k > 0 -> 'Mho^k(G) = <[x ^+ (p ^ k)]>.

Lemma Ohm1Eprime : forall G, 'Ohm_1(G) = <<[set x \in G | prime #[x]]>>.

Lemma abelem_Ohm1 : forall p G,
  p.-group G -> p.-abelem 'Ohm_1(G) = abelian 'Ohm_1(G).

Lemma Ohm1_abelem : forall p G,
  p.-group G -> abelian G -> p.-abelem ('Ohm_1(G)).

Lemma Ohm1_id : forall p G, p.-abelem G -> 'Ohm_1(G) = G.

Lemma abelem_Ohm1P : forall p G,
  abelian G -> p.-group G -> reflect ('Ohm_1(G) = G) (p.-abelem G).

Lemma TI_Ohm1 : forall G H, H :&: 'Ohm_1(G) = 1 -> H :&: G = 1.

Lemma Ohm1_eq1 : forall G, ('Ohm_1(G) == 1) = (G :==: 1).

Lemma meet_Ohm1 : forall G H, G :&: H != 1 -> G :&: 'Ohm_1(H) != 1.

Lemma Ohm1_cent_max : forall G E p,
  E \in 'E*_p(G) -> p.-group G -> 'Ohm_1('C_G(E)) = E.

Lemma Ohm1_cyclic_pgroup_prime : forall p G,
  cyclic G -> p.-group G -> G :!=: 1 -> #|'Ohm_1(G)| = p.

Lemma cyclic_pgroup_dprod_trivg : forall p A B C,
    p.-group C -> cyclic C -> A \x B = C ->
  A = 1 /\ B = C \/ B = 1 /\ A = C.

Lemma piOhm1 : forall G, \pi('Ohm_1(G)) = \pi(G).

Lemma Ohm1Eexponent : forall p G,
  prime p -> exponent 'Ohm_1(G) %| p -> 'Ohm_1(G) = 'Ldiv_p(G).

Lemma p_rank_Ohm1 : forall p G, 'r_p('Ohm_1(G)) = 'r_p(G).

Lemma rank_Ohm1 : forall G, 'r('Ohm_1(G)) = 'r(G).

Lemma p_rank_abelian : forall p G, abelian G -> 'r_p(G) = logn p #|'Ohm_1(G)|.

Lemma rank_abelian_pgroup : forall p G,
  p.-group G -> abelian G -> 'r(G) = logn p #|'Ohm_1(G)|.

End OhmProps.

Section AbelianStructure.

Variable gT : finGroupType.
Implicit Type p : nat.
Implicit Type G H E : {group gT}.

Lemma abelian_splits : forall x G,
  x \in G -> #[x] = exponent G -> abelian G -> [splits G, over <[x]>].

Lemma abelem_splits : forall p G H,
  p.-abelem G -> H \subset G -> [splits G, over H].

Lemma abelian_type_subproof : forall G,
  {H : {group gT} & abelian G -> {x | #[x] = exponent G & <[x]> \x H = G}}.

Fixpoint abelian_type_rec n G :=
  if n is n'.+1 then if abelian G && (G :!=: 1) then
    exponent G :: abelian_type_rec n' (tag (abelian_type_subproof G))
  else [::] else [::].

Definition abelian_type (A : {set gT}) := abelian_type_rec #|A| <<A>>.

Lemma abelian_type_dvdn_sorted : forall A,
  sorted [rel m n | n %| m] (abelian_type A).

Lemma abelian_type_gt1 : forall A, all [pred m | m > 1] (abelian_type A).

Lemma abelian_type_sorted : forall A, sorted geq (abelian_type A).

Theorem abelian_structure : forall G, abelian G ->
  {b | \big[dprod/1]_(x <- b) <[x]> = G & map order b = abelian_type G}.

Lemma count_logn_dprod_cycle : forall p n b G,
    \big[dprod/1]_(x <- b) <[x]> = G ->
  count [pred x | logn p #[x] > n] b = logn p #|'Ohm_n.+1(G) : 'Ohm_n(G)|.

Lemma perm_eq_abelian_type : forall p b G,
    p.-group G -> \big[dprod/1]_(x <- b) <[x]> = G -> 1 \notin b ->
  perm_eq (map order b) (abelian_type G).

Lemma size_abelian_type : forall G, abelian G -> size (abelian_type G) = 'r(G).

Lemma mul_card_Ohm_Mho_abelian : forall n G,
  abelian G -> (#|'Ohm_n(G)| * #|'Mho^n(G)|)%N = #|G|.

Lemma grank_abelian : forall G, abelian G -> 'm(G) = 'r(G).

Lemma rank_cycle : forall x : gT, 'r(<[x]>) = (x != 1).

Lemma abelian_rank1_cyclic : forall G, abelian G -> cyclic G = ('r(G) <= 1).

Definition homocyclic A := abelian A && constant (abelian_type A).

Lemma homocyclic_Ohm_Mho : forall n p G,
  p.-group G -> homocyclic G -> 'Ohm_n(G) = 'Mho^(logn p (exponent G) - n)(G).

Lemma Ohm_Mho_homocyclic : forall (n p : nat) G,
    abelian G -> p.-group G -> 0 < n < logn p (exponent G) ->
  'Ohm_n(G) = 'Mho^(logn p (exponent G) - n)(G) -> homocyclic G.

Lemma abelem_homocyclic : forall p G, p.-abelem G -> homocyclic G.

Lemma Ohm1_homocyclicP : forall p G, p.-group G -> abelian G ->
  reflect ('Ohm_1(G) = 'Mho^(logn p (exponent G)).-1(G)) (homocyclic G).

Lemma abelian_type_homocyclic : forall G,
  homocyclic G -> abelian_type G = nseq 'r(G) (exponent G).

Lemma abelian_type_abelem : forall p G,
  p.-abelem G -> abelian_type G = nseq 'r(G) p.

End AbelianStructure.

Section IsogAbelian.

Variables aT rT : finGroupType.
Implicit Type gT : finGroupType.
Implicit Types D G : {group aT}.
Implicit Types H : {group rT}.

Lemma isog_abelian_type : forall G H,
  isog G H -> abelian_type G = abelian_type H.

Lemma eq_abelian_type_isog : forall G H,
  abelian G -> abelian H -> isog G H = (abelian_type G == abelian_type H).

Lemma isog_abelem_card : forall p G H,
  p.-abelem G -> isog G H = p.-abelem H && (#|H| == #|G|).

Variables (D : {group aT}) (f : {morphism D >-> rT}).

Lemma morphim_rank_abelian : forall G,
  abelian G -> 'r(f @* G) <= 'r(G).

Lemma morphim_p_rank_abelian : forall p G,
  abelian G -> 'r_p(f @* G) <= 'r_p(G).

End IsogAbelian.

Section QuotientRank.

Variables (gT : finGroupType) (p : nat) (G H : {group gT}).
Hypothesis cGG : abelian G.

Lemma quotient_rank_abelian : 'r(G / H) <= 'r(G).

Lemma quotient_p_rank_abelian : 'r_p(G / H) <= 'r_p(G).

End QuotientRank.