+ +

Library mathcomp.solvable.abelian

+ +

+(* (c) Copyright 2006-2016 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.
+ +
+ +
+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).
+ +
+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 )).
+ +
+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 )).
+ +
+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 )).
+ +
+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.
+ +
+ +
+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.
+ +
+