Regular orbits of linear groups
DefinitionZhang's question on regular orbits from \(p\)-regular orbits#✓fully proved
The statement that for every finite field \(F\), every nonzero finite-dimensional vector space \(V\) over \(F\) and every finite group \(G\) acting faithfully on \(V\) by \(F\)-linear maps, if the only \(G\)-invariant subspaces of \(V\) are \(0\) and \(V\), and for every prime \(p\) some vector of \(V\) has a stabilizer in \(G\) of order prime to \(p\) (a \(p\)-regular orbit), then some vector of \(V\) has trivial stabilizer in \(G\) (a regular orbit).
This is Kourovka Notebook Problem 12.25 (Jiping Zhang).
def pRegularOrbitsImplyRegularOrbit : Prop :=
∀ (F : Type) [Field F] [Finite F] (V : Type) [AddCommGroup V] [Module F V]
[FiniteDimensional F V] [Nontrivial V] (G : Type) [Group G] [Finite G]
[DistribMulAction G V] [SMulCommClass G F V], FaithfulSMul G V →
(∀ W : Submodule F V, (∀ g : G, ∀ v ∈ W, g • v ∈ W) → W = ⊥ ∨ W = ⊤) →
(∀ p : ℕ, p.Prime → ∃ v : V, (Nat.card (MulAction.stabilizer G v)).Coprime p) →
∃ v : V, MulAction.stabilizer G v = ⊥Used by 1
Theorem\(p\)-regular orbits for every prime do not force a regular orbit#●ready to prove
There exist a finite field \(F\), a nonzero finite-dimensional vector space \(V\) over \(F\) and a finite group \(G\) acting faithfully on \(V\) by \(F\)-linear maps such that the only \(G\)-invariant subspaces of \(V\) are \(0\) and \(V\) and, for every prime \(p\), some vector of \(V\) has a stabilizer in \(G\) of order prime to \(p\), but no vector of \(V\) has trivial stabilizer in \(G\).
Resolved false: the Kourovka Archive answers 12.25 "No, not always" (V. I. Zenkov). Write \(\mathbb{Z}_n\) for the cyclic group of order \(n\), \(A_4\) for the alternating group of degree \(4\) and \(\mathbb{F}_2\) for the field with two elements. Let \(H = A_4 \wr \mathbb{Z}_5\) be the wreath product, let \(V = O_2(H)\) be the largest normal \(2\)-subgroup of \(H\), so \(V \cong \mathbb{F}_2^{10}\), and let \(G \cong \mathbb{Z}_3 \wr \mathbb{Z}_5\) be a complement to \(V\) in \(H\). The faithful irreducible action of \(G\) on \(V\) by conjugation has orbits with stabilizers of order \(5\) and of order \(3\), hence \(p\)-regular orbits for every prime \(p\), but no regular orbit, since \(|G| = 1215 > 1024 = |V|\).
public theorem_wanted pRegularOrbitsImplyRegularOrbit_refuted : ¬ pRegularOrbitsImplyRegularOrbitdef pRegularOrbitsImplyRegularOrbit : Prop :=
∀ (F : Type) [Field F] [Finite F] (V : Type) [AddCommGroup V] [Module F V]
[FiniteDimensional F V] [Nontrivial V] (G : Type) [Group G] [Finite G]
[DistribMulAction G V] [SMulCommClass G F V], FaithfulSMul G V →
(∀ W : Submodule F V, (∀ g : G, ∀ v ∈ W, g • v ∈ W) → W = ⊥ ∨ W = ⊤) →
(∀ p : ℕ, p.Prime → ∃ v : V, (Nat.card (MulAction.stabilizer G v)).Coprime p) →
∃ v : V, MulAction.stabilizer G v = ⊥WantedExt/GroupTheory/PRegularOrbitsRegularOrbitKourovka12Problem25Wanted.lean:45
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.25 (Jiping Zhang); resolution: V. I. Zenkov, letter of 11 February 1994, as recorded in the Kourovka Archive, Problem 12.25, Archive answer: No, not always; H = A_4 ≀ Z_5, V = O_2(H), G a complement to V acting by conjugation, https://arxiv.org/abs/1401.0300v49.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.