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

@@ -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

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`. -/

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

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 =>

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)

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