Finite images of minimax groups

DefinitionMaximal condition on subgroups#✓fully proved

A group \(G\) satisfies the maximal condition on subgroups when every subgroup of \(G\) is finitely generated.

def HasMaxCondition (G : Type*) [Group G] : Prop :=
  ∀ H : Subgroup G, H.FG

Used by 1

Used byMinimax groups

DefinitionMinimal condition on subgroups#✓fully proved

A group \(G\) satisfies the minimal condition on subgroups when the order on subgroups of \(G\) by inclusion is well-founded: every nonempty set of subgroups of \(G\) has a minimal element, equivalently there is no infinite strictly descending chain of subgroups of \(G\).

def HasMinCondition (G : Type*) [Group G] : Prop :=
  WellFoundedLT (Subgroup G)

Used by 1

Used byMinimax groups

DefinitionMinimax groups#✓fully proved

A group \(G\) is a minimax group when it has a finite subnormal series \(1 = H_0 \le H_1 \le \dots \le H_n = G\), with each \(H_i\) normal in \(H_{i+1}\), such that every factor \(H_{i+1}/H_i\) satisfies the maximal condition on subgroups or the minimal condition on subgroups.

def IsMinimax (G : Type*) [Group G] : Prop :=
  ∃ (n : ℕ) (H : Fin (n + 1) → Subgroup G), H 0 = ⊥ ∧ H (Fin.last n) = ⊤ ∧
    ∀ i : Fin n, H i.castSucc ≤ H i.succ ∧
      ∃ _ : ((H i.castSucc).subgroupOf (H i.succ)).Normal,
        HasMaxCondition (H i.succ ⧸ (H i.castSucc).subgroupOf (H i.succ)) ∨
          HasMinCondition (H i.succ ⧸ (H i.castSucc).subgroupOf (H i.succ))

Uses 2 · Used by 1

Statement usesMaximal condition on subgroups · Minimal condition on subgroups

Used byMinimax groups and finite images (Kourovka 12.90)

DefinitionGroups with the same finite images#✓fully proved

Two groups \(G\) and \(H\) have the same finite images when, for every finite group \(Q\), there is a surjective homomorphism \(G \to Q\) exactly when there is a surjective homomorphism \(H \to Q\).

def SameFiniteImages (G H : Type*) [Group G] [Group H] : Prop :=
  ∀ (Q : Type) [Group Q] [Finite Q],
    (∃ f : G →* Q, Function.Surjective f) ↔ (∃ f : H →* Q, Function.Surjective f)

Used by 1

Used byMinimax groups and finite images (Kourovka 12.90)

DefinitionResidually finite groups#✓fully proved

A group \(G\) is residually finite when for every element \(g \ne 1\) of \(G\) there is a normal subgroup \(N\) of finite index in \(G\) with \(g \notin N\).

def IsResiduallyFinite (G : Type*) [Group G] : Prop :=
  ∀ g : G, g ≠ 1 → ∃ N : Subgroup G, N.Normal ∧ N.FiniteIndex ∧ g ∉ N

Used by 1

Used byMinimax groups and finite images (Kourovka 12.90)

DefinitionMinimax groups and finite images (Kourovka 12.90)#✓fully proved

The statement that for all groups \(G\) and \(H\), if \(G\) is a finitely generated soluble minimax group and \(H\) is a finitely generated residually finite group with the same finite images as \(G\) (a finite group is a homomorphic image of \(G\) exactly when it is a homomorphic image of \(H\)), then \(H\) is a minimax group.

def minimaxDeterminedByFiniteImages : Prop :=
  ∀ (G H : Type) [Group G] [Group H], Group.FG G → Group.IsSolvable G → IsMinimax G →
    Group.FG H → IsResiduallyFinite H → SameFiniteImages G H → IsMinimax H

Uses 3 · Used by 1

Statement usesMinimax groups · Residually finite groups · Groups with the same finite images

Used byFinite images determine minimaxity (Mann–Segal)

TheoremFinite images determine minimaxity (Mann–Segal)#●ready to prove

Let \(G\) be a finitely generated soluble minimax group and let \(H\) be a finitely generated residually finite group with the same finite images as \(G\): a finite group is a homomorphic image of \(G\) exactly when it is a homomorphic image of \(H\). Then \(H\) is a minimax group.

This answers Kourovka Problem 12.90 (J. S. Wilson) affirmatively: the Kourovka Archive answers "Yes, it must" (A. Mann and D. Segal, 1990; see also A. V. Tushev, 1994).

public theorem_wanted minimaxDeterminedByFiniteImages_holds : minimaxDeterminedByFiniteImages

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.90 (J. S. Wilson); resolution: A. Mann and D. Segal, Proc. London Math. Soc. (3) 61 (1990), 529-545; A. V. Tushev, Math. Notes 56 (1994), no. 5, 1190-1192, Kourovka Archive, Problem 12.90: Yes, it must.

Uses 1

Statement usesMinimax groups and finite images (Kourovka 12.90)

6 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.