Groups with Hall maximal subgroups

DefinitionHall subgroup (Kourovka Problem 19.109)#✓fully proved

A subgroup \(H\) of a group \(G\) is a Hall subgroup when its order \(|H|\) is coprime to its index \(|G : H|\), where an infinite order or index is counted as \(0\).

def IsHallSubgroup {G : Type} [Group G] (H : Subgroup G) : Prop :=
  (Nat.card H).Coprime H.index

Used by 1

Used byZenkov's question on Hall maximal subgroups (Kourovka Problem 19.109)

DefinitionPronormal subgroup#✓fully proved

A subgroup \(H\) of a group \(G\) is pronormal in \(G\) when for every \(g \in G\) there is an element \(x\) of the subgroup \(\langle H, gHg^{-1} \rangle\) generated by \(H\) and \(gHg^{-1}\) such that \(xHx^{-1} = gHg^{-1}\).

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

Used by 2

Used byInfinite groups without nontrivial proper pronormal subgroups (Kourovka 19.74, Revin) · Zenkov's question on Hall maximal subgroups (Kourovka Problem 19.109)

DefinitionSecond maximal subgroup#✓fully proved

A subgroup \(K\) of a group \(G\) is second maximal when it is a maximal subgroup of a maximal subgroup of \(G\): there is a maximal subgroup \(M\) of \(G\) with \(K < M\) and no subgroup \(L\) of \(G\) with \(K < L < M\).

def IsSecondMaximal {G : Type} [Group G] (K : Subgroup G) : Prop :=
  ∃ M : Subgroup G, IsCoatom M ∧ K < M ∧ ∀ L : Subgroup G, K < L → ¬ L < M

Used by 1

Used byZenkov's question on Hall maximal subgroups (Kourovka Problem 19.109)

DefinitionZenkov's question on Hall maximal subgroups (Kourovka Problem 19.109)#✓fully proved

For every non-abelian finite simple group \(G\), all maximal subgroups of \(G\) are Hall subgroups if and only if every second maximal subgroup of \(G\) is pronormal in \(G\).

def maximalHallIffSecondMaximalPronormal : Prop :=
  ∀ (G : Type) [Group G] [Finite G], IsSimpleGroup G → (∃ a b : G, a * b ≠ b * a) →
    ((∀ M : Subgroup G, IsCoatom M → IsHallSubgroup M) ↔
      ∀ K : Subgroup G, IsSecondMaximal K → IsPronormal K)

Uses 3 · Used by 1

Statement usesHall subgroup (Kourovka Problem 19.109) · Pronormal subgroup · Second maximal subgroup

Used byNegative answer to Zenkov's question (Kourovka Problem 19.109)

TheoremNegative answer to Zenkov's question (Kourovka Problem 19.109)#●ready to prove

It is not true that for every non-abelian finite simple group \(G\), all maximal subgroups of \(G\) are Hall subgroups if and only if every second maximal subgroup of \(G\) is pronormal in \(G\).

The group \(\mathrm{SL}_2(2^{11})\), in which every second maximal subgroup is pronormal (V. N. Tyutyanov, 2018), is a counterexample.

public theorem_wanted maximalHallIffSecondMaximalPronormal_refuted :
    ¬ maximalHallIffSecondMaximalPronormal

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 19.109 (V. I. Zenkov); resolution: V. N. Tyutyanov, letter of 23 November 2018, as recorded in the Kourovka Archive, Kourovka Archive, Problem 19.109: No, not always; in SL_2(2^11) every second maximal subgroup is pronormal, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesZenkov's question on Hall maximal subgroups (Kourovka Problem 19.109)

DefinitionHall subgroup (Kourovka 17.92)#✓fully proved

A subgroup \(H\) of a group \(G\) is a Hall subgroup when its order \(|H|\) is coprime to its index \(|G : H|\).

Here \(|H|\) and \(|G : H|\) are natural numbers, taken to be \(0\) when infinite.

def IsHallSubgroup {G : Type*} [Group G] (H : Subgroup G) : Prop :=
  Nat.Coprime (Nat.card H) H.index

Used by 1

Used byNon-soluble groups with Hall maximal subgroups

DefinitionComposition factor of a group (Kourovka 17.92)#✓fully proved

For groups \(G\) and \(S\), \(S\) is a composition factor of \(G\) when there are subgroups \(H\) and \(K\) of \(G\) such that \(H\) is subnormal in \(G\), \(H \cap K\) is normal in \(H\), and the quotient \(H/(H \cap K)\) is a simple group isomorphic to \(S\).

def IsCompositionFactor (G S : Type*) [Group G] [Group S] : Prop :=
  ∃ (H K : Subgroup G) (_ : (K.subgroupOf H).Normal), H.IsSubnormal ∧
    IsSimpleGroup (H ⧸ K.subgroupOf H) ∧ Nonempty (H ⧸ K.subgroupOf H ≃* S)

Used by 2

Used byKourovka 17.92, first half: the possible composition factors · Kourovka 17.92, second half: the three factors occur

DefinitionNon-soluble groups with Hall maximal subgroups#✓fully proved

A group \(G\) has this property when \(G\) is not soluble and every maximal subgroup of \(G\) is a Hall subgroup.

def IsMaximalHallNonsoluble (G : Type*) [Group G] : Prop :=
  ¬ Group.IsSolvable G ∧ ∀ M : Subgroup G, IsCoatom M → IsHallSubgroup M

Uses 1 · Used by 2

Statement usesHall subgroup (Kourovka 17.92)

Used byKourovka 17.92, first half: the possible composition factors · Kourovka 17.92, second half: the three factors occur

DefinitionKourovka 17.92, first half: the possible composition factors#✓fully proved

The proposition that every non-abelian composition factor of a finite non-soluble group all of whose maximal subgroups are Hall subgroups is isomorphic to \(L_2(7)\), \(L_2(11)\) or \(L_5(2)\). Here \(L_n(q)\) is the projective special linear group \(\mathrm{PSL}_n(\mathbb{Z}/q\mathbb{Z})\), the quotient of \(\mathrm{SL}_n(\mathbb{Z}/q\mathbb{Z})\) by its centre.

def maximalHallCompositionFactorsInList : Prop :=
  ∀ (G : Type) [Group G] [Finite G], IsMaximalHallNonsoluble G →
    ∀ (S : Type) [Group S], IsCompositionFactor G S → (∃ a b : S, a * b ≠ b * a) →
      Nonempty (S ≃* Matrix.ProjectiveSpecialLinearGroup (Fin 2) (ZMod 7)) ∨
        Nonempty (S ≃* Matrix.ProjectiveSpecialLinearGroup (Fin 2) (ZMod 11)) ∨
        Nonempty (S ≃* Matrix.ProjectiveSpecialLinearGroup (Fin 5) (ZMod 2))

Uses 2 · Used by 1

Statement usesComposition factor of a group (Kourovka 17.92) · Non-soluble groups with Hall maximal subgroups

Used byMaslova's theorem on groups with Hall maximal subgroups

DefinitionKourovka 17.92, second half: the three factors occur#✓fully proved

The proposition that each of \(L_2(7)\), \(L_2(11)\) and \(L_5(2)\) is a composition factor of some finite non-soluble group all of whose maximal subgroups are Hall subgroups. Here \(L_n(q)\) is the projective special linear group \(\mathrm{PSL}_n(\mathbb{Z}/q\mathbb{Z})\), the quotient of \(\mathrm{SL}_n(\mathbb{Z}/q\mathbb{Z})\) by its centre.

def maximalHallCompositionFactorsOccur : Prop :=
  (∃ (G : Type) (_ : Group G) (_ : Finite G), IsMaximalHallNonsoluble G ∧
      IsCompositionFactor G (Matrix.ProjectiveSpecialLinearGroup (Fin 2) (ZMod 7))) ∧
    (∃ (G : Type) (_ : Group G) (_ : Finite G), IsMaximalHallNonsoluble G ∧
      IsCompositionFactor G (Matrix.ProjectiveSpecialLinearGroup (Fin 2) (ZMod 11))) ∧
    (∃ (G : Type) (_ : Group G) (_ : Finite G), IsMaximalHallNonsoluble G ∧
      IsCompositionFactor G (Matrix.ProjectiveSpecialLinearGroup (Fin 5) (ZMod 2)))

Uses 2 · Used by 1

Statement usesComposition factor of a group (Kourovka 17.92) · Non-soluble groups with Hall maximal subgroups

Used byThe three answer groups of Kourovka 17.92 occur

TheoremMaslova's theorem on groups with Hall maximal subgroups#●ready to prove

Every non-abelian composition factor of a finite non-soluble group all of whose maximal subgroups are Hall subgroups is isomorphic to \(L_2(7)\), \(L_2(11)\) or \(L_5(2)\), so the first half of the answer to Kourovka 17.92 holds. Here \(L_n(q)\) is the projective special linear group \(\mathrm{PSL}_n(\mathbb{Z}/q\mathbb{Z})\), the quotient of \(\mathrm{SL}_n(\mathbb{Z}/q\mathbb{Z})\) by its centre.

Maslova (2012) proved this; the Kourovka Archive gives these three groups as the answer to 17.92.

public theorem_wanted maximalHallCompositionFactorsInList_holds :
    maximalHallCompositionFactorsInList

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.92 (V. S. Monakhov); resolution: N. V. Maslova, Siberian Math. J. 53 (2012), 853-861; N. V. Maslova and D. O. Revin, Finite groups whose maximal subgroups have the Hall property, Siberian Adv. Math. 23 (2013), no. 3, Maslova-Revin, Introduction (by Levchuk-Likharev and Tyutyanov, L_2(7), L_2(11) and L_5(2) are groups all of whose maximal subgroups are Hall; by Maslova (2012) every non-abelian composition factor of such a group is one of them, so the three groups exhaust the non-abelian composition factors); Kourovka Archive, Problem 17.92 (Answer: L_2(7), L_2(11), L_5(2)), https://doi.org/10.3103/S105513441303005X.

Uses 1

Statement usesKourovka 17.92, first half: the possible composition factors

TheoremThe three answer groups of Kourovka 17.92 occur#●ready to prove

Each of \(L_2(7)\), \(L_2(11)\) and \(L_5(2)\) is a composition factor of some finite non-soluble group all of whose maximal subgroups are Hall subgroups, so the second half of the answer to Kourovka 17.92 holds. Here \(L_n(q)\) is the projective special linear group \(\mathrm{PSL}_n(\mathbb{Z}/q\mathbb{Z})\), the quotient of \(\mathrm{SL}_n(\mathbb{Z}/q\mathbb{Z})\) by its centre.

Each of the three groups is itself non-soluble with all of its maximal subgroups Hall (Levchuk-Likharev, Tyutyanov, as recalled by Maslova and Revin); with Maslova's theorem the three groups are exactly the non-abelian composition factors.

public theorem_wanted maximalHallCompositionFactorsOccur_holds : maximalHallCompositionFactorsOccur

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.92 (V. S. Monakhov); resolution: N. V. Maslova, Siberian Math. J. 53 (2012), 853-861; N. V. Maslova and D. O. Revin, Finite groups whose maximal subgroups have the Hall property, Siberian Adv. Math. 23 (2013), no. 3, Maslova-Revin, Introduction (by Levchuk-Likharev and Tyutyanov, L_2(7), L_2(11) and L_5(2) are groups all of whose maximal subgroups are Hall; by Maslova (2012) every non-abelian composition factor of such a group is one of them, so the three groups exhaust the non-abelian composition factors); Kourovka Archive, Problem 17.92 (Answer: L_2(7), L_2(11), L_5(2)), https://doi.org/10.3103/S105513441303005X.

Uses 1

Statement usesKourovka 17.92, second half: the three factors occur

9 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.