From bafc9b07c9ed730f5a07a8174ef9702028497304 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sat, 18 Feb 2023 15:48:32 +0000 Subject: [PATCH] feat: port GroupTheory.CommutingProbability (#2284) Co-authored-by: Moritz Firsching Co-authored-by: int-y1 --- Mathlib.lean | 1 + Mathlib/GroupTheory/Abelianization.lean | 2 +- Mathlib/GroupTheory/CommutingProbability.lean | 128 ++++++++++++++++++ 3 files changed, 130 insertions(+), 1 deletion(-) create mode 100644 Mathlib/GroupTheory/CommutingProbability.lean diff --git a/Mathlib.lean b/Mathlib.lean index f7e5a4dfb207e..1cf018658641b 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/GroupTheory/Abelianization.lean b/Mathlib/GroupTheory/Abelianization.lean index 0e69249d2d885..ad77999f02abb 100644 --- a/Mathlib/GroupTheory/Abelianization.lean +++ b/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 => diff --git a/Mathlib/GroupTheory/CommutingProbability.lean b/Mathlib/GroupTheory/CommutingProbability.lean new file mode 100644 index 0000000000000..f292041b80135 --- /dev/null +++ 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