Supplements of maximal subgroups of Sylow subgroups

Definition\(p\)-soluble groups (series with \(p\)- and \(p'\)-factors)#✓fully proved

A group \(G\) is \(p\)-soluble when it has a chain of subgroups \(1 = H_0 \le H_1 \le \cdots \le H_n = G\), each normal in the next, such that for every \(i < n\) the relative index \(|H_{i+1} : H_i|\) (taken to be \(0\) when it is infinite) is a power of \(p\) or is coprime to \(p\). For a finite group this says that every factor \(H_{i+1}/H_i\) is a \(p\)-group or a \(p'\)-group.

def IsPSoluble (p : ℕ) (G : Type*) [Group G] : Prop :=
  ∃ (n : ℕ) (H : Fin (n + 1) → Subgroup G), H 0 = ⊥ ∧ H (Fin.last n) = ⊤ ∧
    ∀ i : Fin n, H i.castSucc ≤ H i.succ ∧ ((H i.castSucc).subgroupOf (H i.succ)).Normal ∧
      ((∃ k : ℕ, (H i.castSucc).relIndex (H i.succ) = p ^ k) ∨
        Nat.Coprime ((H i.castSucc).relIndex (H i.succ)) p)

Used by 1

Used byKourovka Problem 17.111 (supplements of maximal subgroups of Sylow subgroups)

DefinitionKourovka Problem 17.111 (supplements of maximal subgroups of Sylow subgroups)#✓fully proved

The statement, asked by A. N. Skiba, that for every prime \(p\), every finite group \(G\) whose order is divisible by \(p\) and every Sylow \(p\)-subgroup \(P\) of \(G\), if every maximal subgroup \(M\) of \(P\) has a \(p\)-soluble supplement in \(G\), that is, a \(p\)-soluble subgroup \(K\) of \(G\) with \(MK = G\), then \(G\) is \(p\)-soluble.

def sylowMaximalSupplementPSoluble : Prop :=
  ∀ (p : ℕ) (G : Type) [Group G] [Finite G], p.Prime → p ∣ Nat.card G → ∀ P : Sylow p G,
    (∀ M : Subgroup G, M < P → (∀ L : Subgroup G, M < L → L ≤ P → L = P) →
      ∃ K : Subgroup G, IsPSoluble p K ∧ ∀ g : G, ∃ m ∈ M, ∃ k ∈ K, m * k = g) →
    IsPSoluble p G

def IsPSoluble (p : ℕ) (G : Type*) [Group G] : Prop :=
  ∃ (n : ℕ) (H : Fin (n + 1) → Subgroup G), H 0 = ⊥ ∧ H (Fin.last n) = ⊤ ∧
    ∀ i : Fin n, H i.castSucc ≤ H i.succ ∧ ((H i.castSucc).subgroupOf (H i.succ)).Normal ∧
      ((∃ k : ℕ, (H i.castSucc).relIndex (H i.succ) = p ^ k) ∨
        Nat.Coprime ((H i.castSucc).relIndex (H i.succ)) p)

WantedExt/GroupTheory/SylowMaximalPSolubleSupplementKourovka17Problem111Wanted.lean:41

Uses 1 · Used by 1

Statement uses\(p\)-soluble groups (series with \(p\)- and \(p'\)-factors)

Used by\(p\)-soluble supplements of maximal subgroups of a Sylow subgroup force \(p\)-solubility

Theorem\(p\)-soluble supplements of maximal subgroups of a Sylow subgroup force \(p\)-solubility#●ready to prove

Let \(p\) be a prime, \(G\) a finite group whose order is divisible by \(p\), and \(P\) a Sylow \(p\)-subgroup of \(G\). If every maximal subgroup \(M\) of \(P\) has a \(p\)-soluble supplement in \(G\), that is, a \(p\)-soluble subgroup \(K\) of \(G\) with \(MK = G\), then \(G\) is \(p\)-soluble.

public theorem_wanted sylowMaximalSupplementPSoluble_holds : sylowMaximalSupplementPSoluble

def sylowMaximalSupplementPSoluble : Prop :=
  ∀ (p : ℕ) (G : Type) [Group G] [Finite G], p.Prime → p ∣ Nat.card G → ∀ P : Sylow p G,
    (∀ M : Subgroup G, M < P → (∀ L : Subgroup G, M < L → L ≤ P → L = P) →
      ∃ K : Subgroup G, IsPSoluble p K ∧ ∀ g : G, ∃ m ∈ M, ∃ k ∈ K, m * k = g) →
    IsPSoluble p G

WantedExt/GroupTheory/SylowMaximalPSolubleSupplementKourovka17Problem111Wanted.lean:50

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.111 (A. N. Skiba); resolution: GuoHua Qian, Science China Math. 56 (2013), 1015-1018, Kourovka Archive, Problem 17.111 (Yes, it must).

Uses 1

Statement usesKourovka Problem 17.111 (supplements of maximal subgroups of Sylow subgroups)

DefinitionKourovka Problem 19.88 (statement)#✓fully proved

The statement that for every partition \(\sigma\) of the set of all primes and every finite group \(G\): if for every prime \(p\), every Sylow \(p\)-subgroup \(P\) of \(G\) and every maximal subgroup \(V\) of \(P\) there is a \(\sigma\)-nilpotent subgroup \(T\) of \(G\) with \(VT = G\), that is, every element of \(G\) is a product \(vt\) with \(v \in V\) and \(t \in T\), then \(G\) is \(\sigma\)-nilpotent. Here a partition of the primes is a family of nonempty, pairwise disjoint sets of primes whose union is the set of all primes, and a group is \(\sigma\)-nilpotent when it is the internal direct product of finitely many normal subgroups, each of whose order has all its prime divisors in a single block of \(\sigma\).

def sylowMaximalSigmaNilpotentSupplement : Prop :=
  ∀ (I : Type) (σ : I → Set ℕ), IsPrimePartition σ → ∀ (G : Type) [Group G] [Finite G],
    (∀ p : ℕ, p.Prime → ∀ (P : Sylow p G) (V : Subgroup G), V ⋖ (P : Subgroup G) →
      ∃ T : Subgroup G, IsSigmaNilpotent σ T ∧ ∀ g : G, ∃ v ∈ V, ∃ t ∈ T, v * t = g) →
    IsSigmaNilpotent σ G

def IsPrimePartition {I : Type} (σ : I → Set ℕ) : Prop :=
  (∀ i, (σ i).Nonempty ∧ ∀ p ∈ σ i, p.Prime) ∧ (∀ i j, i ≠ j → Disjoint (σ i) (σ j)) ∧
    ∀ p : ℕ, p.Prime → ∃ i, p ∈ σ i

WantedExt/GroupTheory/KourovkaNotebookShared.lean:74

def IsSigmaNilpotent {I : Type} (σ : I → Set ℕ) (G : Type*) [Group G] : Prop :=
  ∃ (t : ℕ) (H : Fin t → Subgroup G), (∀ k, (H k).Normal ∧ IsSigmaPrimary σ (Nat.card (H k))) ∧
    (⨆ k, H k) = ⊤ ∧ ∀ k, H k ⊓ (⨆ j ∈ ({k}ᶜ : Set (Fin t)), H j) = ⊥

WantedExt/GroupTheory/KourovkaNotebookShared.lean:93

Uses 2 · Used by 1

Statement usesPartitions of the primes · \(\sigma\)-nilpotent groups

Used byσ-nilpotent supplements to the maximal subgroups of Sylow subgroups (Kourovka 19.88)

Theoremσ-nilpotent supplements to the maximal subgroups of Sylow subgroups (Kourovka 19.88)#●ready to prove

Let \(\sigma\) be a partition of the set of all primes and let \(G\) be a finite group. If for every prime \(p\), every Sylow \(p\)-subgroup \(P\) of \(G\) and every maximal subgroup \(V\) of \(P\) there is a \(\sigma\)-nilpotent subgroup \(T\) of \(G\) with \(VT = G\), that is, every element of \(G\) is a product \(vt\) with \(v \in V\) and \(t \in T\), then \(G\) is \(\sigma\)-nilpotent. Here a partition of the primes is a family of nonempty, pairwise disjoint sets of primes whose union is the set of all primes, and a group is \(\sigma\)-nilpotent when it is the internal direct product of finitely many normal subgroups, each of whose order has all its prime divisors in a single block of \(\sigma\).

public theorem_wanted sylowMaximalSigmaNilpotentSupplement_holds :
    sylowMaximalSigmaNilpotentSupplement

def sylowMaximalSigmaNilpotentSupplement : Prop :=
  ∀ (I : Type) (σ : I → Set ℕ), IsPrimePartition σ → ∀ (G : Type) [Group G] [Finite G],
    (∀ p : ℕ, p.Prime → ∀ (P : Sylow p G) (V : Subgroup G), V ⋖ (P : Subgroup G) →
      ∃ T : Subgroup G, IsSigmaNilpotent σ T ∧ ∀ g : G, ∃ v ∈ V, ∃ t ∈ T, v * t = g) →
    IsSigmaNilpotent σ G

WantedExt/GroupTheory/SylowMaximalSigmaNilpotentSupplementKourovka19Problem88Wanted.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), Archive of Solved Problems, Problem 19.88 (A. N. Skiba); resolution: A.-M. Liu, W. Guo, I. N. Safonova and A. N. Skiba, G-covering subgroup systems for some classes of σ-soluble groups, J. Algebra 585 (2021), 280-293; another solution using CFSG by S. F. Kamornikov and V. N. Tyutyanov, Trudy Inst. Mat. Mekh. UrO RAN 27 (2021), no. 1, 98-102, abstract: a set of subgroups of G containing a supplement to each maximal subgroup of every Sylow subgroup of G is a G-covering subgroup system for the classes of σ-soluble and of σ-nilpotent groups, which answers 19.87 and 19.88; Kourovka Archive, Problem 19.88: Yes, it is true, https://doi.org/10.1016/j.jalgebra.2021.06.010.

Uses 1

Statement usesKourovka Problem 19.88 (statement)

DefinitionKourovka Problem 19.87 (statement)#✓fully proved

The statement that for every partition \(\sigma\) of the set of all primes and every finite group \(G\): if for every prime \(p\), every Sylow \(p\)-subgroup \(P\) of \(G\) and every maximal subgroup \(V\) of \(P\) there is a \(\sigma\)-soluble subgroup \(T\) of \(G\) with \(VT = G\), that is, every element of \(G\) is a product \(vt\) with \(v \in V\) and \(t \in T\), then \(G\) is \(\sigma\)-soluble. Here a partition of the primes is a family of nonempty, pairwise disjoint sets of primes whose union is the set of all primes, and a group is \(\sigma\)-soluble when for every chief factor \(A/B\) of it (normal subgroups \(B < A\) with no normal subgroup strictly between them) all prime divisors of the index \(|A : B|\) lie in a single block of \(\sigma\).

def sylowMaximalSigmaSolubleSupplement : Prop :=
  ∀ (I : Type) (σ : I → Set ℕ), IsPrimePartition σ → ∀ (G : Type) [Group G] [Finite G],
    (∀ p : ℕ, p.Prime → ∀ (P : Sylow p G) (V : Subgroup G), V ⋖ (P : Subgroup G) →
      ∃ T : Subgroup G, IsSigmaSoluble σ T ∧ ∀ g : G, ∃ v ∈ V, ∃ t ∈ T, v * t = g) →
    IsSigmaSoluble σ G

def IsPrimePartition {I : Type} (σ : I → Set ℕ) : Prop :=
  (∀ i, (σ i).Nonempty ∧ ∀ p ∈ σ i, p.Prime) ∧ (∀ i j, i ≠ j → Disjoint (σ i) (σ j)) ∧
    ∀ p : ℕ, p.Prime → ∃ i, p ∈ σ i

WantedExt/GroupTheory/KourovkaNotebookShared.lean:74

def IsSigmaSoluble {I : Type} (σ : I → Set ℕ) (G : Type*) [Group G] : Prop :=
  ∀ A B : Subgroup G, IsChiefFactor A B → IsSigmaPrimary σ (B.relIndex A)

WantedExt/GroupTheory/KourovkaNotebookShared.lean:99

Uses 2 · Used by 1

Statement usesPartitions of the primes · \(\sigma\)-soluble groups

Used byσ-soluble supplements to the maximal subgroups of Sylow subgroups (Kourovka 19.87)

Theoremσ-soluble supplements to the maximal subgroups of Sylow subgroups (Kourovka 19.87)#●ready to prove

Let \(\sigma\) be a partition of the set of all primes and let \(G\) be a finite group. If for every prime \(p\), every Sylow \(p\)-subgroup \(P\) of \(G\) and every maximal subgroup \(V\) of \(P\) there is a \(\sigma\)-soluble subgroup \(T\) of \(G\) with \(VT = G\), that is, every element of \(G\) is a product \(vt\) with \(v \in V\) and \(t \in T\), then \(G\) is \(\sigma\)-soluble. Here a partition of the primes is a family of nonempty, pairwise disjoint sets of primes whose union is the set of all primes, and a group is \(\sigma\)-soluble when for every chief factor \(A/B\) of it (normal subgroups \(B < A\) with no normal subgroup strictly between them) all prime divisors of the index \(|A : B|\) lie in a single block of \(\sigma\).

public theorem_wanted sylowMaximalSigmaSolubleSupplement_holds : sylowMaximalSigmaSolubleSupplement

def sylowMaximalSigmaSolubleSupplement : Prop :=
  ∀ (I : Type) (σ : I → Set ℕ), IsPrimePartition σ → ∀ (G : Type) [Group G] [Finite G],
    (∀ p : ℕ, p.Prime → ∀ (P : Sylow p G) (V : Subgroup G), V ⋖ (P : Subgroup G) →
      ∃ T : Subgroup G, IsSigmaSoluble σ T ∧ ∀ g : G, ∃ v ∈ V, ∃ t ∈ T, v * t = g) →
    IsSigmaSoluble σ G

WantedExt/GroupTheory/SylowMaximalSigmaSolubleSupplementKourovka19Problem87Wanted.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), Archive of Solved Problems, Problem 19.87 (A. N. Skiba); resolution: A.-M. Liu, W. Guo, I. N. Safonova and A. N. Skiba, G-covering subgroup systems for some classes of σ-soluble groups, J. Algebra 585 (2021), 280-293; another solution using CFSG by S. F. Kamornikov and V. N. Tyutyanov, Trudy Inst. Mat. Mekh. UrO RAN 27 (2021), no. 1, 98-102, abstract: a set of subgroups of G containing a supplement to each maximal subgroup of every Sylow subgroup of G is a G-covering subgroup system for the classes of σ-soluble and of σ-nilpotent groups, which answers 19.87 and 19.88; Kourovka Archive, Problem 19.87: Yes, it is true, https://doi.org/10.1016/j.jalgebra.2021.06.010.

Uses 1

Statement usesKourovka Problem 19.87 (statement)

4 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.