Formalising the Feit-Thompson Theorem:

completed on September 20, 2012

current version: May 21, 2013

Local Analysis for The Odd Order Theorem

by Helmut Bender, George Glauberman

Chapter I. Preliminary Results

• Elementary Properties of Solvable Groups

100%

1.1, 1.2, 1.3, 1.4, 1.5(a), 1.5(b), 1.5(c), 1.5(d), 1.5(e), 1.6(a), , 1.6(b), 1.6(c), 1.6(d), 1.6(e), 1.7(a), 1.7(b), 1.7(c), 1.7(d), 1.8, 1.9, 1.10, 1.11, 1.12, 1.13 1.14, 1.15(a), 1.15(b), 1.16, 1.17, 1.18, 1.19(a), 1.19(b), 1.20, 1.21(a), 1.21(b), 1.21(c), 1.21(d), 1.21(e), 1.22
• General Results on Representations

100%

2.1(a), 2.1(b), 2.1(c), 2.2, 2.3, 2.4(a), 2.4(b), 2.4(c), 2.4(d), 2.4(e), 2.4(f), 2.4(g), 2.4(h), 2.4(j), 2.4(k), 2.5, 2.6(a), 2.6(b), 2.7
• Actions of Frobenius Groups and Related Results

100%

3.1, 3.2(a), 3.2(b), 3.3, 3.4, 3.5, 3.6, 3.7, 3.8, 3.9, 3.10
• p-Groups of Small Rank

100%

4.1, 4.2(a), 4.2(b), 4.3, 4.4(a), 4.4(b), 4.5(a), 4.5(b), 4.5(c), 4.6, 4.7, 4.8(a), 4.8(b), 4.9, 4.10, 4.11, 4.12, 4.13, 4.14, 4.15, 4.16, 4.17, 4.18(a), 4.18(b), 4.18(c), 4.18(d), 4.18(e), 4.19, 4.20(a), 4.20(b), 4.20(c1) 4.20(c2) 4.20(c3)
• Narrow p-Groups

100%

5.1(a), 5.1(b), 5.2, 5.3, 5.3(c), 5.4, 5.5, 5.6, 5.7
• Additional Results

100%

6.1, 6.2, 6.3(a), 6.3(b), 6.4, 6.5(a), 6.5(b), 6.5(c), 6.6(a1), 6.6(a2), 6.6(b), 6.6(c), 6.6(d), 6.7

Chapter II. The Uniqueness Theorem

• The Transitivity Theorem

100%

7.1, 7.2, 7.3, 7.4, 7.5(a), 7.5(b), 7.6
• The Fitting Subgroup of a Maximal Subgroup

100%

8.1(a), 8.1(b)
• The Uniqueness Theorem

100%

9.1(a), 9.1(b), 9.2, 9.3, 9.4, 9.5, 9.6

Chapter III. Maximal Subgroups

• The Subgoups M_α and M_σ

100%

10.1(a,b,c), 10.1(d), 10.2(a1), 10.2(a2), 10.2(b1), 10.2(b2), 10.2(c), 10.2(d1), 10.2(d2), 10.2(e), 10.3, 10.4(a), 10.4(b), 10.4(c1), 10.4(c2), 10.5(1), 10.5(2), 10.6, 10.7(a1), 10.7(a2), 10.7(b), 10.7(c), 10.7(d), 10.7(e), 10.8(a1), 10.8(a2), 10.8(b), 10.8(c), 10.9(a), 10.9(b), 10.10, 10.11(a), 10.11(b), 10.11(c), 10.11(d), 10.12, 10.13, 10.14(a) 10.14(b) 10.14(c) 10.14(d)
• Exceptional Maximal Subgroups

100%

11.1, 11.2, 11.3, 11.4, 11.5, 11.6, 11.7
• The Subgroup E

100%

12.1(a), 12.1(b-f), 12.1(g), 12.2(a), 12.2(b), 12.3, 12.4, 12.5(a), 12.5(b-f), 12.6(a,b,c,f), 12.6(d,e), 12.7, 12.8(c), 12.8(a,b,d,e), 12.8, 12.9, 12.10(a), 12.10(b1), 12.10(b2), 12.10(c), 12.10(d), 12.10(e), 12.11, 12.12, 12.13, 12.14, 12.15, 12.16, 12.17, 12.18, 12.19
• Prime Action

100%

13.1, 13.2, 13.3(a), 13.3(b), 13.4, 13.5, 13.6, 13.7, 13.8, 13.9, 13.10, 13.11, 13.12, 13.13

Chapter IV. The Family of All Maximal Subgroups of G

• Maximal Subgroups of Type P and Counting Arguments

100%

14.1, 14.2, 14.3, 14.4, 14.5(a), 14.5(b), 14.5(c), 14.6, 14.7, 14.8(1), 14.8(2), 14.9, 14.10, 14.11, 14.12, 14.13
• The Subgroup M_F

100%

15.1, 15.2, 15.3(a), 15.3(b), 15.4, 15.5, 15.6, 15.7, 15.8, 15.9
• The Main Results

100%

A, B, C, D, E, 16.1, 16.1(a), 16.1(b), 16.1(c), 16.1(d), 16.1(e), 16.1(f), I, II

Appendices

100%

100%

100%

Character Theory for The Odd Order Theorem

by Thomas Peterfalvi

Part I Character Theory for the Odd Order Theorem

1. Preliminary Results from Character Theory

100%

1.1, 1.2, 1.3(a), 1.3(b), 1.4, 1.5(a), 1.5(b), 1.5(c), 1.5(d), 1.5(e), 1.6(a), 1.6(b), 1.7(a) , 1.7(b) , 1.7(c) , 1.8, 1.9(a) , 1.9(b) , 1.10(a) 1.10(b)
2. The Dade Isometry

100%

2.1, 2.2, 2.3, 2.4, 2.5, 2.6(a), 2.6(b), 2.7(a), 2.7(b), 2.8, 2.10, 2.10.1, 2.10.2, 2.10.3, 2.11
3. TI-Subsets with Cyclic Normalizers

100%

3.2, 3.4, 3.5, 3.7, 3.8, 3.9(a), 3.9(b), 3.9(c)

4. The Dade Isometry for a Certain Type of Subgroup

100%

4.1, 4.3(a), 4.3(b, c), 4.3(d), 4.4, 4.5(a), 4.5(b), 4.7, 4.8, 4.9, 4.10
5. Coherence

100%

5.3(a), 5.3(b), 5.4, 5.5, 5.6, 5.7, 5.8, 5.9(a), 5.9(b)
6. Some Coherence Theorems

100%

6.2, 6.3, 6.5, 6.6, 6.7, 6.8
7. Non-existence of a Certain Type of Group of Odd Order

100%

7.2(a), 7.2(b), 7.3, 7.5, 7.7, 7.8, 7.9, 7.10, 7.11
8. Structure of a Minimal Simple Group of Odd Order

100%

8.2, 8.5, 8.8, 8.9, 8.11, 8.12, 8.13, 8.15, 8.16, 8.17, 8.18
9. On the Maximal Subgroups of G of Types II, III and IV

100%

9.1, 9.3, 9.4, 9.6, 9.7(a), 9.7(b), 9.8(a -- d) , 9.9(a -- c) , 9.10 , 9.11 ,
10. Maximal Subgroups of Types III, IV and V

100%

10.2, 10.3, 10.5, 10.6(a), 10.6(b), 10.7, 10.8, 10.9, 10.10, 10.11
11. Maximal Subgroups of Types III and IV

100%

11.1 , 11.3 , 11.4 , 11.5 , 11.6 , 11.7 , 11.8 , 11.9
12. Maximal Subgroups of Types I

100%

12.2(a) , 12.2(b) , 12.3 , 12.4 , 12.5 , 12.6 , 12.7 , 12.9 , 12.10 , 12.11 , 12.12 , 12.14 , 12.15 , 12.16 , 12.17
13. The Subgroups S and T

100%

13.2, 13.3(a), 13.3(b), 13.3(c), 13.4, 13.5(a b c), 13.6, 13.7, 13.8, 13.9(a), 13.9(b), 13.10, 13.11(a b c), 13.12, 13.13, 13.14, 13.15, 13.16, 13.17(a b c) , 13.18(a b c d), 13.19(a b c)
14. Non-existence of G

100%

14.2 , 14.4 , 14.5 , 14.6 , 14.7 , 14.8(a) , 14.8(b) , 14.9 , 14.11 , 14.12 , 14.14 , 14.15 , 14.16