Frattini and complemented chief factors

DefinitionFrattini chief factor#✓fully proved

For subgroups \(A\) and \(B\) of a group \(G\), \(A/B\) is a Frattini chief factor of \(G\) when \(A/B\) is a chief factor of \(G\) and \(A\) is contained in every maximal subgroup of \(G\) that contains \(B\); equivalently, \(A/B \le \Phi(G/B)\), where \(\Phi\) denotes the Frattini subgroup.

def IsFrattiniChiefFactor {G : Type*} [Group G] (A B : Subgroup G) : Prop :=
  IsChiefFactor A B ∧ ∀ M : Subgroup G, IsCoatom M → B ≤ M → A ≤ M

Uses 1 · Used by 1

Statement usesChief factors

Used byKourovka Problem 19.38

DefinitionComplemented chief factor#✓fully proved

For subgroups \(A\) and \(B\) of a group \(G\), \(A/B\) is a complemented chief factor of \(G\) when \(A/B\) is a chief factor of \(G\) and some subgroup \(M\) of \(G\) satisfies \(\langle M, A \rangle = G\) and \(M \cap A = B\) (as \(A\) is normal, the first condition says \(MA = G\)).

def IsComplementedChiefFactor {G : Type*} [Group G] (A B : Subgroup G) : Prop :=
  IsChiefFactor A B ∧ ∃ M : Subgroup G, M ⊔ A = ⊤ ∧ M ⊓ A = B

Uses 1 · Used by 1

Statement usesChief factors

Used byKourovka Problem 19.38

DefinitionKourovka Problem 19.38#✓fully proved

The statement that for every finite soluble group \(G\) and every subgroup \(H\) of \(G\) that covers every Frattini chief factor \(A/B\) of \(G\), that is, \(A \le \langle H, B \rangle\) (which is \(HB\), as \(B\) is normal), and avoids every complemented chief factor \(A/B\) of \(G\), that is, \(H \cap A \le B\), there are \(x, y \in G\) such that \(H \cap H^x \cap H^y = H_G\), where \(H^x = xHx^{-1}\) and \(H_G\) is the normal core of \(H\), the largest normal subgroup of \(G\) contained in \(H\).

def coverAvoidTripleIntersectionCore : Prop :=
  ∀ (G : Type) [Group G] [Finite G], Group.IsSolvable G → ∀ H : Subgroup G,
    (∀ A B : Subgroup G, IsFrattiniChiefFactor A B → A ≤ H ⊔ B) →
    (∀ A B : Subgroup G, IsComplementedChiefFactor A B → H ⊓ A ≤ B) →
    ∃ x y : G, H ⊓ H.map (MulAut.conj x).toMonoidHom ⊓ H.map (MulAut.conj y).toMonoidHom =
      H.normalCore

Uses 2 · Used by 1

Statement usesComplemented chief factor · Frattini chief factor

Used byKamornikov–Shemetkova theorem (Kourovka Problem 19.38)

TheoremKamornikov–Shemetkova theorem (Kourovka Problem 19.38)#●ready to prove

Let \(H\) be a subgroup of a finite soluble group \(G\). Suppose that \(H\) covers every Frattini chief factor \(A/B\) of \(G\), that is, \(A \le \langle H, B \rangle\) (which is \(HB\), as \(B\) is normal), and avoids every complemented chief factor \(A/B\) of \(G\), that is, \(H \cap A \le B\). Then there are \(x, y \in G\) such that \(H \cap H^x \cap H^y = H_G\), where \(H^x = xHx^{-1}\) and \(H_G\) is the normal core of \(H\), the largest normal subgroup of \(G\) contained in \(H\).

public theorem_wanted coverAvoidTripleIntersectionCore_holds : coverAvoidTripleIntersectionCore

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.38 (S. F. Kamornikov); resolution: S. F. Kamornikov and O. L. Shemetkova, On a question concerning the intersection of Φ-isolators of finite soluble groups, J. Algebra 641 (2024), 1-8, doi:10.1016/j.jalgebra.2023.11.029, the Kourovka Notebook (21st issue) marks 19.38 solved: Yes, it is true, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesKourovka Problem 19.38

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.