Permutation characters

DefinitionComplex permutation character on the cosets of a subgroup#✓fully proved

For a subgroup \(H\) of a group \(G\), the permutation character \(1_H^G : G \to \mathbb{C}\) sends \(g \in G\) to the number of left cosets \(xH\) of \(H\) with \(gxH = xH\), and to \(0\) when \(g\) fixes infinitely many cosets. For finite \(G\) and the trivial subgroup \(H = 1\) this is the regular character \(1^G\).

noncomputable def permChar {G : Type*} [Group G] (H : Subgroup G) (g : G) : ℂ :=
  (Nat.card {q : G ⧸ H // g • q = q} : ℂ)

Used by 1

Used byStrunkov's class function

DefinitionStrunkov's class function#✓fully proved

For elements \(a, b\) of a group \(G\), Strunkov's function \(\varphi : G \to \mathbb{C}\) is

\[\varphi = 1^G - 1_{\langle a \rangle}^G - 1_{\langle b \rangle}^G - 1_{\langle ab \rangle}^G + 2\]

where \(1_H^G\) is the complex permutation character of \(G\) on the cosets of a subgroup \(H\), \(1^G = 1_1^G\) is the one for the trivial subgroup, \(\langle x \rangle\) is the cyclic subgroup generated by \(x\), and \(2\) is the constant function with value \(2\).

noncomputable def strunkovFunction {G : Type*} [Group G] (a b : G) (g : G) : ℂ :=
  permChar ⊥ g - permChar (Subgroup.zpowers a) g - permChar (Subgroup.zpowers b) g -
    permChar (Subgroup.zpowers (a * b)) g + 2

Uses 1 · Used by 1

Statement usesComplex permutation character on the cosets of a subgroup

Used byStrunkov's two-generation criterion (Kourovka 12.79)

DefinitionCharacters of a group#✓fully proved

A function \(\varphi : G \to \mathbb{C}\) on a group \(G\) is a character of \(G\) when there are a finite-dimensional complex vector space \(V\) and a representation \(\rho\) of \(G\) on \(V\) whose character \(g \mapsto \operatorname{tr} \rho(g)\) equals \(\varphi\).

def IsCharacter {G : Type} [Group G] (φ : G → ℂ) : Prop :=
  ∃ (V : Type) (_ : AddCommGroup V) (_ : Module ℂ V) (_ : FiniteDimensional ℂ V)
    (ρ : Representation ℂ G V), ρ.character = φ

Used by 1

Used byStrunkov's two-generation criterion (Kourovka 12.79)

DefinitionStrunkov's two-generation criterion (Kourovka 12.79)#✓fully proved

The assertion that for every finite group \(G\) and all \(a, b \in G\), if Strunkov's class function \(1^G - 1_{\langle a \rangle}^G - 1_{\langle b \rangle}^G - 1_{\langle ab \rangle}^G + 2\) is a character of \(G\), then \(a\) and \(b\) generate \(G\). Here \(1_H^G\) is the permutation character of \(G\) on the cosets of a subgroup \(H\), \(1^G = 1_1^G\), \(\langle x \rangle\) is the cyclic subgroup generated by \(x\), and \(2\) is the constant function with value \(2\).

def strunkovCharacterImpliesGeneration : Prop :=
  ∀ (G : Type) [Group G] [Finite G] (a b : G), IsCharacter (strunkovFunction a b) →
    Subgroup.closure {a, b} = ⊤

Uses 2 · Used by 1

Statement usesCharacters of a group · Strunkov's class function

Used byStrunkov's two-generation criterion fails (Kourovka 12.79)

TheoremStrunkov's two-generation criterion fails (Kourovka 12.79)#●ready to prove

It is not true that for every finite group \(G\) and all \(a, b \in G\) such that Strunkov's class function \(1^G - 1_{\langle a \rangle}^G - 1_{\langle b \rangle}^G - 1_{\langle ab \rangle}^G + 2\) is a character of \(G\), the elements \(a\) and \(b\) generate \(G\). Here \(1_H^G\) is the permutation character of \(G\) on the cosets of a subgroup \(H\), \(1^G = 1_1^G\), \(\langle x \rangle\) is the cyclic subgroup generated by \(x\), and \(2\) is the constant function with value \(2\).

Counterexample (S. V. Skresanov, 2019): \(G = A_4\) and \(a = b = (1\,2\,3)\). The function takes the values \(2, 2, -1, -1\) on the classes of \(1\), \((1\,2)(3\,4)\), \((1\,2\,3)\), \((1\,3\,2)\), so it is the sum of the two nontrivial linear characters of \(A_4\), while \(\langle a, b \rangle\) has order \(3\).

public theorem_wanted strunkovCharacterImpliesGeneration_refuted :
    ¬ strunkovCharacterImpliesGeneration

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 12.79 (S. P. Strunkov); resolution: S. V. Skresanov, Algebra Logic 58 (2019), no. 3, 249-253, Kourovka Archive, Problem 12.79: No, not always; counterexample G = A_4, a = b = (123).

Uses 1

Statement usesStrunkov's two-generation criterion (Kourovka 12.79)

DefinitionRational permutation character on the cosets of a subgroup#✓fully proved

For a subgroup \(H\) of a group \(G\), the permutation character \(1_H^G : G \to \mathbb{Q}\) sends \(g \in G\) to the number of left cosets \(xH\) of \(H\) with \(gxH = xH\), and to \(0\) when \(g\) fixes infinitely many cosets.

noncomputable def permChar {G : Type*} [Group G] (H : Subgroup G) (g : G) : ℚ :=
  Nat.card {c : G ⧸ H // g • c = c}

Used by 1

Used byFinite insoluble groups with independent permutation characters (Kourovka 11.9)

DefinitionFinite insoluble groups with independent permutation characters (Kourovka 11.9)#✓fully proved

The assertion that there is a finite non-soluble group \(G\) such that, choosing a representative \(H\) of each conjugacy class of subgroups of \(G\), the rational-valued permutation characters \(1_H^G\) of \(G\) on the left cosets of these subgroups \(H\) are linearly independent over \(\mathbb{Q}\).

def insolubleIndependentPermutationCharacters : Prop :=
  ∃ (G : Type) (_ : Group G) (_ : Finite G), ¬ Group.IsSolvable G ∧
    LinearIndependent ℚ fun c : MulAction.orbitRel.Quotient (ConjAct G) (Subgroup G) =>
      permChar (Quotient.out c)

Uses 1 · Used by 1

Statement usesRational permutation character on the cosets of a subgroup

Used byNo insoluble group has independent permutation characters (Kourovka 11.9)

TheoremNo insoluble group has independent permutation characters (Kourovka 11.9)#●ready to prove

There is no finite non-soluble group \(G\) such that, choosing a representative \(H\) of each conjugacy class of subgroups of \(G\), the rational-valued permutation characters \(1_H^G\) of \(G\) on the left cosets of these subgroups \(H\) are linearly independent over \(\mathbb{Q}\).

Brescia, Ingrosso and Trombetti prove that these permutation characters are linearly independent if and only if \(G\) is cyclic; the Kourovka Notebook (21st issue) marks 11.9 solved, "No, there are no such groups".

public theorem_wanted insolubleIndependentPermutationCharacters_refuted :
    ¬ insolubleIndependentPermutationCharacters

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 11.9 (Ya. G. Berkovich); resolution: M. Brescia, E. Ingrosso and M. Trombetti, On the independence of permutation characters, arXiv:2608.16957 (2026), main theorem: the characters π_H, H over representatives of the conjugacy classes of subgroups, are linearly independent iff G is cyclic; the Kourovka Notebook (21st issue) marks 11.9 solved, https://arxiv.org/abs/2608.16957.

Uses 1

Statement usesFinite insoluble groups with independent permutation characters (Kourovka 11.9)

6 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.