# Library mathcomp.solvable.abelian

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

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div fintype finfun bigop finset prime binomial.
From mathcomp Require Import fingroup morphism perm automorphism action.
From mathcomp Require Import quotient gfunctor gproduct ssralg finalg zmodp.
From mathcomp Require Import cyclic 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.

Arguments exponent {gT} A%g.
Arguments abelem {gT} p%N A%g.
Arguments is_abelem {gT} A%g.
Arguments pElem {gT} p%N A%g.
Arguments pnElem {gT} p%N n%N A%g.
Arguments nElem {gT} n%N A%g.
Arguments pmaxElem {gT} p%N A%g.
Arguments p_rank {gT} p%N A%g.
Arguments rank {gT} A%g.
Arguments gen_rank {gT} A%g.

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.

Arguments Ohm n%N {gT} A%g.
Arguments Ohm_group n%N {gT} A%g.
Arguments Mho n%N {gT} A%g.
Arguments Mho_group n%N {gT} A%g.
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).
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 : core.

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)).
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)).
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)).
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.

Arguments LdivP {gT A n x}.
Arguments exponentP {gT A n}.
Arguments abelemP {gT p G}.
Arguments is_abelemP {gT G}.
Arguments pElemP {gT p A E}.
Arguments pnElemP {gT p n A E}.
Arguments nElemP {gT n G E}.
Arguments nElem1P {gT G E}.
Arguments pmaxElemP {gT p A E}.
Arguments pmaxElem_LdivP {gT p G E}.
Arguments p_rank_geP {gT p n G}.
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.