From c54060b4a386fb664d066bd0d611e2d9002d82f6 Mon Sep 17 00:00:00 2001 From: Eric Rodriguez Date: Mon, 14 Aug 2023 12:56:23 +0000 Subject: [PATCH] feat: the class equation (groups) (#6375) This is mostly mathported work of Johan's towards Wedderburn's Little theorem. Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com> --- Mathlib.lean | 1 + Mathlib/Algebra/BigOperators/Basic.lean | 4 + Mathlib/GroupTheory/ClassEquation.lean | 82 +++++++++++++++++++ Mathlib/GroupTheory/GroupAction/ConjAct.lean | 5 ++ Mathlib/GroupTheory/GroupAction/Quotient.lean | 9 ++ Mathlib/GroupTheory/Subgroup/Basic.lean | 31 +++++++ 6 files changed, 132 insertions(+) create mode 100644 Mathlib/GroupTheory/ClassEquation.lean diff --git a/Mathlib.lean b/Mathlib.lean index 9df11ea1dbb0b..cfeced9eb9168 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1962,6 +1962,7 @@ import Mathlib.Geometry.Manifold.VectorBundle.Tangent import Mathlib.Geometry.Manifold.WhitneyEmbedding import Mathlib.GroupTheory.Abelianization import Mathlib.GroupTheory.Archimedean +import Mathlib.GroupTheory.ClassEquation import Mathlib.GroupTheory.Commensurable import Mathlib.GroupTheory.Commutator import Mathlib.GroupTheory.CommutingProbability diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean index f91c9fe99e388..3b62e193e178e 100644 --- a/Mathlib/Algebra/BigOperators/Basic.lean +++ b/Mathlib/Algebra/BigOperators/Basic.lean @@ -925,6 +925,10 @@ theorem prod_subtype {p : α → Prop} {F : Fintype (Subtype p)} (s : Finset α) #align finset.prod_subtype Finset.prod_subtype #align finset.sum_subtype Finset.sum_subtype +@[to_additive] +theorem prod_set_coe (s : Set α) [Fintype s] : (∏ i : s, f i) = ∏ i in s.toFinset, f i := +(Finset.prod_subtype s.toFinset (fun _ ↦ Set.mem_toFinset) f).symm + /-- The product of a function `g` defined only on a set `s` is equal to the product of a function `f` defined everywhere, as long as `f` and `g` agree on `s`, and `f = 1` off `s`. -/ diff --git a/Mathlib/GroupTheory/ClassEquation.lean b/Mathlib/GroupTheory/ClassEquation.lean new file mode 100644 index 0000000000000..4f06e6d0ccbdb --- /dev/null +++ b/Mathlib/GroupTheory/ClassEquation.lean @@ -0,0 +1,82 @@ +/- +Copyright (c) 2021 Johan Commelin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johan Commelin, Eric Rodriguez +-/ + +import Mathlib.GroupTheory.GroupAction.Quotient +import Mathlib.Algebra.BigOperators.Finprod +import Mathlib.Data.Set.Card +import Mathlib.Algebra.Group.ConjFinite + +/-! +# Class Equation + +This file establishes the class equation for finite groups. + +## Main statements + +* `Group.card_center_add_sum_card_noncenter_eq_card`: The **class equation** for finite groups. + The cardinality of a group is equal to the size of its center plus the sum of the size of all its + nontrivial conjugacy classes. Also `Group.nat_card_center_add_sum_card_noncenter_eq_card`. + +-/ + +open ConjAct MulAction ConjClasses + +open scoped BigOperators + +variable (G : Type u) [Group G] + +/-- Conjugacy classes form a partition of G, stated in terms of cardinality. -/ +theorem sum_conjClasses_card_eq_card [Fintype <| ConjClasses G] [Fintype G] + [∀ x : ConjClasses G, Fintype x.carrier] : + ∑ x : ConjClasses G, x.carrier.toFinset.card = Fintype.card G := by + suffices : (Σ x : ConjClasses G, x.carrier) ≃ G + · simpa using (Fintype.card_congr this) + simpa [carrier_eq_preimage_mk] using Equiv.sigmaFiberEquiv ConjClasses.mk + +/-- Conjugacy classes form a partition of G, stated in terms of cardinality. -/ +theorem Group.sum_card_conj_classes_eq_card [Finite G] : + ∑ᶠ x : ConjClasses G, x.carrier.ncard = Nat.card G := by + classical + cases nonempty_fintype G + rw [Nat.card_eq_fintype_card, ←sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype] + simp [Set.ncard_eq_toFinset_card'] + +/-- The **class equation** for finite groups. The cardinality of a group is equal to the size +of its center plus the sum of the size of all its nontrivial conjugacy classes. -/ +theorem Group.nat_card_center_add_sum_card_noncenter_eq_card [Finite G] : + Nat.card (Subgroup.center G) + ∑ᶠ x ∈ noncenter G, Nat.card x.carrier = Nat.card G := by + classical + cases nonempty_fintype G + rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ← + Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ] + simp only [Nat.card_eq_fintype_card, Set.toFinset_card] + congr 1 + swap + · convert finsum_cond_eq_sum_of_cond_iff _ _ + simp [Set.mem_toFinset] + calc + Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) := + Fintype.card_congr ((mk_bijOn G).equiv _) + _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := + by rw [←Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff] + _ = _ := ?_ + rw [Finset.card_eq_sum_ones] + refine Finset.sum_congr rfl ?_ + rintro ⟨g⟩ hg + simp only [noncenter, Set.not_subsingleton_iff, Set.toFinset_setOf, Finset.mem_univ, true_and, + forall_true_left, Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg + rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one] + exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩ + +theorem Group.card_center_add_sum_card_noncenter_eq_card (G) [Group G] + [∀ x : ConjClasses G, Fintype x.carrier] [Fintype G] [Fintype <| Subgroup.center G] + [Fintype <| noncenter G] : Fintype.card (Subgroup.center G) + + ∑ x in (noncenter G).toFinset, x.carrier.toFinset.card = Fintype.card G := by + convert Group.nat_card_center_add_sum_card_noncenter_eq_card G using 2 + · simp + · rw [←finsum_set_coe_eq_finsum_mem (noncenter G), finsum_eq_sum_of_fintype, ←Finset.sum_set_coe] + simp + · simp diff --git a/Mathlib/GroupTheory/GroupAction/ConjAct.lean b/Mathlib/GroupTheory/GroupAction/ConjAct.lean index bdcdf72eb26f1..1b85cfa354ef5 100644 --- a/Mathlib/GroupTheory/GroupAction/ConjAct.lean +++ b/Mathlib/GroupTheory/GroupAction/ConjAct.lean @@ -309,6 +309,11 @@ theorem orbitRel_conjAct : (orbitRel (ConjAct G) G).Rel = IsConj := funext₂ fun g h => by rw [orbitRel_apply, mem_orbit_conjAct] #align conj_act.orbit_rel_conj_act ConjAct.orbitRel_conjAct +theorem orbit_eq_carrier_conjClasses [Group G] (g : G) : + orbit (ConjAct G) g = (ConjClasses.mk g).carrier := by + ext h + rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj, mem_orbit_conjAct] + theorem stabilizer_eq_centralizer (g : G) : stabilizer (ConjAct G) g = centralizer (zpowers (toConjAct g) : Set (ConjAct G)) := le_antisymm (le_centralizer_iff.mp (zpowers_le.mpr fun _ => mul_inv_eq_iff_eq_mul.mp)) fun _ h => diff --git a/Mathlib/GroupTheory/GroupAction/Quotient.lean b/Mathlib/GroupTheory/GroupAction/Quotient.lean index b0f460dc21590..99f419030b2fe 100644 --- a/Mathlib/GroupTheory/GroupAction/Quotient.lean +++ b/Mathlib/GroupTheory/GroupAction/Quotient.lean @@ -351,6 +351,15 @@ instance isPretransitive_quotient (G) [Group G] (H : Subgroup G) : IsPretransiti end MulAction +theorem ConjClasses.card_carrier [Group G] [Fintype G] (g : G) [Fintype (ConjClasses.mk g).carrier] + [Fintype <| MulAction.stabilizer (ConjAct G) g] : Fintype.card (ConjClasses.mk g).carrier = + Fintype.card G / Fintype.card (MulAction.stabilizer (ConjAct G) g) := by + classical + rw [Fintype.card_congr <| ConjAct.toConjAct (G := G) |>.toEquiv] + rw [←MulAction.card_orbit_mul_card_stabilizer_eq_card_group (ConjAct G) g, Nat.mul_div_cancel] + simp_rw [ConjAct.orbit_eq_carrier_conjClasses] + exact Fintype.card_pos_iff.mpr inferInstance + namespace Subgroup variable {G : Type*} [Group G] (H : Subgroup G) diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean index 08b70c4e8b7fe..6d8f20413987a 100644 --- a/Mathlib/GroupTheory/Subgroup/Basic.lean +++ b/Mathlib/GroupTheory/Subgroup/Basic.lean @@ -3717,4 +3717,35 @@ theorem eq_of_right_mem_center {g h : M} (H : IsConj g h) (Hh : h ∈ Set.center end IsConj +namespace ConjClasses + +/-- The conjugacy classes that are not trivial. -/ +def noncenter (G : Type _) [Monoid G] : Set (ConjClasses G) := + {x | x.carrier.Nontrivial} + +@[simp] lemma mem_noncenter [Monoid G] (g : ConjClasses G) : + g ∈ noncenter G ↔ g.carrier.Nontrivial := Iff.rfl + +theorem mk_bijOn (G : Type _) [Group G] : + Set.BijOn ConjClasses.mk (↑(Subgroup.center G)) (noncenter G)ᶜ := by + refine ⟨fun g hg ↦ ?_, fun x hx y _ H ↦ ?_, ?_⟩ + · simp only [mem_noncenter, Set.compl_def, Set.mem_setOf, Set.not_nontrivial_iff] + intro x hx y hy + simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy + rw [hx.eq_of_right_mem_center hg, hy.eq_of_right_mem_center hg] + · rw [mk_eq_mk_iff_isConj] at H + exact H.eq_of_left_mem_center hx + · rintro ⟨g⟩ hg + refine ⟨g, ?_, rfl⟩ + simp only [mem_noncenter, Set.compl_def, Set.mem_setOf, Set.not_nontrivial_iff] at hg + intro h + rw [← mul_inv_eq_iff_eq_mul] + refine hg ?_ mem_carrier_mk + rw [mem_carrier_iff_mk_eq] + apply mk_eq_mk_iff_isConj.mpr + rw [isConj_comm, isConj_iff] + exact ⟨h, rfl⟩ + +end ConjClasses + assert_not_exists Multiset