The 5/8 theorem

If G is a nonabelian group, then its Mathlib commuting probability is at most 5/8. For infinite groups this is immediate because commProb is defined to be 0; the substantive finite case is the theorem of Gustafson, What is the probability that two group elements commute? (Amer. Math. Monthly 80, 1973), and the bound is attained (e.g. by the quaternion group of order 8).

The proof is the classical counting argument:

• If G is nonabelian then G ⧸ Z(G) is not cyclic, so the index of the center is not 1 or a prime; hence |Z(G)| / |G| ≤ 1/4.
• For g ∉ Z(G) the centralizer of g is a proper subgroup, so |C(g)| / |G| ≤ 1/2.
• Summing |C(g)| over g ∈ G counts the commuting pairs, and splitting the sum over Z(G) and its complement gives commProb G ≤ z + (1 - z) / 2 ≤ 1/2 + (1/4)/2 = 5/8, where z = |Z(G)| / |G|.

Main results

• FiveEighths.commProb_le_five_eighths: the commuting probability of a nonabelian group is at most 5/8.
• FiveEighths.centralFraction_le_quarter: the center of a finite nonabelian group contains at most a quarter of its elements.
• FiveEighths.centralizerFraction_le_half: the centralizer of a noncentral element contains at most half of the elements.

All declarations live in the FiveEighths namespace.

noncomputable def FiveEighths.centralFraction (G : Type u_1) [Group G] : ℚ

The fraction of elements of a finite group G that lie in its center.

Equations

• FiveEighths.centralFraction G = ↑(Nat.card ↥(Subgroup.center G)) / ↑(Nat.card G)

noncomputable def FiveEighths.centralizerFraction {G : Type u_1} [Group G] (g : G) : ℚ

The fraction of elements of a finite group that commute with a given element g.

Equations

• FiveEighths.centralizerFraction g = ↑(Nat.card ↥(Subgroup.centralizer {g})) / ↑(Nat.card G)

theorem FiveEighths.centralFraction_eq_one_div_index {G : Type u_1} [Group G] [Finite G] : centralFraction G = 1 / ↑(Subgroup.center G).index

theorem FiveEighths.center_index_ne_prime {G : Type u_1} [Group G] (h : ¬IsMulCommutative G) {p : ℕ} (hp : Nat.Prime p) : (Subgroup.center G).index ≠ p

If G is nonabelian then G ⧸ Z(G) is not cyclic, so the index of the center cannot be prime.

theorem FiveEighths.four_le_center_index {G : Type u_1} [Group G] [Finite G] (h : ¬IsMulCommutative G) : 4 ≤ (Subgroup.center G).index

The center of a finite nonabelian group has index at least 4: the index is nonzero by finiteness, is not 1 by noncommutativity, and is not 2 or 3 because those are prime.

theorem FiveEighths.centralFraction_le_quarter {G : Type u_1} [Group G] [Finite G] (h : ¬IsMulCommutative G) : centralFraction G ≤ 1 / 4

The center of a finite nonabelian group contains at most a quarter of its elements.

theorem FiveEighths.two_le_centralizer_index {G : Type u_1} [Group G] [Finite G] {g : G} (hg : g ∉ Subgroup.center G) : 2 ≤ (Subgroup.centralizer {g}).index

The centralizer of a noncentral element is a proper subgroup, so its index is at least 2.

theorem FiveEighths.centralizerFraction_le_half {G : Type u_1} [Group G] [Finite G] {g : G} (hg : g ∉ Subgroup.center G) : centralizerFraction g ≤ 1 / 2

The centralizer of a noncentral element contains at most half of the elements.

theorem FiveEighths.commProb_eq_ncard_div_sq (G : Type u_2) [Group G] : commProb G = ↑{(g, h) : G × G | g * h = h * g}.ncard / ↑(Nat.card G) ^ 2

The commuting probability of G counts the commuting pairs of elements.

@[reducible, inline]

noncomputable abbrev FiveEighths.typeQCard (G : Type u_2) : ℚ

The cardinality of a type, as a rational number (zero if the type is infinite).

Equations

• FiveEighths.typeQCard G = ↑(Nat.card G)

noncomputable def FiveEighths.setQCard {α : Type u_2} (s : Set α) : ℚ

The cardinality of a set, as a rational number (zero if the set is infinite).

Equations

• FiveEighths.setQCard s = ↑s.ncard

theorem FiveEighths.commProb_le_five_eighths (G : Type u_2) [Group G] (h : ¬IsMulCommutative G) : commProb G ≤ 5 / 8

The 5/8 theorem: the commuting probability of a nonabelian group is at most 5/8. For infinite groups, this follows from Mathlib's convention that commProb is 0; the finite case is Gustafson's theorem.