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 = ⊤
def IsPronormal {G : Type} [Group G] (H : Subgroup G) : Prop :=
∀ g : G, ∃ x ∈ H ⊔ H.map (MulAut.conj g).toMonoidHom,
H.map (MulAut.conj x).toMonoidHom = H.map (MulAut.conj g).toMonoidHom
WantedExt/GroupTheory/HallMaximalPronormalSecondMaximalKourovka19Problem109Wanted.lean:44
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
def existsInfiniteGroupWithoutProperPronormal : Prop :=
∃ (G : Type) (_ : Group G), Infinite G ∧ ∀ H : Subgroup G, IsPronormal H → H = ⊥ ∨ H = ⊤
WantedExt/GroupTheory/NoProperPronormalSubgroupsKourovka19Problem74Wanted.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), 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.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.