-
Notifications
You must be signed in to change notification settings - Fork 110
/
abelian.v
2180 lines (1869 loc) · 87.5 KB
/
abelian.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* (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.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
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.
Prenex Implicits exponent.
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.
Proof.
move=> p_x; rewrite /order -cycle_eq1.
by case/(pgroup_pdiv p_x)=> p_pr _ [k ->]; rewrite pdiv_pfactor.
Qed.
Lemma OhmPredP (x : gT) :
reflect (exists2 p, prime p & x ^+ (p ^ n) = 1) (x ^+ (pdiv #[x] ^ n) == 1).
Proof.
have [-> | nt_x] := eqVneq x 1.
by rewrite expg1n eqxx; left; exists 2; rewrite ?expg1n.
apply: (iffP idP) => [/eqP | [p p_pr /eqP x_pn]].
by exists (pdiv #[x]); rewrite ?pdiv_prime ?order_gt1.
rewrite (@pdiv_p_elt p) //; rewrite -order_dvdn in x_pn.
by rewrite [p_elt _ _](pnat_dvd x_pn) // pnat_exp pnat_id.
Qed.
Lemma Mho_p_elt (p : nat) x : x \in A -> p.-elt x -> x ^+ (p ^ n) \in Mho.
Proof.
move=> Ax p_x; case: (eqVneq x 1) => [-> | ntx]; first by rewrite groupX.
by apply: mem_gen; apply/imsetP; exists x; rewrite ?inE ?Ax (pdiv_p_elt p_x).
Qed.
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)).
Proof. by rewrite !inE; apply: (iffP andP) => [] [-> /eqP]. Qed.
Lemma dvdn_exponent x A : x \in A -> #[x] %| exponent A.
Proof. by move=> Ax; rewrite (biglcmn_sup x). Qed.
Lemma expg_exponent x A : x \in A -> x ^+ exponent A = 1.
Proof. by move=> Ax; apply/eqP; rewrite -order_dvdn dvdn_exponent. Qed.
Lemma exponentS A B : A \subset B -> exponent A %| exponent B.
Proof.
by move=> sAB; apply/dvdn_biglcmP=> x Ax; rewrite dvdn_exponent ?(subsetP sAB).
Qed.
Lemma exponentP A n :
reflect (forall x, x \in A -> x ^+ n = 1) (exponent A %| n).
Proof.
apply: (iffP (dvdn_biglcmP _ _ _)) => eAn x Ax.
by apply/eqP; rewrite -order_dvdn eAn.
by rewrite order_dvdn eAn.
Qed.
Arguments exponentP {A n}.
Lemma trivg_exponent G : (G :==: 1) = (exponent G %| 1).
Proof.
rewrite -subG1.
by apply/subsetP/exponentP=> trG x /trG; rewrite expg1 => /set1P.
Qed.
Lemma exponent1 : exponent [1 gT] = 1%N.
Proof. by apply/eqP; rewrite -dvdn1 -trivg_exponent eqxx. Qed.
Lemma exponent_dvdn G : exponent G %| #|G|.
Proof. by apply/dvdn_biglcmP=> x Gx; apply: order_dvdG. Qed.
Lemma exponent_gt0 G : 0 < exponent G.
Proof. exact: dvdn_gt0 (exponent_dvdn G). Qed.
Hint Resolve exponent_gt0 : core.
Lemma pnat_exponent pi G : pi.-nat (exponent G) = pi.-group G.
Proof.
congr (_ && _); first by rewrite cardG_gt0 exponent_gt0.
apply: eq_all_r => p; rewrite !mem_primes cardG_gt0 exponent_gt0 /=.
apply: andb_id2l => p_pr; apply/idP/idP=> pG.
exact: dvdn_trans pG (exponent_dvdn G).
by case/Cauchy: pG => // x Gx <-; apply: dvdn_exponent.
Qed.
Lemma exponentJ A x : exponent (A :^ x) = exponent A.
Proof.
rewrite /exponent (reindex_inj (conjg_inj x)).
by apply: eq_big => [y | y _]; rewrite ?orderJ ?memJ_conjg.
Qed.
Lemma exponent_witness G : nilpotent G -> {x | x \in G & exponent G = #[x]}.
Proof.
move=> nilG; have [//=| /= x Gx max_x] := @arg_maxP _ 1 (mem G) order.
exists x => //; apply/eqP; rewrite eqn_dvd dvdn_exponent // andbT.
apply/dvdn_biglcmP=> y Gy; apply/dvdn_partP=> //= p.
rewrite mem_primes => /andP[p_pr _]; have p_gt1: p > 1 := prime_gt1 p_pr.
rewrite p_part pfactor_dvdn // -(leq_exp2l _ _ p_gt1) -!p_part.
rewrite -(leq_pmul2r (part_gt0 p^' #[x])) partnC // -!order_constt.
rewrite -orderM ?order_constt ?coprime_partC // ?max_x ?groupM ?groupX //.
case/dprodP: (nilpotent_pcoreC p nilG) => _ _ cGpGp' _.
have inGp := mem_normal_Hall (nilpotent_pcore_Hall _ nilG) (pcore_normal _ _).
by red; rewrite -(centsP cGpGp') // inGp ?p_elt_constt ?groupX.
Qed.
Lemma exponent_cycle x : exponent <[x]> = #[x].
Proof. by apply/eqP; rewrite eqn_dvd exponent_dvdn dvdn_exponent ?cycle_id. Qed.
Lemma exponent_cyclic X : cyclic X -> exponent X = #|X|.
Proof. by case/cyclicP=> x ->; apply: exponent_cycle. Qed.
Lemma primes_exponent G : primes (exponent G) = primes (#|G|).
Proof.
apply/eq_primes => p; rewrite !mem_primes exponent_gt0 cardG_gt0 /=.
by apply: andb_id2l => p_pr; apply: negb_inj; rewrite -!p'natE // pnat_exponent.
Qed.
Lemma pi_of_exponent G : \pi(exponent G) = \pi(G).
Proof. by rewrite /pi_of primes_exponent. Qed.
Lemma partn_exponentS pi H G :
H \subset G -> #|G|`_pi %| #|H| -> (exponent H)`_pi = (exponent G)`_pi.
Proof.
move=> sHG Gpi_dvd_H; apply/eqP; rewrite eqn_dvd.
rewrite partn_dvd ?exponentS ?exponent_gt0 //=; apply/dvdn_partP=> // p.
rewrite pi_of_part ?exponent_gt0 // => /andP[_ /= pi_p].
have sppi: {subset (p : nat_pred) <= pi} by move=> q /eqnP->.
have [P sylP] := Sylow_exists p H; have sPH := pHall_sub sylP.
have{sylP} sylP: p.-Sylow(G) P.
rewrite pHallE (subset_trans sPH) //= (card_Hall sylP) eqn_dvd andbC.
by rewrite -{1}(partn_part _ sppi) !partn_dvd ?cardSg ?cardG_gt0.
rewrite partn_part ?partn_biglcm //.
apply: (@big_ind _ (dvdn^~ _)) => [|m n|x Gx]; first exact: dvd1n.
by rewrite dvdn_lcm => ->.
rewrite -order_constt; have p_y := p_elt_constt p x; set y := x.`_p in p_y *.
have sYG: <[y]> \subset G by rewrite cycle_subG groupX.
have [z _ Pyz] := Sylow_Jsub sylP sYG p_y.
rewrite (bigD1 (y ^ z)) ?(subsetP sPH) -?cycle_subG ?cycleJ //=.
by rewrite orderJ part_pnat_id ?dvdn_lcml // (pi_pnat p_y).
Qed.
Lemma exponent_Hall pi G H : pi.-Hall(G) H -> exponent H = (exponent G)`_pi.
Proof.
move=> hallH; have [sHG piH _] := and3P hallH.
rewrite -(partn_exponentS sHG) -?(card_Hall hallH) ?part_pnat_id //.
by apply: pnat_dvd piH; apply: exponent_dvdn.
Qed.
Lemma exponent_Zgroup G : Zgroup G -> exponent G = #|G|.
Proof.
move/forall_inP=> ZgG; apply/eqP; rewrite eqn_dvd exponent_dvdn.
apply/(dvdn_partP _ (cardG_gt0 _)) => p _.
have [S sylS] := Sylow_exists p G; rewrite -(card_Hall sylS).
have /cyclicP[x defS]: cyclic S by rewrite ZgG ?(p_Sylow sylS).
by rewrite defS dvdn_exponent // -cycle_subG -defS (pHall_sub sylS).
Qed.
Lemma cprod_exponent A B G :
A \* B = G -> lcmn (exponent A) (exponent B) = (exponent G).
Proof.
case/cprodP=> [[K H -> ->{A B}] <- cKH].
apply/eqP; rewrite eqn_dvd dvdn_lcm !exponentS ?mulG_subl ?mulG_subr //=.
apply/exponentP=> _ /imset2P[x y Kx Hy ->].
rewrite -[1]mulg1 expgMn; last by red; rewrite -(centsP cKH).
congr (_ * _); apply/eqP; rewrite -order_dvdn.
by rewrite (dvdn_trans (dvdn_exponent Kx)) ?dvdn_lcml.
by rewrite (dvdn_trans (dvdn_exponent Hy)) ?dvdn_lcmr.
Qed.
Lemma dprod_exponent A B G :
A \x B = G -> lcmn (exponent A) (exponent B) = (exponent G).
Proof.
case/dprodP=> [[K H -> ->{A B}] defG cKH _].
by apply: cprod_exponent; rewrite cprodE.
Qed.
Lemma sub_LdivT A n : (A \subset 'Ldiv_n()) = (exponent A %| n).
Proof. by apply/subsetP/exponentP=> eAn x /eAn; rewrite inE => /eqP. Qed.
Lemma LdivT_J n x : 'Ldiv_n() :^ x = 'Ldiv_n().
Proof.
apply/setP=> y; rewrite !inE mem_conjg inE -conjXg.
by rewrite (canF_eq (conjgKV x)) conj1g.
Qed.
Lemma LdivJ n A x : 'Ldiv_n(A :^ x) = 'Ldiv_n(A) :^ x.
Proof. by rewrite conjIg LdivT_J. Qed.
Lemma sub_Ldiv A n : (A \subset 'Ldiv_n(A)) = (exponent A %| n).
Proof. by rewrite subsetI subxx sub_LdivT. Qed.
Lemma group_Ldiv G n : abelian G -> group_set 'Ldiv_n(G).
Proof.
move=> cGG; apply/group_setP.
split=> [|x y]; rewrite !inE ?group1 ?expg1n //=.
case/andP=> Gx /eqP xn /andP[Gy /eqP yn].
by rewrite groupM //= expgMn ?xn ?yn ?mulg1 //; apply: (centsP cGG).
Qed.
Lemma abelian_exponent_gen A : abelian A -> exponent <<A>> = exponent A.
Proof.
rewrite -abelian_gen; set n := exponent A; set G := <<A>> => cGG.
apply/eqP; rewrite eqn_dvd andbC exponentS ?subset_gen //= -sub_Ldiv.
rewrite -(gen_set_id (group_Ldiv n cGG)) genS // subsetI subset_gen /=.
by rewrite sub_LdivT.
Qed.
Lemma abelem_pgroup p A : p.-abelem A -> p.-group A.
Proof. by case/andP. Qed.
Lemma abelem_abelian p A : p.-abelem A -> abelian A.
Proof. by case/and3P. Qed.
Lemma abelem1 p : p.-abelem [1 gT].
Proof. by rewrite /abelem pgroup1 abelian1 exponent1 dvd1n. Qed.
Lemma abelemE p G : prime p -> p.-abelem G = abelian G && (exponent G %| p).
Proof.
move=> p_pr; rewrite /abelem -pnat_exponent andbA -!(andbC (_ %| _)).
by case: (dvdn_pfactor _ 1 p_pr) => // [[k _ ->]]; rewrite pnat_exp pnat_id.
Qed.
Lemma abelemP p G :
prime p ->
reflect (abelian G /\ forall x, x \in G -> x ^+ p = 1) (p.-abelem G).
Proof.
by move=> p_pr; rewrite abelemE //; apply: (iffP andP) => [] [-> /exponentP].
Qed.
Lemma abelem_order_p p G x : p.-abelem G -> x \in G -> x != 1 -> #[x] = p.
Proof.
case/and3P=> pG _ eG Gx; rewrite -cycle_eq1 => ntX.
have{ntX} [p_pr p_x _] := pgroup_pdiv (mem_p_elt pG Gx) ntX.
by apply/eqP; rewrite eqn_dvd p_x andbT order_dvdn (exponentP eG).
Qed.
Lemma cyclic_abelem_prime p X : p.-abelem X -> cyclic X -> X :!=: 1 -> #|X| = p.
Proof.
move=> abelX cycX; case/cyclicP: cycX => x -> in abelX *.
by rewrite cycle_eq1; apply: abelem_order_p abelX (cycle_id x).
Qed.
Lemma cycle_abelem p x : p.-elt x || prime p -> p.-abelem <[x]> = (#[x] %| p).
Proof.
move=> p_xVpr; rewrite /abelem cycle_abelian /=.
apply/andP/idP=> [[_ xp1] | x_dvd_p].
by rewrite order_dvdn (exponentP xp1) ?cycle_id.
split; last exact: dvdn_trans (exponent_dvdn _) x_dvd_p.
by case/orP: p_xVpr => // /pnat_id; apply: pnat_dvd.
Qed.
Lemma exponent2_abelem G : exponent G %| 2 -> 2.-abelem G.
Proof.
move/exponentP=> expG; apply/abelemP=> //; split=> //.
apply/centsP=> x Gx y Gy; apply: (mulIg x); apply: (mulgI y).
by rewrite -!mulgA !(mulgA y) -!(expgS _ 1) !expG ?mulg1 ?groupM.
Qed.
Lemma prime_abelem p G : prime p -> #|G| = p -> p.-abelem G.
Proof.
move=> p_pr oG; rewrite /abelem -oG exponent_dvdn.
by rewrite /pgroup cyclic_abelian ?prime_cyclic ?oG ?pnat_id.
Qed.
Lemma abelem_cyclic p G : p.-abelem G -> cyclic G = (logn p #|G| <= 1).
Proof.
move=> abelG; have [pG _ expGp] := and3P abelG.
case: (eqsVneq G 1) => [-> | ntG]; first by rewrite cyclic1 cards1 logn1.
have [p_pr _ [e oG]] := pgroup_pdiv pG ntG; apply/idP/idP.
case/cyclicP=> x defG; rewrite -(pfactorK 1 p_pr) dvdn_leq_log ?prime_gt0 //.
by rewrite defG order_dvdn (exponentP expGp) // defG cycle_id.
by rewrite oG pfactorK // ltnS leqn0 => e0; rewrite prime_cyclic // oG (eqP e0).
Qed.
Lemma abelemS p H G : H \subset G -> p.-abelem G -> p.-abelem H.
Proof.
move=> sHG /and3P[cGG pG Gp1]; rewrite /abelem.
by rewrite (pgroupS sHG) // (abelianS sHG) // (dvdn_trans (exponentS sHG)).
Qed.
Lemma abelemJ p G x : p.-abelem (G :^ x) = p.-abelem G.
Proof. by rewrite /abelem pgroupJ abelianJ exponentJ. Qed.
Lemma cprod_abelem p A B G :
A \* B = G -> p.-abelem G = p.-abelem A && p.-abelem B.
Proof.
case/cprodP=> [[H K -> ->{A B}] defG cHK].
apply/idP/andP=> [abelG | []].
by rewrite !(abelemS _ abelG) // -defG (mulG_subl, mulG_subr).
case/and3P=> pH cHH expHp; case/and3P=> pK cKK expKp.
rewrite -defG /abelem pgroupM pH pK abelianM cHH cKK cHK /=.
apply/exponentP=> _ /imset2P[x y Hx Ky ->].
rewrite expgMn; last by red; rewrite -(centsP cHK).
by rewrite (exponentP expHp) // (exponentP expKp) // mul1g.
Qed.
Lemma dprod_abelem p A B G :
A \x B = G -> p.-abelem G = p.-abelem A && p.-abelem B.
Proof.
move=> defG; case/dprodP: (defG) => _ _ _ tiHK.
by apply: cprod_abelem; rewrite -dprodEcp.
Qed.
Lemma is_abelem_pgroup p G : p.-group G -> is_abelem G = p.-abelem G.
Proof.
rewrite /is_abelem => pG.
case: (eqsVneq G 1) => [-> | ntG]; first by rewrite !abelem1.
by have [p_pr _ [k ->]] := pgroup_pdiv pG ntG; rewrite pdiv_pfactor.
Qed.
Lemma is_abelemP G : reflect (exists2 p, prime p & p.-abelem G) (is_abelem G).
Proof.
apply: (iffP idP) => [abelG | [p p_pr abelG]].
case: (eqsVneq G 1) => [-> | ntG]; first by exists 2; rewrite ?abelem1.
by exists (pdiv #|G|); rewrite ?pdiv_prime // ltnNge -trivg_card_le1.
by rewrite (is_abelem_pgroup (abelem_pgroup abelG)).
Qed.
Lemma pElemP p A E : reflect (E \subset A /\ p.-abelem E) (E \in 'E_p(A)).
Proof. by rewrite inE; apply: andP. Qed.
Arguments pElemP {p A E}.
Lemma pElemS p A B : A \subset B -> 'E_p(A) \subset 'E_p(B).
Proof.
by move=> sAB; apply/subsetP=> E; rewrite !inE => /andP[/subset_trans->].
Qed.
Lemma pElemI p A B : 'E_p(A :&: B) = 'E_p(A) :&: subgroups B.
Proof. by apply/setP=> E; rewrite !inE subsetI andbAC. Qed.
Lemma pElemJ x p A E : ((E :^ x)%G \in 'E_p(A :^ x)) = (E \in 'E_p(A)).
Proof. by rewrite !inE conjSg abelemJ. Qed.
Lemma pnElemP p n A E :
reflect [/\ E \subset A, p.-abelem E & logn p #|E| = n] (E \in 'E_p^n(A)).
Proof. by rewrite !inE -andbA; apply: (iffP and3P) => [] [-> -> /eqP]. Qed.
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.
Proof.
by case/pnElemP=> -> abelE <-; rewrite -card_pgroup // abelem_pgroup.
Qed.
Lemma card_pnElem p n A E : E \in 'E_p^n(A) -> #|E| = (p ^ n)%N.
Proof. by case/pnElemPcard. Qed.
Lemma pnElem0 p G : 'E_p^0(G) = [set 1%G].
Proof.
apply/setP=> E; rewrite !inE -andbA; apply/and3P/idP=> [[_ pE] | /eqP->].
apply: contraLR; case/(pgroup_pdiv (abelem_pgroup pE)) => p_pr _ [k ->].
by rewrite pfactorK.
by rewrite sub1G abelem1 cards1 logn1.
Qed.
Lemma pnElem_prime p n A E : E \in 'E_p^n.+1(A) -> prime p.
Proof. by case/pnElemP=> _ _; rewrite lognE; case: prime. Qed.
Lemma pnElemE p n A :
prime p -> 'E_p^n(A) = [set E in 'E_p(A) | #|E| == (p ^ n)%N].
Proof.
move/pfactorK=> pnK; apply/setP=> E; rewrite 3!inE.
case: (@andP (E \subset A)) => //= [[_]] /andP[/p_natP[k ->] _].
by rewrite pnK (can_eq pnK).
Qed.
Lemma pnElemS p n A B : A \subset B -> 'E_p^n(A) \subset 'E_p^n(B).
Proof.
move=> sAB; apply/subsetP=> E.
by rewrite !inE -!andbA => /andP[/subset_trans->].
Qed.
Lemma pnElemI p n A B : 'E_p^n(A :&: B) = 'E_p^n(A) :&: subgroups B.
Proof. by apply/setP=> E; rewrite !inE subsetI -!andbA; do !bool_congr. Qed.
Lemma pnElemJ x p n A E : ((E :^ x)%G \in 'E_p^n(A :^ x)) = (E \in 'E_p^n(A)).
Proof. by rewrite inE pElemJ cardJg !inE. Qed.
Lemma abelem_pnElem p n G :
p.-abelem G -> n <= logn p #|G| -> exists E, E \in 'E_p^n(G).
Proof.
case: n => [|n] abelG lt_nG; first by exists 1%G; rewrite pnElem0 set11.
have p_pr: prime p by move: lt_nG; rewrite lognE; case: prime.
case/(normal_pgroup (abelem_pgroup abelG)): lt_nG => // E [sEG _ oE].
by exists E; rewrite pnElemE // !inE oE sEG (abelemS sEG) /=.
Qed.
Lemma card_p1Elem p A X : X \in 'E_p^1(A) -> #|X| = p.
Proof. exact: card_pnElem. Qed.
Lemma p1ElemE p A : prime p -> 'E_p^1(A) = [set X in subgroups A | #|X| == p].
Proof.
move=> p_pr; apply/setP=> X; rewrite pnElemE // !inE -andbA; congr (_ && _).
by apply: andb_idl => /eqP oX; rewrite prime_abelem ?oX.
Qed.
Lemma TIp1ElemP p A X Y :
X \in 'E_p^1(A) -> Y \in 'E_p^1(A) -> reflect (X :&: Y = 1) (X :!=: Y).
Proof.
move=> EpX EpY; have p_pr := pnElem_prime EpX.
have [oX oY] := (card_p1Elem EpX, card_p1Elem EpY).
have [<- |] := altP eqP.
by right=> X1; rewrite -oX -(setIid X) X1 cards1 in p_pr.
by rewrite eqEcard oX oY leqnn andbT; left; rewrite prime_TIg ?oX.
Qed.
Lemma card_p1Elem_pnElem p n A E :
E \in 'E_p^n(A) -> #|'E_p^1(E)| = (\sum_(i < n) p ^ i)%N.
Proof.
case/pnElemP=> _ {A} abelE dimE; have [pE cEE _] := and3P abelE.
have [E1 | ntE] := eqsVneq E 1.
rewrite -dimE E1 cards1 logn1 big_ord0 eq_card0 // => X.
by rewrite !inE subG1 trivg_card1; case: eqP => // ->; rewrite logn1 andbF.
have [p_pr _ _] := pgroup_pdiv pE ntE; have p_gt1 := prime_gt1 p_pr.
apply/eqP; rewrite -(@eqn_pmul2l (p - 1)) ?subn_gt0 // subn1 -predn_exp.
have groupD1_inj: injective (fun X => (gval X)^#).
apply: can_inj (@generated_group _) _ => X.
by apply: val_inj; rewrite /= genD1 ?group1 ?genGid.
rewrite -dimE -card_pgroup // (cardsD1 1 E) group1 /= mulnC.
rewrite -(card_imset _ groupD1_inj) eq_sym.
apply/eqP; apply: card_uniform_partition => [X'|].
case/imsetP=> X; rewrite pnElemE // expn1 => /setIdP[_ /eqP <-] ->.
by rewrite (cardsD1 1 X) group1.
apply/and3P; split; last 1 first.
- apply/imsetP=> [[X /card_p1Elem oX X'0]].
by rewrite -oX (cardsD1 1) -X'0 group1 cards0 in p_pr.
- rewrite eqEsubset; apply/andP; split.
by apply/bigcupsP=> _ /imsetP[X /pnElemP[sXE _ _] ->]; apply: setSD.
apply/subsetP=> x /setD1P[ntx Ex].
apply/bigcupP; exists <[x]>^#; last by rewrite !inE ntx cycle_id.
apply/imsetP; exists <[x]>%G; rewrite ?p1ElemE // !inE cycle_subG Ex /=.
by rewrite -orderE (abelem_order_p abelE).
apply/trivIsetP=> _ _ /imsetP[X EpX ->] /imsetP[Y EpY ->]; apply/implyP.
rewrite (inj_eq groupD1_inj) -setI_eq0 -setDIl setD_eq0 subG1.
by rewrite (sameP eqP (TIp1ElemP EpX EpY)) implybb.
Qed.
Lemma card_p1Elem_p2Elem p A E : E \in 'E_p^2(A) -> #|'E_p^1(E)| = p.+1.
Proof. by move/card_p1Elem_pnElem->; rewrite big_ord_recl big_ord1. Qed.
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).
Proof.
move=> Ep2E EpX EpY; have [_ abelE oE] := pnElemPcard Ep2E.
apply: (iffP (TIp1ElemP EpX EpY)) => [tiXY|]; last by case/dprodP.
have [[sXE _ oX] [sYE _ oY]] := (pnElemPcard EpX, pnElemPcard EpY).
rewrite dprodE ?(sub_abelian_cent2 (abelem_abelian abelE)) //.
by apply/eqP; rewrite eqEcard mul_subG //= TI_cardMg // oX oY oE.
Qed.
Lemma nElemP n G E : reflect (exists p, E \in 'E_p^n(G)) (E \in 'E^n(G)).
Proof.
rewrite ['E^n(G)]big_mkord.
apply: (iffP bigcupP) => [[[p /= _] _] | [p]]; first by exists p.
case: n => [|n EpnE]; first by rewrite pnElem0; exists ord0; rewrite ?pnElem0.
suffices lepG: p < #|G|.+1 by exists (Ordinal lepG).
have:= EpnE; rewrite pnElemE ?(pnElem_prime EpnE) // !inE -andbA ltnS.
case/and3P=> sEG _ oE; rewrite dvdn_leq // (dvdn_trans _ (cardSg sEG)) //.
by rewrite (eqP oE) dvdn_exp.
Qed.
Arguments nElemP {n G E}.
Lemma nElem0 G : 'E^0(G) = [set 1%G].
Proof.
apply/setP=> E; apply/nElemP/idP=> [[p] |]; first by rewrite pnElem0.
by exists 2; rewrite pnElem0.
Qed.
Lemma nElem1P G E :
reflect (E \subset G /\ exists2 p, prime p & #|E| = p) (E \in 'E^1(G)).
Proof.
apply: (iffP nElemP) => [[p pE] | [sEG [p p_pr oE]]].
have p_pr := pnElem_prime pE; rewrite pnElemE // !inE -andbA in pE.
by case/and3P: pE => -> _ /eqP; split; last exists p.
exists p; rewrite pnElemE // !inE sEG oE eqxx abelemE // -oE exponent_dvdn.
by rewrite cyclic_abelian // prime_cyclic // oE.
Qed.
Lemma nElemS n G H : G \subset H -> 'E^n(G) \subset 'E^n(H).
Proof.
move=> sGH; apply/subsetP=> E /nElemP[p EpnG_E].
by apply/nElemP; exists p; rewrite // (subsetP (pnElemS _ _ sGH)).
Qed.
Lemma nElemI n G H : 'E^n(G :&: H) = 'E^n(G) :&: subgroups H.
Proof.
apply/setP=> E; apply/nElemP/setIP=> [[p] | []].
by rewrite pnElemI; case/setIP; split=> //; apply/nElemP; exists p.
by case/nElemP=> p EpnG_E sHE; exists p; rewrite pnElemI inE EpnG_E.
Qed.
Lemma def_pnElem p n G : 'E_p^n(G) = 'E_p(G) :&: 'E^n(G).
Proof.
apply/setP=> E; rewrite inE in_setI; apply: andb_id2l => /pElemP[sEG abelE].
apply/idP/nElemP=> [|[q]]; first by exists p; rewrite !inE sEG abelE.
rewrite !inE -2!andbA => /and4P[_ /pgroupP qE _].
case: (eqVneq E 1%G) => [-> | ]; first by rewrite cards1 !logn1.
case/(pgroup_pdiv (abelem_pgroup abelE)) => p_pr pE _.
by rewrite (eqnP (qE p p_pr pE)).
Qed.
Lemma pmaxElemP 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)).
Proof. by rewrite [E \in 'E*_p(A)]inE; apply: (iffP maxgroupP). Qed.
Lemma pmaxElem_exists p A D :
D \in 'E_p(A) -> {E | E \in 'E*_p(A) & D \subset E}.
Proof.
move=> EpD; have [E maxE sDE] := maxgroup_exists (EpD : mem 'E_p(A) D).
by exists E; rewrite // inE.
Qed.
Lemma pmaxElem_LdivP p G E :
prime p -> reflect ('Ldiv_p('C_G(E)) = E) (E \in 'E*_p(G)).
Proof.
move=> p_pr; apply: (iffP (pmaxElemP p G E)) => [[] | defE].
case/pElemP=> sEG abelE maxE; have [_ cEE eE] := and3P abelE.
apply/setP=> x; rewrite !inE -andbA; apply/and3P/idP=> [[Gx cEx xp] | Ex].
rewrite -(maxE (<[x]> <*> E)%G) ?joing_subr //.
by rewrite -cycle_subG joing_subl.
rewrite inE join_subG cycle_subG Gx sEG /=.
rewrite (cprod_abelem _ (cprodEY _)); last by rewrite centsC cycle_subG.
by rewrite cycle_abelem ?p_pr ?orbT // order_dvdn xp.
by rewrite (subsetP sEG) // (subsetP cEE) // (exponentP eE).
split=> [|H]; last first.
case/pElemP=> sHG /abelemP[// | cHH Hp1] sEH.
apply/eqP; rewrite eqEsubset sEH andbC /= -defE; apply/subsetP=> x Hx.
by rewrite 3!inE (subsetP sHG) // Hp1 ?(subsetP (centsS _ cHH)) /=.
apply/pElemP; split; first by rewrite -defE -setIA subsetIl.
apply/abelemP=> //; rewrite /abelian -{1 3}defE setIAC subsetIr.
by split=> //; apply/exponentP; rewrite -sub_LdivT setIAC subsetIr.
Qed.
Lemma pmaxElemS p A B :
A \subset B -> 'E*_p(B) :&: subgroups A \subset 'E*_p(A).
Proof.
move=> sAB; apply/subsetP=> E; rewrite !inE.
case/andP=> /maxgroupP[/pElemP[_ abelE] maxE] sEA.
apply/maxgroupP; rewrite inE sEA; split=> // D EpD.
by apply: maxE; apply: subsetP EpD; apply: pElemS.
Qed.
Lemma pmaxElemJ p A E x : ((E :^ x)%G \in 'E*_p(A :^ x)) = (E \in 'E*_p(A)).
Proof.
apply/pmaxElemP/pmaxElemP=> [] [EpE maxE].
rewrite pElemJ in EpE; split=> //= H EpH sEH; apply: (act_inj 'Js x).
by apply: maxE; rewrite ?conjSg ?pElemJ.
rewrite pElemJ; split=> // H; rewrite -(actKV 'JG x H) pElemJ conjSg => EpHx'.
by move/maxE=> /= ->.
Qed.
Lemma grank_min B : 'm(<<B>>) <= #|B|.
Proof.
by rewrite /gen_rank; case: arg_minP => [|_ _ -> //]; rewrite genGid.
Qed.
Lemma grank_witness G : {B | <<B>> = G & #|B| = 'm(G)}.
Proof.
rewrite /gen_rank; case: arg_minP => [|B defG _]; first by rewrite genGid.
by exists B; first apply/eqP.
Qed.
Lemma p_rank_witness p G : {E | E \in 'E_p^('r_p(G))(G)}.
Proof.
have [E EG_E mE]: {E | E \in 'E_p(G) & 'r_p(G) = logn p #|E| }.
by apply: eq_bigmax_cond; rewrite (cardD1 1%G) inE sub1G abelem1.
by exists E; rewrite inE EG_E -mE /=.
Qed.
Lemma p_rank_geP p n G : reflect (exists E, E \in 'E_p^n(G)) (n <= 'r_p(G)).
Proof.
apply: (iffP idP) => [|[E]]; last first.
by rewrite inE => /andP[Ep_E /eqP <-]; rewrite (bigmax_sup E).
have [D /pnElemP[sDG abelD <-]] := p_rank_witness p G.
by case/abelem_pnElem=> // E; exists E; apply: (subsetP (pnElemS _ _ sDG)).
Qed.
Lemma p_rank_gt0 p H : ('r_p(H) > 0) = (p \in \pi(H)).
Proof.
rewrite mem_primes cardG_gt0 /=; apply/p_rank_geP/andP=> [[E] | [p_pr]].
case/pnElemP=> sEG _; rewrite lognE; case: and3P => // [[-> _ pE] _].
by rewrite (dvdn_trans _ (cardSg sEG)).
case/Cauchy=> // x Hx ox; exists <[x]>%G; rewrite 2!inE [#|_|]ox cycle_subG.
by rewrite Hx (pfactorK 1) ?abelemE // cycle_abelian -ox exponent_dvdn.
Qed.
Lemma p_rank1 p : 'r_p([1 gT]) = 0.
Proof. by apply/eqP; rewrite eqn0Ngt p_rank_gt0 /= cards1. Qed.
Lemma logn_le_p_rank p A E : E \in 'E_p(A) -> logn p #|E| <= 'r_p(A).
Proof. by move=> EpA_E; rewrite (bigmax_sup E). Qed.
Lemma p_rank_le_logn p G : 'r_p(G) <= logn p #|G|.
Proof.
have [E EpE] := p_rank_witness p G.
by have [sEG _ <-] := pnElemP EpE; apply: lognSg.
Qed.
Lemma p_rank_abelem p G : p.-abelem G -> 'r_p(G) = logn p #|G|.
Proof.
move=> abelG; apply/eqP; rewrite eqn_leq andbC (bigmax_sup G) //.
by apply/bigmax_leqP=> E; rewrite inE => /andP[/lognSg->].
by rewrite inE subxx.
Qed.
Lemma p_rankS p A B : A \subset B -> 'r_p(A) <= 'r_p(B).
Proof.
move=> sAB; apply/bigmax_leqP=> E /(subsetP (pElemS p sAB)) EpB_E.
by rewrite (bigmax_sup E).
Qed.
Lemma p_rankElem_max p A : 'E_p^('r_p(A))(A) \subset 'E*_p(A).
Proof.
apply/subsetP=> E /setIdP[EpE dimE].
apply/pmaxElemP; split=> // F EpF sEF; apply/eqP.
have pF: p.-group F by case/pElemP: EpF => _ /and3P[].
have pE: p.-group E by case/pElemP: EpE => _ /and3P[].
rewrite eq_sym eqEcard sEF dvdn_leq // (card_pgroup pE) (card_pgroup pF).
by rewrite (eqP dimE) dvdn_exp2l // logn_le_p_rank.
Qed.
Lemma p_rankJ p A x : 'r_p(A :^ x) = 'r_p(A).
Proof.
rewrite /p_rank (reindex_inj (act_inj 'JG x)).
by apply: eq_big => [E | E _]; rewrite ?cardJg ?pElemJ.
Qed.
Lemma p_rank_Sylow p G H : p.-Sylow(G) H -> 'r_p(H) = 'r_p(G).
Proof.
move=> sylH; apply/eqP; rewrite eqn_leq (p_rankS _ (pHall_sub sylH)) /=.
apply/bigmax_leqP=> E; rewrite inE => /andP[sEG abelE].
have [P sylP sEP] := Sylow_superset sEG (abelem_pgroup abelE).
have [x _ ->] := Sylow_trans sylP sylH.
by rewrite p_rankJ -(p_rank_abelem abelE) (p_rankS _ sEP).
Qed.
Lemma p_rank_Hall pi p G H : pi.-Hall(G) H -> p \in pi -> 'r_p(H) = 'r_p(G).
Proof.
move=> hallH pi_p; have [P sylP] := Sylow_exists p H.
by rewrite -(p_rank_Sylow sylP) (p_rank_Sylow (subHall_Sylow hallH pi_p sylP)).
Qed.
Lemma p_rank_pmaxElem_exists p r G :
'r_p(G) >= r -> exists2 E, E \in 'E*_p(G) & 'r_p(E) >= r.
Proof.
case/p_rank_geP=> D /setIdP[EpD /eqP <- {r}].
have [E EpE sDE] := pmaxElem_exists EpD; exists E => //.
case/pmaxElemP: EpE => /setIdP[_ abelE] _.
by rewrite (p_rank_abelem abelE) lognSg.
Qed.
Lemma rank1 : 'r([1 gT]) = 0.
Proof. by rewrite ['r(1)]big1_seq // => p _; rewrite p_rank1. Qed.
Lemma p_rank_le_rank p G : 'r_p(G) <= 'r(G).
Proof.
case: (posnP 'r_p(G)) => [-> //|]; rewrite p_rank_gt0 mem_primes.
case/and3P=> p_pr _ pG; have lepg: p < #|G|.+1 by rewrite ltnS dvdn_leq.
by rewrite ['r(G)]big_mkord (bigmax_sup (Ordinal lepg)).
Qed.
Lemma rank_gt0 G : ('r(G) > 0) = (G :!=: 1).
Proof.
case: (eqsVneq G 1) => [-> |]; first by rewrite rank1 eqxx.
case: (trivgVpdiv G) => [-> | [p p_pr]]; first by case/eqP.
case/Cauchy=> // x Gx oxp ->; apply: leq_trans (p_rank_le_rank p G).
have EpGx: <[x]>%G \in 'E_p(G).
by rewrite inE cycle_subG Gx abelemE // cycle_abelian -oxp exponent_dvdn.
by apply: leq_trans (logn_le_p_rank EpGx); rewrite -orderE oxp logn_prime ?eqxx.
Qed.
Lemma rank_witness G : {p | prime p & 'r(G) = 'r_p(G)}.
Proof.
have [p _ defmG]: {p : 'I_(#|G|.+1) | true & 'r(G) = 'r_p(G)}.
by rewrite ['r(G)]big_mkord; apply: eq_bigmax_cond; rewrite card_ord.
case: (eqsVneq G 1) => [-> | ]; first by exists 2; rewrite // rank1 p_rank1.
by rewrite -rank_gt0 defmG p_rank_gt0 mem_primes; case/andP; exists p.
Qed.
Lemma rank_pgroup p G : p.-group G -> 'r(G) = 'r_p(G).
Proof.
move=> pG; apply/eqP; rewrite eqn_leq p_rank_le_rank andbT.
rewrite ['r(G)]big_mkord; apply/bigmax_leqP=> [[q /= _] _].
case: (posnP 'r_q(G)) => [-> // |]; rewrite p_rank_gt0 mem_primes.
by case/and3P=> q_pr _ qG; rewrite (eqnP (pgroupP pG q q_pr qG)).
Qed.
Lemma rank_Sylow p G P : p.-Sylow(G) P -> 'r(P) = 'r_p(G).
Proof.
move=> sylP; have pP := pHall_pgroup sylP.
by rewrite -(p_rank_Sylow sylP) -(rank_pgroup pP).
Qed.
Lemma rank_abelem p G : p.-abelem G -> 'r(G) = logn p #|G|.
Proof.
by move=> abelG; rewrite (rank_pgroup (abelem_pgroup abelG)) p_rank_abelem.
Qed.
Lemma nt_pnElem p n E A : E \in 'E_p^n(A) -> n > 0 -> E :!=: 1.
Proof. by case/pnElemP=> _ /rank_abelem <- <-; rewrite rank_gt0. Qed.
Lemma rankJ A x : 'r(A :^ x) = 'r(A).
Proof. by rewrite /rank cardJg; apply: eq_bigr => p _; rewrite p_rankJ. Qed.
Lemma rankS A B : A \subset B -> 'r(A) <= 'r(B).
Proof.
move=> sAB; rewrite /rank !big_mkord; apply/bigmax_leqP=> p _.
have leAB: #|A| < #|B|.+1 by rewrite ltnS subset_leq_card.
by rewrite (bigmax_sup (widen_ord leAB p)) // p_rankS.
Qed.
Lemma rank_geP n G : reflect (exists E, E \in 'E^n(G)) (n <= 'r(G)).
Proof.
apply: (iffP idP) => [|[E]].
have [p _ ->] := rank_witness G; case/p_rank_geP=> E.
by rewrite def_pnElem; case/setIP; exists E.
case/nElemP=> p; rewrite inE => /andP[EpG_E /eqP <-].
by rewrite (leq_trans (logn_le_p_rank EpG_E)) ?p_rank_le_rank.
Qed.
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.
Proof.
apply/exponentP=> _ /morphimP[x Dx Gx ->].
by rewrite -morphX // expg_exponent // morph1.
Qed.
Lemma morphim_LdivT n : f @* 'Ldiv_n() \subset 'Ldiv_n().
Proof.
apply/subsetP=> _ /morphimP[x Dx xn ->]; rewrite inE in xn.
by rewrite inE -morphX // (eqP xn) morph1.
Qed.
Lemma morphim_Ldiv n A : f @* 'Ldiv_n(A) \subset 'Ldiv_n(f @* A).
Proof.
by apply: subset_trans (morphimI f A _) (setIS _ _); apply: morphim_LdivT.
Qed.
Lemma morphim_abelem p G : p.-abelem G -> p.-abelem (f @* G).
Proof.
case: (eqsVneq G 1) => [-> | ntG] abelG; first by rewrite morphim1 abelem1.
have [p_pr _ _] := pgroup_pdiv (abelem_pgroup abelG) ntG.
case/abelemP: abelG => // abG elemG; apply/abelemP; rewrite ?morphim_abelian //.
by split=> // _ /morphimP[x Dx Gx ->]; rewrite -morphX // elemG ?morph1.
Qed.
Lemma morphim_pElem p G E : E \in 'E_p(G) -> (f @* E)%G \in 'E_p(f @* G).
Proof.
by rewrite !inE => /andP[sEG abelE]; rewrite morphimS // morphim_abelem.
Qed.
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)}.
Proof.
rewrite inE => /andP[EpE /eqP <-].
by exists (logn p #|f @* E|); rewrite ?logn_morphim // inE morphim_pElem /=.
Qed.
Lemma morphim_grank G : G \subset D -> 'm(f @* G) <= 'm(G).
Proof.
have [B defG <-] := grank_witness G; rewrite -defG gen_subG => sBD.
by rewrite morphim_gen ?morphimEsub ?(leq_trans (grank_min _)) ?leq_imset_card.
Qed.
(* 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.
Proof. by apply/eqP; rewrite eqn_dvd -{3}defG !exponent_morphim. Qed.
Lemma injm_Ldiv n A : f @* 'Ldiv_n(A) = 'Ldiv_n(f @* A).
Proof.
apply/eqP; rewrite eqEsubset morphim_Ldiv.
rewrite -[f @* 'Ldiv_n(A)](morphpre_invm injf).
rewrite -sub_morphim_pre; last by rewrite subIset ?morphim_sub.
rewrite injmI ?injm_invm // setISS ?morphim_LdivT //.
by rewrite sub_morphim_pre ?morphim_sub // morphpre_invm.
Qed.
Lemma injm_abelem p : p.-abelem (f @* G) = p.-abelem G.
Proof. by apply/idP/idP; first rewrite -{2}defG; apply: morphim_abelem. Qed.
Lemma injm_pElem p (E : {group aT}) :
E \subset D -> ((f @* E)%G \in 'E_p(f @* G)) = (E \in 'E_p(G)).
Proof.
move=> sED; apply/idP/idP=> EpE; last exact: morphim_pElem.
by rewrite -defG -(group_inj (morphim_invm injf sED)) morphim_pElem.
Qed.
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)).
Proof. by move=> sED; rewrite inE injm_pElem // card_injm ?inE. Qed.
Lemma injm_nElem n (E : {group aT}) :
E \subset D -> ((f @* E)%G \in 'E^n(f @* G)) = (E \in 'E^n(G)).
Proof.
move=> sED; apply/nElemP/nElemP=> [] [p EpE];
by exists p; rewrite injm_pnElem in EpE *.