Simply reducible groups

DefinitionSimply reducible group#✓fully proved

A group \(G\) is simply reducible when the character of every irreducible finite-dimensional complex representation of \(G\) is real-valued, and for all irreducible finite-dimensional complex representations \(U\), \(V\) and \(W\) of \(G\), the space \(\mathrm{Hom}_G(U, V \otimes W)\) of \(G\)-equivariant linear maps from \(U\) to the tensor product \(V \otimes W\) has complex dimension at most \(1\).

For finite \(G\), by Maschke's and Schur's theorems this dimension is the multiplicity of \(U\) in \(V \otimes W\), so the second condition says that \(V \otimes W\) has no repeated irreducible constituents.

def IsSimplyReducible (G : Type) [Group G] : Prop :=
  (∀ V : FDRep ℂ G, Simple V → ∀ g : G, (V.character g).im = 0) ∧
    ∀ V W U : FDRep ℂ G, Simple V → Simple W → Simple U → Module.finrank ℂ (U ⟶ V ⊗ W) ≤ 1
Used by 1

DefinitionSolubility of finite simply reducible groups (Kourovka 11.94)#✓fully proved

The statement, asked by S. P. Strunkov as Kourovka Problem 11.94, that every finite simply reducible group is soluble.

def simplyReducibleSoluble : Prop :=
  ∀ (G : Type) [Group G] [Finite G], IsSimplyReducible G → Group.IsSolvable G
Uses 1 · Used by 1

TheoremFinite simply reducible groups are soluble#●ready to prove

Every finite simply reducible group is soluble; that is, the statement of Kourovka Problem 11.94 holds.

This was proved by Kazarin and Chankov; the Kourovka Archive answers 11.94 "Yes, it is".

public theorem_wanted simplyReducibleSoluble_holds : simplyReducibleSoluble
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 11.94 (S. P. Strunkov); resolution: L. S. Kazarin and E. I. Chankov, Sb. Math. 201, no. 5 (2010), 655-668, Kourovka Archive, Problem 11.94: "Yes, it is", https://arxiv.org/abs/1401.0300v49.
Uses 1
2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.