feat: port GroupTheory.CommutingProbability (#2284)

Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: int-y1 <jason_yuen2007@hotmail.com>

Mathlib.lean

@@ -689,6 +689,7 @@ import Mathlib.GroupTheory.Abelianization
 import Mathlib.GroupTheory.Archimedean
 import Mathlib.GroupTheory.Commensurable
 import Mathlib.GroupTheory.Commutator
+import Mathlib.GroupTheory.CommutingProbability
 import Mathlib.GroupTheory.Congruence
 import Mathlib.GroupTheory.Coset
 import Mathlib.GroupTheory.Divisible

Mathlib/GroupTheory/Abelianization.lean

@@ -89,7 +89,7 @@ namespace Abelianization
 
 attribute [local instance] QuotientGroup.leftRel
 
-instance : CommGroup (Abelianization G) :=
+instance commGroup : CommGroup (Abelianization G) :=
   { QuotientGroup.Quotient.group _ with
     mul_comm := fun x y =>
       Quotient.inductionOn₂' x y fun a b =>

Mathlib/GroupTheory/CommutingProbability.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2022 Thomas Browning. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning
+
+! This file was ported from Lean 3 source module group_theory.commuting_probability
+! leanprover-community/mathlib commit dc6c365e751e34d100e80fe6e314c3c3e0fd2988
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Algebra.Group.ConjFinite
+import Mathlib.GroupTheory.Abelianization
+import Mathlib.GroupTheory.GroupAction.ConjAct
+import Mathlib.GroupTheory.GroupAction.Quotient
+import Mathlib.GroupTheory.Index
+
+/-!
+# Commuting Probability
+This file introduces the commuting probability of finite groups.
+
+## Main definitions
+* `commProb`: The commuting probability of a finite type with a multiplication operation.
+
+## Todo
+* Neumann's theorem.
+-/
+noncomputable section
+
+open Classical
+
+open BigOperators
+
+open Fintype
+
+variable (M : Type _) [Mul M]
+
+/-- The commuting probability of a finite type with a multiplication operation. -/
+def commProb : ℚ :=
+  Nat.card { p : M × M // p.1 * p.2 = p.2 * p.1 } / (Nat.card M : ℚ) ^ 2
+#align comm_prob commProb
+
+theorem commProb_def :
+    commProb M = Nat.card { p : M × M // p.1 * p.2 = p.2 * p.1 } / (Nat.card M : ℚ) ^ 2 :=
+  rfl
+#align comm_prob_def commProb_def
+
+variable [Finite M]
+
+theorem commProb_pos [h : Nonempty M] : 0 < commProb M :=
+  h.elim fun x ↦
+    div_pos (Nat.cast_pos.mpr (Finite.card_pos_iff.mpr ⟨⟨(x, x), rfl⟩⟩))
+      (pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2)
+#align comm_prob_pos commProb_pos
+
+theorem commProb_le_one : commProb M ≤ 1 := by
+  refine' div_le_one_of_le _ (sq_nonneg (Nat.card M : ℚ))
+  rw [← Nat.cast_pow, Nat.cast_le, sq, ← Nat.card_prod]
+  apply Finite.card_subtype_le
+#align comm_prob_le_one commProb_le_one
+
+variable {M}
+
+theorem commProb_eq_one_iff [h : Nonempty M] :
+    commProb M = 1 ↔ Commutative ((· * ·) : M → M → M) := by
+  haveI := Fintype.ofFinite M
+  rw [commProb, ← Set.coe_setOf, Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
+  rw [div_eq_one_iff_eq, ← Nat.cast_pow, Nat.cast_inj, sq, ← card_prod,
+    set_fintype_card_eq_univ_iff, Set.eq_univ_iff_forall]
+  · exact ⟨fun h x y ↦ h (x, y), fun h x ↦ h x.1 x.2⟩
+  · exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr card_ne_zero)
+#align comm_prob_eq_one_iff commProb_eq_one_iff
+
+variable (G : Type _) [Group G] [Finite G]
+
+theorem card_comm_eq_card_conjClasses_mul_card :
+    Nat.card { p : G × G // p.1 * p.2 = p.2 * p.1 } = Nat.card (ConjClasses G) * Nat.card G := by
+  haveI := Fintype.ofFinite G
+  simp only [Nat.card_eq_fintype_card]
+  -- Porting note: Changed `calc` proof into a `rw` proof.
+  rw [card_congr (Equiv.subtypeProdEquivSigmaSubtype fun g h : G ↦ g * h = h * g), card_sigma,
+    sum_equiv ConjAct.toConjAct.toEquiv (fun a ↦ card { b // a * b = b * a })
+      (fun g ↦ card (MulAction.fixedBy (ConjAct G) G g))
+      fun g ↦ card_congr' <| congr_arg _ <| funext fun h ↦ mul_inv_eq_iff_eq_mul.symm.to_eq,
+    MulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group, ConjAct.card,
+    (Setoid.ext fun g h ↦ (Setoid.comm' _).trans isConj_iff.symm :
+      MulAction.orbitRel (ConjAct G) G = IsConj.setoid G),
+    @card_congr' (Quotient (IsConj.setoid G)) (ConjClasses G) _ _ rfl]
+
+#align card_comm_eq_card_conj_classes_mul_card card_comm_eq_card_conjClasses_mul_card
+
+theorem commProb_def' : commProb G = Nat.card (ConjClasses G) / Nat.card G := by
+  rw [commProb, card_comm_eq_card_conjClasses_mul_card, Nat.cast_mul, sq]
+  exact mul_div_mul_right _ _ (Nat.cast_ne_zero.mpr Finite.card_pos.ne')
+#align comm_prob_def' commProb_def'
+
+-- porting note: inserted [Group G]
+variable {G} [Group G] (H : Subgroup G)
+
+theorem Subgroup.commProb_subgroup_le : commProb H ≤ commProb G * (H.index : ℚ) ^ 2 := by
+  /- After rewriting with `commProb_def`, we reduce to showing that `G` has at least as many
+      commuting pairs as `H`. -/
+  rw [commProb_def, commProb_def, div_le_iff, mul_assoc, ← mul_pow, ← Nat.cast_mul,
+    mul_comm H.index, H.card_mul_index, div_mul_cancel, Nat.cast_le]
+  · refine' Finite.card_le_of_injective (fun p ↦ ⟨⟨p.1.1, p.1.2⟩, Subtype.ext_iff.mp p.2⟩) _
+    exact fun p q h ↦ by simpa only [Subtype.ext_iff, Prod.ext_iff] using h
+  · exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr Finite.card_pos.ne')
+  · exact pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2
+#align subgroup.comm_prob_subgroup_le Subgroup.commProb_subgroup_le
+
+theorem Subgroup.commProb_quotient_le [H.Normal] : commProb (G ⧸ H) ≤ commProb G * Nat.card H := by
+  /- After rewriting with `commProb_def'`, we reduce to showing that `G` has at least as many
+      conjugacy classes as `G ⧸ H`. -/
+  rw [commProb_def', commProb_def', div_le_iff, mul_assoc, ← Nat.cast_mul, ← Subgroup.index,
+    H.card_mul_index, div_mul_cancel, Nat.cast_le]
+  · apply Finite.card_le_of_surjective
+    show Function.Surjective (ConjClasses.map (QuotientGroup.mk' H))
+    exact ConjClasses.map_surjective Quotient.surjective_Quotient_mk''
+  · exact Nat.cast_ne_zero.mpr Finite.card_pos.ne'
+  · exact Nat.cast_pos.mpr Finite.card_pos
+#align subgroup.comm_prob_quotient_le Subgroup.commProb_quotient_le
+
+variable (G)
+
+theorem inv_card_commutator_le_commProb : (↑(Nat.card (commutator G)))⁻¹ ≤ commProb G :=
+  (inv_pos_le_iff_one_le_mul (Nat.cast_pos.mpr Finite.card_pos)).mpr
+    (le_trans (ge_of_eq (commProb_eq_one_iff.mpr (Abelianization.commGroup G).mul_comm))
+      (commutator G).commProb_quotient_le)
+#align inv_card_commutator_le_comm_prob inv_card_commutator_le_commProb