(Joint Center)Library MathComp.abelian

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div fintype.
Require Import finfun bigop finset prime binomial fingroup morphism perm.
Require Import automorphism action quotient gfunctor gproduct zmodp cyclic.
Require Import pgroup gseries nilpotent sylow.

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.

Set Implicit Arguments.

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 Types (x : gT) (A B : {set gT}) (pi : nat_pred) (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 in A & (pdiv #[x]).-elt x]>>.

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

Lemma pdiv_p_elt (p : nat) (x : gT) : p.-elt xx != 1 → pdiv #[x] = p.

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

Lemma Mho_p_elt (p : nat) x : x \in Ap.-elt xx ^+ (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) : Group_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) : Group_scope.

Section ExponentAbelem.

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

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

Lemma dvdn_exponent x A : x \in A#[x] %| exponent A.

Lemma expg_exponent x A : x \in Ax ^+ exponent A = 1.

Lemma exponentS A B : A \subset Bexponent A %| exponent B.

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

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

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

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

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

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

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

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

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

Lemma exponent_cyclic X : cyclic Xexponent X = #|X|.

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

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

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

Lemma exponent_Hall pi G H : pi.-Hall(G) Hexponent H = (exponent G)`_pi.

Lemma exponent_Zgroup G : Zgroup Gexponent G = #|G|.

Lemma cprod_exponent A B G :
  A \* B = Glcmn (exponent A) (exponent B) = (exponent G).

Lemma dprod_exponent A B G :
  A \x B = Glcmn (exponent A) (exponent B) = (exponent G).

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

Lemma LdivT_J n x : 'Ldiv_n :^ x = 'Ldiv_n.

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

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

Lemma group_Ldiv G n : abelian Ggroup_set 'Ldiv_n(G).

Lemma abelian_exponent_gen A : abelian Aexponent <<A>> = exponent A.

Lemma abelem_pgroup p A : p.-abelem Ap.-group A.

Lemma abelem_abelian p A : p.-abelem Aabelian A.

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

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

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

Lemma abelem_order_p p G x : p.-abelem Gx \in Gx != 1 → #[x] = p.

Lemma cyclic_abelem_prime p X : p.-abelem Xcyclic XX :!=: 1 → #|X| = p.

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

Lemma exponent2_abelem G : exponent G %| 2 → 2.-abelem G.

Lemma prime_abelem p G : prime p#|G| = pp.-abelem G.

Lemma abelem_cyclic p G : p.-abelem Gcyclic G = (logn p #|G| 1).

Lemma abelemS p H G : H \subset Gp.-abelem Gp.-abelem H.

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

Lemma cprod_abelem p A B G :
  A \* B = Gp.-abelem G = p.-abelem A && p.-abelem B.

Lemma dprod_abelem p A B G :
  A \x B = Gp.-abelem G = p.-abelem A && p.-abelem B.

Lemma is_abelem_pgroup p G : p.-group Gis_abelem G = p.-abelem G.

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

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

Lemma pElemS p A B : A \subset B'E_p(A) \subset 'E_p(B).

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

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

Lemma pnElemP 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 p n A E :
  E \in 'E_p^n(A)[/\ E \subset A, p.-abelem E & #|E| = p ^ n]%N.

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

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

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

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

Lemma pnElemS p n A B : A \subset B'E_p^n(A) \subset 'E_p^n(B).

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

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

Lemma abelem_pnElem p n G :
  p.-abelem Gn logn p #|G| E, E \in 'E_p^n(G).

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

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

Lemma TIp1ElemP 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 p n A E :
  E \in 'E_p^n(A)#|'E_p^1(E)| = (\sum_(i < n) p ^ i)%N.

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

Lemma p2Elem_dprodP 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 n G E : reflect ( p, E \in 'E_p^n(G)) (E \in 'E^n(G)).
Implicit Arguments nElemP [n G E].

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

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

Lemma nElemS n G H : G \subset H'E^n(G) \subset 'E^n(H).

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

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

Lemma pmaxElemP p A E :
  reflect (E \in 'E_p(A) H, H \in 'E_p(A)E \subset HH :=: E)
          (E \in 'E×_p(A)).

Lemma pmaxElem_exists p A D :
  D \in 'E_p(A){E | E \in 'E×_p(A) & D \subset E}.

Lemma pmaxElem_LdivP p G E :
  prime preflect ('Ldiv_p('C_G(E)) = E) (E \in 'E×_p(G)).

Lemma pmaxElemS p A B :
  A \subset B'E×_p(B) :&: subgroups A \subset 'E×_p(A).

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

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

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

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

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

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

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

Lemma logn_le_p_rank p A E : E \in 'E_p(A)logn p #|E| 'r_p(A).

Lemma p_rank_le_logn p G : 'r_p(G) logn p #|G|.

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

Lemma p_rankS p A B : A \subset B'r_p(A) 'r_p(B).

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

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

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

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

Lemma p_rank_pmaxElem_exists p r G :
  'r_p(G) rexists2 E, E \in 'E×_p(G) & 'r_p(E) r.

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

Lemma p_rank_le_rank p G : 'r_p(G) 'r(G).

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

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

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

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

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

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

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

Lemma rankS A B : A \subset B'r(A) 'r(B).

Lemma rank_geP n G : reflect ( 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}) (A B : {set aT}).

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

Lemma morphim_LdivT n : f @* 'Ldiv_n \subset 'Ldiv_n.

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

Lemma morphim_abelem p G : p.-abelem Gp.-abelem (f @* G).

Lemma morphim_pElem p G E : E \in 'E_p(G) → (f @* E)%G \in 'E_p(f @* G).

Lemma morphim_pnElem 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 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 n A : f @* 'Ldiv_n(A) = 'Ldiv_n(f @* A).

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

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

Lemma injm_pnElem 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 n (E : {group aT}) :
  E \subset D((f @* E)%G \in 'E^n(f @* G)) = (E \in 'E^n(G)).

Lemma injm_pmaxElem 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 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 p : p.-abelem G = p.-abelem H.

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

Lemma isog_p_rank 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 G H : exponent (G / H) %| exponent G.

Lemma quotient_LdivT n H : 'Ldiv_n / H \subset 'Ldiv_n.

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

Lemma quotient_abelem G H : p.-abelem Gp.-abelem (G / H).

Lemma quotient_pElem G H E : E \in 'E_p(G) → (E / H)%G \in 'E_p(G / H).

Lemma logn_quotient G H : logn p #|G / H| logn p #|G|.

Lemma quotient_pnElem 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 G H : G \subset 'N(H)'m(G / H) 'm(G).

Lemma p_rank_quotient G H : G \subset 'N(H)'r_p(G) - 'r_p(H) 'r_p(G / H).

Lemma p_rank_dprod K H G : K \x H = G'r_p(K) + 'r_p(H) = 'r_p(G).

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

End QuotientAbelem.

Section OhmProps.

Section Generic.

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

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

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

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

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

Lemma OhmS H G : H \subset G'Ohm_n(H) \subset 'Ohm_n(G).

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

Lemma OhmEabelian p G :
  p.-group Gabelian 'Ohm_n(G)'Ohm_n(G) = 'Ldiv_(p ^ n)(G).

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

Lemma Ohm_dprod A B G : A \x B = G'Ohm_n(A) \x 'Ohm_n(B) = 'Ohm_n(G).

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

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

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

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

Lemma MhoS H G : H \subset G'Mho^n(H) \subset 'Mho^n(G).

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

Lemma MhoEabelian p G :
  p.-group Gabelian G'Mho^n(G) = [set x ^+ (p ^ n) | x in G].

Lemma trivg_Mho G : 'Mho^n(G) == 1 → 'Ohm_n(G) == G.

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

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

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

End Generic.

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

Canonical Mho_igFun i := [igFun by Mho_sub i & Mho_cont i].
Canonical Mho_gFun i := [gFun by Mho_cont i].
Canonical 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 (f : {morphism D >-> rT}) :
  G \subset Df @* 'Ohm_n(G) \subset 'Ohm_n(f @* G).

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

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

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

End char.

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

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

Lemma Ohm_leq m n G : m n'Ohm_m(G) \subset 'Ohm_n(G).

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

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

Lemma Mho_leq m n G : m n'Mho^n(G) \subset 'Mho^m(G).

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

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

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

Lemma abelem_Ohm1 p G : p.-group Gp.-abelem 'Ohm_1(G) = abelian 'Ohm_1(G).

Lemma Ohm1_abelem p G : p.-group Gabelian Gp.-abelem ('Ohm_1(G)).

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

Lemma abelem_Ohm1P p G :
  abelian Gp.-group Greflect ('Ohm_1(G) = G) (p.-abelem G).

Lemma TI_Ohm1 G H : H :&: 'Ohm_1(G) = 1 → H :&: G = 1.

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

Lemma meet_Ohm1 G H : G :&: H != 1 → G :&: 'Ohm_1(H) != 1.

Lemma Ohm1_cent_max G E p : E \in 'E×_p(G)p.-group G'Ohm_1('C_G(E)) = E.

Lemma Ohm1_cyclic_pgroup_prime p G :
  cyclic Gp.-group GG :!=: 1 → #|'Ohm_1(G)| = p.

Lemma cyclic_pgroup_dprod_trivg p A B C :
    p.-group Ccyclic CA \x B = C
  A = 1 B = C B = 1 A = C.

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

Lemma Ohm1Eexponent p G :
  prime pexponent 'Ohm_1(G) %| p'Ohm_1(G) = 'Ldiv_p(G).

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

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

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

Lemma rank_abelian_pgroup p G :
  p.-group Gabelian G'r(G) = logn p #|'Ohm_1(G)|.

End OhmProps.

Section AbelianStructure.

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

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

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

Fact abelian_type_subproof 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 A : sorted [rel m n | n %| m] (abelian_type A).

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

Lemma abelian_type_sorted A : sorted geq (abelian_type A).

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

Lemma count_logn_dprod_cycle 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 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 G : abelian Gsize (abelian_type G) = 'r(G).

Lemma mul_card_Ohm_Mho_abelian n G :
  abelian G → (#|'Ohm_n(G)| × #|'Mho^n(G)|)%N = #|G|.

Lemma grank_abelian G : abelian G'm(G) = 'r(G).

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

Lemma abelian_rank1_cyclic G : abelian Gcyclic G = ('r(G) 1).

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

Lemma homocyclic_Ohm_Mho n p G :
  p.-group Ghomocyclic G'Ohm_n(G) = 'Mho^(logn p (exponent G) - n)(G).

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

Lemma abelem_homocyclic p G : p.-abelem Ghomocyclic G.

Lemma homocyclic1 : homocyclic [1 gT].

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

Lemma abelian_type_homocyclic G :
  homocyclic Gabelian_type G = nseq 'r(G) (exponent G).

Lemma abelian_type_abelem p G : p.-abelem Gabelian_type G = nseq 'r(G) p.

Lemma max_card_abelian G :
  abelian G#|G| exponent G ^ 'r(G) ?= iff homocyclic G.

Lemma card_homocyclic G : homocyclic G#|G| = (exponent G ^ 'r(G))%N.

Lemma abelian_type_dprod_homocyclic p K H G :
    K \x H = Gp.-group Ghomocyclic G
     abelian_type K = nseq 'r(K) (exponent G)
   abelian_type H = nseq 'r(H) (exponent G).

Lemma dprod_homocyclic p K H G :
  K \x H = Gp.-group Ghomocyclic Ghomocyclic K homocyclic H.

Lemma exponent_dprod_homocyclic p K H G :
    K \x H = Gp.-group Ghomocyclic GK :!=: 1 →
  exponent K = exponent G.

End AbelianStructure.


Section IsogAbelian.

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

Lemma isog_abelian_type G H : isog G Habelian_type G = abelian_type H.

Lemma eq_abelian_type_isog G H :
  abelian Gabelian Hisog G H = (abelian_type G == abelian_type H).

Lemma isog_abelem_card p G H :
  p.-abelem Gisog G H = p.-abelem H && (#|H| == #|G|).

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

Lemma morphim_rank_abelian G : abelian G'r(f @* G) 'r(G).

Lemma morphim_p_rank_abelian p G : abelian G'r_p(f @* G) 'r_p(G).

Lemma isog_homocyclic G H : G \isog Hhomocyclic G = homocyclic H.

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.