feat(group_theory/commuting_probability): Commuting probability inequalities (#11564)

This PR adds some inequalities for the commuting probability.

Author: tb65536

src/group_theory/commuting_probability.lean

@@ -3,8 +3,9 @@ Copyright (c) 2022 Thomas Browning. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
-import algebra.group.conj
+import group_theory.abelianization
 import group_theory.group_action.conj_act
+import group_theory.index
 
 /-!
 # Commuting Probability
@@ -42,6 +43,8 @@ begin
   apply set_fintype_card_le_univ,
 end
 
+variables {M}
+
 lemma comm_prob_eq_one_iff [h : nonempty M] : comm_prob M = 1 ↔ commutative ((*) : M → M → M) :=
 begin
   change (card {p : M × M | p.1 * p.2 = p.2 * p.1} : ℚ) / _ = 1 ↔ _,
@@ -72,3 +75,37 @@ begin
   rw [comm_prob, card_comm_eq_card_conj_classes_mul_card, nat.cast_mul, sq],
   exact mul_div_mul_right (card (conj_classes G)) (card G) (nat.cast_ne_zero.mpr card_ne_zero),
 end
+
+variables {G} (H : subgroup G)
+
+lemma subgroup.comm_prob_subgroup_le : comm_prob H ≤ comm_prob G * H.index ^ 2 :=
+begin
+  /- After rewriting with `comm_prob_def`, we reduce to showing that `G` has at least as many
+    commuting pairs as `H`. -/
+  rw [comm_prob_def, comm_prob_def, div_le_iff, mul_assoc, ←mul_pow, ←nat.cast_mul,
+      H.index_mul_card, div_mul_cancel, nat.cast_le],
+  { apply card_le_of_injective _ _,
+    exact λ p, ⟨⟨p.1.1, p.1.2⟩, subtype.ext_iff.mp p.2⟩,
+    exact λ p q h, by simpa only [subtype.ext_iff, prod.ext_iff] using h },
+  { exact pow_ne_zero 2 (nat.cast_ne_zero.mpr card_ne_zero) },
+  { exact pow_pos (nat.cast_pos.mpr card_pos) 2 },
+end
+
+lemma subgroup.comm_prob_quotient_le [H.normal] : comm_prob (G ⧸ H) ≤ comm_prob G * card H :=
+begin
+  /- After rewriting with `comm_prob_def'`, we reduce to showing that `G` has at least as many
+    conjugacy classes as `G ⧸ H`. -/
+  rw [comm_prob_def', comm_prob_def', div_le_iff, mul_assoc, ←nat.cast_mul, mul_comm (card H),
+      ←subgroup.card_eq_card_quotient_mul_card_subgroup, div_mul_cancel, nat.cast_le],
+  { exact card_le_of_surjective (conj_classes.map (quotient_group.mk' H))
+      (conj_classes.map_surjective quotient.surjective_quotient_mk') },
+  { exact nat.cast_ne_zero.mpr card_ne_zero },
+  { exact nat.cast_pos.mpr card_pos },
+end
+
+variables (G)
+
+lemma inv_card_commutator_le_comm_prob : (↑(card (commutator G)))⁻¹ ≤ comm_prob G :=
+(inv_pos_le_iff_one_le_mul (by exact nat.cast_pos.mpr card_pos)).mpr
+  (le_trans (ge_of_eq (comm_prob_eq_one_iff.mpr (abelianization.comm_group G).mul_comm))
+    (commutator G).comm_prob_quotient_le)