FormalConjectures.Paper.ConjugacyClassSizes

FormalConjectures
Paper
ConjugacyClassSizes

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

The $S_3$-conjecture (conjugacy classes of distinct sizes)

References:

W. Zhou, I. Gorshkov, On ${2,3,5}$-groups with conjugacy classes of distinct sizes, arXiv:2606.22244 (2026).

F. M. Markel, Groups with many conjugate elements, J. Algebra 26 (1973), 69–74. (Origin of the $S_3$-conjecture.)

R. Knörr, W. Lempken, B. Thielcke, The $S_3$-conjecture for solvable groups, Israel J. Math. 91 (1995), 61–76.

J. Zhang, Finite groups with many conjugate elements, J. Algebra 170 (1994), 608–624.

Z. Arad, M. Muzychuk, A. Oliver, On groups with conjugacy classes of distinct sizes, J. Algebra 280 (2004), 537–576.

Conjugacy class

A finite group in which distinct conjugacy classes have distinct cardinalities is called an anti-homogeneous group (or ah-group). The symmetric group $S_3$ is an ah-group: its three conjugacy classes have sizes $1$, $2$, and $3$. Markel's $S_3$-conjecture (1973) asserts that, up to isomorphism, $S_3$ is the only nontrivial finite ah-group. The conjecture has been proved for all solvable groups (independently by Zhang and by Knörr–Lempken–Thielcke), but the general non-solvable case remains open.


namespace ConjugacyClassSizes


open ConjClasses

The cardinality of the conjugacy class c.

noncomputable def conjClassCard {G : Type*} [Monoid G] (c : ConjClasses G) : ℕ :=
  Nat.card c.carrier

A finite group G satisfies HasDistinctConjClassSizes if the map assigning to each conjugacy class the cardinality of its carrier is injective, i.e. distinct conjugacy classes have distinct sizes.

Such a group is called an anti-homogeneous group (or ah-group).

def HasDistinctConjClassSizes (G : Type*) [Group G] [Fintype G] : Prop :=
  Function.Injective (conjClassCard (G := G))

Equivalently, two conjugacy classes with the same cardinality must coincide.

@[category API, AMS 20]
theorem hasDistinctConjClassSizes_iff {G : Type*} [Group G] [Fintype G] :
    HasDistinctConjClassSizes G ↔
      ∀ (a b : ConjClasses G), conjClassCard a = conjClassCard b → a = b := byG:Type u_1inst✝¹:Group Ginst✝:Fintype G⊢ HasDistinctConjClassSizes G ↔ ∀ (a b : ConjClasses G), conjClassCard a = conjClassCard b → a = b
  simp only [HasDistinctConjClassSizes, Function.Injective]All goals completed! 🐙

The trivial group is anti-homogeneous, since it has a single conjugacy class.

@[category test, AMS 20]
theorem hasDistinctConjClassSizes_of_subsingleton {G : Type*} [Group G] [Fintype G]
    [Subsingleton G] : HasDistinctConjClassSizes (G := G) := byG:Type u_1inst✝²:Group Ginst✝¹:Fintype Ginst✝:Subsingleton G⊢ HasDistinctConjClassSizes G
  have hsub : Subsingleton (ConjClasses G) :=
    inferInstanceAs (Subsingleton (Quotient (IsConj.setoid G)))G:Type u_1inst✝²:Group Ginst✝¹:Fintype Ginst✝:Subsingleton Ghsub:Subsingleton (ConjClasses G) := inferInstanceAs (Subsingleton (Quotient (IsConj.setoid G)))⊢ HasDistinctConjClassSizes G
  rw [hasDistinctConjClassSizes_iff]G:Type u_1inst✝²:Group Ginst✝¹:Fintype Ginst✝:Subsingleton Ghsub:Subsingleton (ConjClasses G) := inferInstanceAs (Subsingleton (Quotient (IsConj.setoid G)))⊢ ∀ (a b : ConjClasses G), conjClassCard a = conjClassCard b → a = b
  intros a b _G:Type u_1inst✝²:Group Ginst✝¹:Fintype Ginst✝:Subsingleton Ghsub:Subsingleton (ConjClasses G) := inferInstanceAs (Subsingleton (Quotient (IsConj.setoid G)))a:ConjClasses Gb:ConjClasses Ga✝:conjClassCard a = conjClassCard b⊢ a = b
  exact Subsingleton.elim a bAll goals completed! 🐙

An anti-homogeneous group has trivial center, since each central element is in its own conjugacy class.

@[category test, AMS 20]
theorem trivial_center_of_hasDistinctConjClassSizes {G : Type*} [Group G] [Fintype G]
    (h : HasDistinctConjClassSizes G) : Subgroup.center G = ⊥ := byG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes G⊢ Subgroup.center G = ⊥
  -- A central element `w` is conjugate only to itself, so its conjugacy class is `{w}`.
  have hcard : ∀ w : G, w ∈ Subgroup.center G → conjClassCard (ConjClasses.mk w) = 1 := byG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes G⊢ Subgroup.center G = ⊥
    intro w hwG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Gw:Ghw:w ∈ Subgroup.center G⊢ conjClassCard (ConjClasses.mk w) = 1
    have hset : ConjClasses.carrier (ConjClasses.mk w) = {w} := byG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes G⊢ Subgroup.center G = ⊥
      ext ahG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Gw:Ghw:w ∈ Subgroup.center Ga:G⊢ a ∈ (ConjClasses.mk w).carrier ↔ a ∈ {w}
      rw [ConjClasses.mem_carrier_iff_mk_eq, ConjClasses.mk_eq_mk_iff_isConj,
        Set.mem_singleton_iff]hG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Gw:Ghw:w ∈ Subgroup.center Ga:G⊢ IsConj a w ↔ a = w
      constructorh.mpG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Gw:Ghw:w ∈ Subgroup.center Ga:G⊢ IsConj a w → a = wh.mprG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Gw:Ghw:w ∈ Subgroup.center Ga:G⊢ a = w → IsConj a w
      ·h.mpG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Gw:Ghw:w ∈ Subgroup.center Ga:G⊢ IsConj a w → a = w rintro ⟨c, hc⟩h.mpG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Gw:Ghw:w ∈ Subgroup.center Ga:Gc:Gˣhc:SemiconjBy (↑c) a w⊢ a = w
        rw [SemiconjBy] at hch.mpG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Gw:Ghw:w ∈ Subgroup.center Ga:Gc:Gˣhc:↑c * a = w * ↑c⊢ a = w
        have : c * a = c * w := byG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes G⊢ Subgroup.center G = ⊥ rw [hc]G:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Gw:Ghw:w ∈ Subgroup.center Ga:Gc:Gˣhc:↑c * a = w * ↑c⊢ w * ↑c = ↑c * w; exact (Subgroup.mem_center_iff.mp hw c).symmAll goals completed! 🐙
        exact mul_left_cancel thisAll goals completed! 🐙
      ·h.mprG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Gw:Ghw:w ∈ Subgroup.center Ga:G⊢ a = w → IsConj a w rintro rflh.mprG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Ga:Ghw:a ∈ Subgroup.center G⊢ IsConj a a
        exact IsConj.refl aAll goals completed! 🐙
    simp [conjClassCard, hset]All goals completed! 🐙
  -- Hence the class of any central `z` has the same size as the class of `1`, forcing `z = 1`.
  rw [Subgroup.eq_bot_iff_forall]G:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Ghcard:∀ w ∈ Subgroup.center G, conjClassCard (ConjClasses.mk w) = 1 := 
  fun w hw =>
    have hset :=
      Set.ext fun a =>
        Eq.mpr (id (congrArg (fun _a => _a ↔ a ∈ {w}) (propext mem_carrier_iff_mk_eq)))
          (Eq.mpr (id (congrArg (fun _a => _a ↔ a ∈ {w}) (propext mk_eq_mk_iff_isConj)))
            (Eq.mpr (id (congrArg (fun _a => IsConj a w ↔ _a) (propext Set.mem_singleton_iff)))
              {
                mp := fun a_1 =>
                  Exists.casesOn a_1 fun c hc =>
                    have this :=
                      Eq.mpr
                        (id
                          (congrArg (fun _a => _a = ↑c * w)
                            (Eq.mp (congrArg (fun _a => _a) (SemiconjBy.eq_1 (↑c) a w)) hc)))
                        (Eq.symm (Subgroup.mem_center_iff.mp hw ↑c));
                    mul_left_cancel this,
                mpr := fun a_1 =>
                  Eq.ndrec (motive := fun w => w ∈ Subgroup.center G → IsConj a w) (fun hw => IsConj.refl a) a_1 hw }));
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = 1)
          (Eq.trans (Eq.trans (congrArg (fun x => Nat.card ↑x) hset) Nat.card_eq_fintype_card) Fintype.card_unique))
        (eq_self 1))⊢ ∀ x ∈ Subgroup.center G, x = 1
  intro z hzG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Ghcard:∀ w ∈ Subgroup.center G, conjClassCard (ConjClasses.mk w) = 1 := 
  fun w hw =>
    have hset :=
      Set.ext fun a =>
        Eq.mpr (id (congrArg (fun _a => _a ↔ a ∈ {w}) (propext mem_carrier_iff_mk_eq)))
          (Eq.mpr (id (congrArg (fun _a => _a ↔ a ∈ {w}) (propext mk_eq_mk_iff_isConj)))
            (Eq.mpr (id (congrArg (fun _a => IsConj a w ↔ _a) (propext Set.mem_singleton_iff)))
              {
                mp := fun a_1 =>
                  Exists.casesOn a_1 fun c hc =>
                    have this :=
                      Eq.mpr
                        (id
                          (congrArg (fun _a => _a = ↑c * w)
                            (Eq.mp (congrArg (fun _a => _a) (SemiconjBy.eq_1 (↑c) a w)) hc)))
                        (Eq.symm (Subgroup.mem_center_iff.mp hw ↑c));
                    mul_left_cancel this,
                mpr := fun a_1 =>
                  Eq.ndrec (motive := fun w => w ∈ Subgroup.center G → IsConj a w) (fun hw => IsConj.refl a) a_1 hw }));
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = 1)
          (Eq.trans (Eq.trans (congrArg (fun x => Nat.card ↑x) hset) Nat.card_eq_fintype_card) Fintype.card_unique))
        (eq_self 1))z:Ghz:z ∈ Subgroup.center G⊢ z = 1
  have hz1 : ConjClasses.mk z = ConjClasses.mk 1 := byG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes G⊢ Subgroup.center G = ⊥
    apply haG:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Ghcard:∀ w ∈ Subgroup.center G, conjClassCard (ConjClasses.mk w) = 1 := 
  fun w hw =>
    have hset :=
      Set.ext fun a =>
        Eq.mpr (id (congrArg (fun _a => _a ↔ a ∈ {w}) (propext mem_carrier_iff_mk_eq)))
          (Eq.mpr (id (congrArg (fun _a => _a ↔ a ∈ {w}) (propext mk_eq_mk_iff_isConj)))
            (Eq.mpr (id (congrArg (fun _a => IsConj a w ↔ _a) (propext Set.mem_singleton_iff)))
              {
                mp := fun a_1 =>
                  Exists.casesOn a_1 fun c hc =>
                    have this :=
                      Eq.mpr
                        (id
                          (congrArg (fun _a => _a = ↑c * w)
                            (Eq.mp (congrArg (fun _a => _a) (SemiconjBy.eq_1 (↑c) a w)) hc)))
                        (Eq.symm (Subgroup.mem_center_iff.mp hw ↑c));
                    mul_left_cancel this,
                mpr := fun a_1 =>
                  Eq.ndrec (motive := fun w => w ∈ Subgroup.center G → IsConj a w) (fun hw => IsConj.refl a) a_1 hw }));
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = 1)
          (Eq.trans (Eq.trans (congrArg (fun x => Nat.card ↑x) hset) Nat.card_eq_fintype_card) Fintype.card_unique))
        (eq_self 1))z:Ghz:z ∈ Subgroup.center G⊢ conjClassCard (ConjClasses.mk z) = conjClassCard (ConjClasses.mk 1)
    rw [hcard z hz, hcard 1 (Subgroup.one_mem _)]All goals completed! 🐙
  rw [ConjClasses.mk_eq_mk_iff_isConj] at hz1G:Type u_1inst✝¹:Group Ginst✝:Fintype Gh:HasDistinctConjClassSizes Ghcard:∀ w ∈ Subgroup.center G, conjClassCard (ConjClasses.mk w) = 1 := 
  fun w hw =>
    have hset :=
      Set.ext fun a =>
        Eq.mpr (id (congrArg (fun _a => _a ↔ a ∈ {w}) (propext mem_carrier_iff_mk_eq)))
          (Eq.mpr (id (congrArg (fun _a => _a ↔ a ∈ {w}) (propext mk_eq_mk_iff_isConj)))
            (Eq.mpr (id (congrArg (fun _a => IsConj a w ↔ _a) (propext Set.mem_singleton_iff)))
              {
                mp := fun a_1 =>
                  Exists.casesOn a_1 fun c hc =>
                    have this :=
                      Eq.mpr
                        (id
                          (congrArg (fun _a => _a = ↑c * w)
                            (Eq.mp (congrArg (fun _a => _a) (SemiconjBy.eq_1 (↑c) a w)) hc)))
                        (Eq.symm (Subgroup.mem_center_iff.mp hw ↑c));
                    mul_left_cancel this,
                mpr := fun a_1 =>
                  Eq.ndrec (motive := fun w => w ∈ Subgroup.center G → IsConj a w) (fun hw => IsConj.refl a) a_1 hw }));
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = 1)
          (Eq.trans (Eq.trans (congrArg (fun x => Nat.card ↑x) hset) Nat.card_eq_fintype_card) Fintype.card_unique))
        (eq_self 1))z:Ghz:z ∈ Subgroup.center Ghz1:IsConj z 1⊢ z = 1
  exact isConj_one_right.mp hz1.symmAll goals completed! 🐙

The symmetric group $S_3$ is anti-homogeneous, since its three conjugacy classes have sizes $1$, $2$ and $3$.

@[category test, AMS 20]
theorem hasDistinctConjClassSizes_perm_fin_three :
    HasDistinctConjClassSizes (Equiv.Perm (Fin 3)) := by⊢ HasDistinctConjClassSizes (Equiv.Perm (Fin 3))
  have key : (conjClassCard (G := Equiv.Perm (Fin 3))) =
      fun c => c.carrier.toFinset.card := by⊢ HasDistinctConjClassSizes (Equiv.Perm (Fin 3))
    funext chc:ConjClasses (Equiv.Perm (Fin 3))⊢ conjClassCard c = c.carrier.toFinset.card
    rw [conjClassCard, Nat.card_eq_fintype_card, ← Set.toFinset_card]All goals completed! 🐙
  unfold HasDistinctConjClassSizeskey:conjClassCard = fun c => c.carrier.toFinset.card := 
  funext fun c =>
    Eq.mpr (id (congrArg (fun _a => _a = c.carrier.toFinset.card) (conjClassCard.eq_1 c)))
      (Eq.mpr (id (congrArg (fun _a => _a = c.carrier.toFinset.card) Nat.card_eq_fintype_card))
        (Eq.mpr (id (congrArg (fun _a => _a = c.carrier.toFinset.card) (Eq.symm (Set.toFinset_card c.carrier))))
          (Eq.refl c.carrier.toFinset.card)))⊢ Function.Injective conjClassCard
  rw [key]key:conjClassCard = fun c => c.carrier.toFinset.card := 
  funext fun c =>
    Eq.mpr (id (congrArg (fun _a => _a = c.carrier.toFinset.card) (conjClassCard.eq_1 c)))
      (Eq.mpr (id (congrArg (fun _a => _a = c.carrier.toFinset.card) Nat.card_eq_fintype_card))
        (Eq.mpr (id (congrArg (fun _a => _a = c.carrier.toFinset.card) (Eq.symm (Set.toFinset_card c.carrier))))
          (Eq.refl c.carrier.toFinset.card)))⊢ Function.Injective fun c => c.carrier.toFinset.card
  decideAll goals completed! 🐙

Markel's $S_3$-conjecture (1973): any nontrivial finite ah-group is isomorphic to $S_3$.

The conjecture is open in general; it is known to be true for solvable groups.

@[category research open, AMS 20]
theorem declaration uses 'sorry'conjClassSizes_iff_sym_three
    (G : Type) [Group G] [Fintype G] [Nontrivial G]
    (h : HasDistinctConjClassSizes (G := G)) :
    Nonempty (G ≃* Equiv.Perm (Fin 3)) := byG:Typeinst✝²:Group Ginst✝¹:Fintype Ginst✝:Nontrivial Gh:HasDistinctConjClassSizes G⊢ Nonempty (G ≃* Equiv.Perm (Fin 3))
  sorryAll goals completed! 🐙

The $S_3$-conjecture holds for solvable groups: every nontrivial solvable finite ah-group is isomorphic to $S_3$. This was proved independently by Zhang (1994) and by Knörr–Lempken–Thielcke (1995).

@[category research solved, AMS 20]
theorem declaration uses 'sorry'conjClassSizes_iff_sym_three_solvable
    (G : Type) [Group G] [Fintype G] [IsSolvable G] [Nontrivial G]
    (h : HasDistinctConjClassSizes (G := G)) :
    Nonempty (G ≃* Equiv.Perm (Fin 3)) := byG:Typeinst✝³:Group Ginst✝²:Fintype Ginst✝¹:IsSolvable Ginst✝:Nontrivial Gh:HasDistinctConjClassSizes G⊢ Nonempty (G ≃* Equiv.Perm (Fin 3))
  sorryAll goals completed! 🐙


end ConjugacyClassSizes