2 - The study of J₄ via the theory of uniqueness systems

Summary

This article serves as an exposition of the main result of. In we give the first computer free proof of the uniqueness of groups of type J₄. In addition we supply simplified proofs of some properties of such groups, such as the structure of certain subgroups.

A group of type J₄ is a finite group G possessing an involution z such that H = C_G(z) satisfies F*(H) = Q is extraspecial of order 2¹³, H/Q is isomorphic to ℝ₃ extended by Aut(M₂₂), and z^G ∩ Q ≠ {z}. We prove:

Main TheoremUp to isomorphism there exists at most one group of type J₄.

Janko was the first to consider groups of type J₄ in, where he established various properties of such groups. For example Janko showed that each group G of type J₄ is simple, he determined the order of G, and he described the normalizers of all subgroups of G of prime order. However Janko left open the question of whether there exist groups of type J₄ and whether all groups of type J₄ are isomorphic. Thus Janko is said to have discovered J₄ and indeed J₄ was the last of the 26 sporadic simple groups to be discovered.

Around 1980, Conway, Norton, Parker, and Thackray proved the existence and uniqueness of J₄ using extensive machine computation. This work is discussed briefly in. Norton et al. construct J₄ as a linear group in 112 dimensions over the field of order 2. While the notion of 2-local geometry did not exist at that time, this geometry plays an implicit role in.