# Library mathcomp.solvable.abelian

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.                                  *)

Require Import mathcomp.ssreflect.ssreflect.

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 x x != 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 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) : 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 A x ^+ exponent A = 1.

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

Lemma exponentP A n :
reflect ( x, x \in A x ^+ 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 X exponent 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) H exponent H = (exponent G)_pi.

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

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

Lemma dprod_exponent A B G :
A \x B = G lcmn (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 G group_set 'Ldiv_n(G).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Lemma is_abelem_pgroup p G : p.-group G is_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 G n 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 H H :=: 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 p reflect ('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) H p \in pi 'r_p(H) = 'r_p(G).

Lemma p_rank_pmaxElem_exists 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 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 G p.-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 G p.-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 H G \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 G abelian '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 D f @* '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 G abelian 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 D f @* 'Ohm_n(G) \subset 'Ohm_n(f @* G).

Lemma injm_Ohm (f : {morphism D >-> rT}) :
'injm f G \subset D f @* '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 G x \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 G p.-abelem 'Ohm_1(G) = abelian 'Ohm_1(G).

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

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

Lemma abelem_Ohm1P p G :
abelian G p.-group G reflect ('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 G p.-group G G :!=: 1 #|'Ohm_1(G)| = p.

Lemma cyclic_pgroup_dprod_trivg p A B C :
p.-group C cyclic C A \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 p exponent '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 G abelian 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 G abelian G [splits G, over <[x]>].

Lemma abelem_splits p G H : p.-abelem G H \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 G size (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 G cyclic G = ('r(G) 1).

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

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

Lemma Ohm_Mho_homocyclic (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 p G : p.-abelem G homocyclic G.

Lemma homocyclic1 : homocyclic [1 gT].

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

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

Lemma abelian_type_abelem p G : p.-abelem G abelian_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 = G p.-group G homocyclic 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 = G p.-group G homocyclic G homocyclic K homocyclic H.

Lemma exponent_dprod_homocyclic p K H G :
K \x H = G p.-group G homocyclic G K :!=: 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 H abelian_type G = abelian_type H.

Lemma eq_abelian_type_isog G H :
abelian G abelian H isog G H = (abelian_type G == abelian_type H).

Lemma isog_abelem_card 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 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 H homocyclic 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.

Section FimModAbelem.

Import GRing.Theory FinRing.Theory.

Lemma fin_lmod_char_abelem p (R : ringType) (V : finLmodType R):
p \in [char R]%R p.-abelem [set: V].

Lemma fin_Fp_lmod_abelem p (V : finLmodType 'F_p) :
prime p p.-abelem [set: V].

Lemma fin_ring_char_abelem p (R : finRingType) :
p \in [char R]%R p.-abelem [set: R].

End FimModAbelem.