Surjections injective on no nontrivial subgroup

DefinitionKourovka Problem 17.50: surjections injective on no nontrivial subgroup#✓fully proved

The statement that for every finite group \(G\) there are a finite group \(F\) and a surjective homomorphism \(f \colon F \to G\) such that for every nontrivial subgroup \(H\) of \(F\) the restriction of \(f\) to \(H\) is not injective.

def surjectionNoninjectiveOnSubgroups : Prop :=
  ∀ (G : Type) [Group G] [Finite G], ∃ (F : Type) (_ : Group F) (_ : Finite F) (f : F →* G),
    Function.Surjective f ∧ ∀ H : Subgroup F, H ≠ ⊥ → ¬ Function.Injective (f.comp H.subtype)

Used by 1

Used byBurichenko's theorem on surjections injective on no nontrivial subgroup

TheoremBurichenko's theorem on surjections injective on no nontrivial subgroup#●ready to prove

For every finite group \(G\) there are a finite group \(F\) and a surjective homomorphism \(f \colon F \to G\) such that for every nontrivial subgroup \(H\) of \(F\) the restriction of \(f\) to \(H\) is not injective.

public theorem_wanted surjectionNoninjectiveOnSubgroups_holds : surjectionNoninjectiveOnSubgroups

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 17.50 (E. G. Zelenyuk); resolution: V. P. Burichenko, Math. Notes 92 (2012), 327-332, Kourovka Archive, Problem 17.50 (Yes, it is).

Uses 1

Statement usesKourovka Problem 17.50: surjections injective on no nontrivial subgroup

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.