Pronormal subgroups

DefinitionInfinite groups without nontrivial proper pronormal subgroups (Kourovka 19.74, Revin)#✓fully proved

The statement that there is an infinite group \(G\) in which every pronormal subgroup is trivial or equal to \(G\). Here a subgroup \(H\) of \(G\) is pronormal when, for every \(g \in G\), the subgroups \(H\) and \(H^g = gHg^{-1}\) are conjugate by an element of \(\langle H, H^g \rangle\).

def existsInfiniteGroupWithoutProperPronormal : Prop :=
  ∃ (G : Type) (_ : Group G), Infinite G ∧ ∀ H : Subgroup G, IsPronormal H → H = ⊥ ∨ H = ⊤
Uses 1 · Used by 1

TheoremAn infinite group without nontrivial proper pronormal subgroups exists#●ready to prove

There is an infinite group \(G\) in which every pronormal subgroup is trivial or equal to \(G\). Here a subgroup \(H\) of \(G\) is pronormal when, for every \(g \in G\), the subgroups \(H\) and \(H^g = gHg^{-1}\) are conjugate by an element of \(\langle H, H^g \rangle\). This answers Kourovka Problem 19.74 in the affirmative.

Corson constructs an infinite simple group with no proper abnormal subgroup, which the problem states is equivalent (the normalizer of a pronormal subgroup is abnormal); the 21st issue of the Kourovka Notebook marks 19.74 solved ("Yes, it does").

public theorem_wanted existsInfiniteGroupWithoutProperPronormal_holds :
    existsInfiniteGroupWithoutProperPronormal
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 19.74 (D. O. Revin); resolution: S. M. Corson, Infinite simple groups with no proper abnormal subgroups, Monatsh. Math. (2025), doi:10.1007/s00605-025-02116-8 (arXiv:2505.07330), Theorem 1: there is an infinite group that is simple, torsion-free, has no maximal subgroup and has no proper abnormal subgroup, answering Revin's problem; the Kourovka Notebook (21st issue) marks 19.74 solved: Yes, it does (the problem states the equivalent form: an infinite simple group without proper abnormal subgroups), https://arxiv.org/abs/2505.07330.
Uses 1
1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.