These vary in length, some are open ended, some may be in reach within the week, others may involve much more work.
Defining semisimple groups and proving some of their basic properties (Isaacs, Finite Group Theory, page 274)
Semisimple Groups
A group G is semisimple if it is a product of nonabelian simple normal subgroups.
Lemma. Suppose that a finite group G is the product of the members of some collection X of
nonabelian simple normal subgroups.
Then the product is direct, and X is the set of all minimal normal subgroups of G.
Proof. The members of X are clearly minimal normal subgroups of G, and thus
if S ∈ X and N is a minimal normal subgroup of G different from S, then
N ∩ S = 1, and hence S centralizes N. It follows that the product of all members of
X different from N centralizes N.
We can certainly assume that X is nonempty. Let T ∈ X, and let K be the product of all
other members of X, so that T K = G.
By the result of the first paragraph, K centralizes T.
Since T is nonabelian and simple, it has trivial center, and thus
T ∩ K ⊆ Z(T) = 1.
It follows that
G = T K = T × K.
Now K is the product of the members of the collection X \ {T}, so working by induction
on |X|, it follows that this product is direct, and thus G = T × K is the direct product of
the members of X.
Finally, if N is minimal normal in G and N ∉ X, then by the result of the first paragraph,
N is centralized by Π X = G, and thus N ⊆ Z(G).
But G is a direct product of groups having trivial centers, so Z(G) = 1, and
this contradiction shows that X contains all minimal normal subgroups of G.
Minimal normal subgroups of finite groups are abelian or semisimple (Isaacs, Finite Group Theory, Lemma 9.6, page 275)
Lemma. Let N be a minimal normal subgroup of a finite group G.
Then either N is abelian, or it is semisimple.
Proof. Let S be a minimal normal subgroup of N.
If S is abelian, then S ⊆ F(N), and thus F(N) is a nontrivial normal subgroup of G contained in N.
Since N is minimal normal in G, we have F(N) = N, and thus N is nilpotent.
But then Z(N) is a nontrivial normal subgroup of G contained in N, and thus Z(N) = N,
so N is abelian.
We may now assume that S is nonabelian, and we argue that S is simple.
If K ◁ S, then K ◁ G, and thus by Theorem 2.6*, the minimal normal subgroup N of G normalizes K, and hence K ⊆ N. But K ⊆ S and S is minimal normal in N. Thus either K = 1 or K = S, which shows that S is simple, as required.
We may therefore assume that S is a nonabelian simple group.
Each conjugate of S in G is a nonabelian simple group that is normal in N, and
so the product Σ of these conjugates is semisimple. Also,
1 < Σ ◁ G, Σ ⊆ N,
and by the minimality of N, it follows that Σ = N.
Thus N is semisimple, as claimed.
Theorem 2.6.
Let S be a subnormal subgroup of the finite group G and let M be a minimal normal subgroup of G.
Then M is contained in the normaliser of S in G.
F(G)' ≤ F(G') holds.
Does it hold also for not necessarily finite groups?x and y in a (finite?) group generate a dihedral group of order 2|xy|.G is probably finite):
Let x and y be distinct involutions in G, n = |xy|, and D the subgroup generated by x , y. Then
D \ ⟨xy⟩ is an involution.n is odd then D is transitive on its involutions,
so in particular x is conjugate to y in D.If n is even then each involution in D is conjugate to exactly one of x, y, or z,
where z is the unique involution in ⟨xy⟩.
Further z is in the center of D.
[Suggestion: it is probably a good idea to define the “z” in this item explicitly and build some API around it.]
n is even and z is the involution in ⟨xy⟩ then xz is conjugate to x in D if and only if n = 0 mod 4.The Brauer-Fowler theorem (Aschbacher, Finite Simple Groups, Theorem 45.5, page 244)
Let H be a finite group.
Then there exists at most a finite number of finite simple groups G with an involution t such that C_G(t) = H.
Construct one of the 26 sporadic simple groups, prove that it is simple, compute its size, find the conjugacy classes of its involutions
For instance, formalising the Mathieu groups should be easily accessible.
The constructions of the sporadic groups often have a very combinatorial component.
mathlib has little support for such arguments.
This means that their formalisation will involve larger explorations of the available alternatives and probably some trial and error.