Generation from two double cosets

If every element outside a subgroup B lies in one double coset B w B, then B and w generate the ambient group. When that group is nonsolvable, every solvable subgroup containing B is therefore equal to B.

Main statements

• Subgroup.closure_insert_eq_top_of_notMem_imp_mem_doubleCoset: a subgroup and a representative generate the ambient group when their two double cosets cover it.
• Subgroup.le_of_isSolvable_of_not_isSolvable_of_notMem_imp_mem_doubleCoset: in a nonsolvable group, that subgroup contains every solvable overgroup.

theorem Subgroup.closure_insert_eq_top_of_notMem_imp_mem_doubleCoset {G : Type u_1} [Group G] (B : Subgroup G) (w : G) (hcell : ∀ {g : G}, g ∉ B → g ∈ DoubleCoset.doubleCoset w ↑B ↑B) : closure (insert w ↑B) = ⊤

If every element outside a subgroup B belongs to the double coset B w B, then B and w generate the ambient group.

theorem Subgroup.le_of_isSolvable_of_not_isSolvable_of_notMem_imp_mem_doubleCoset {G : Type u_1} [Group G] (B P : Subgroup G) (w : G) [Group.IsSolvable ↥P] (hG : ¬Group.IsSolvable G) (hcell : ∀ {g : G}, g ∉ B → g ∈ DoubleCoset.doubleCoset w ↑B ↑B) (hBP : B ≤ P) : P ≤ B

Suppose every element outside B belongs to B w B. If the ambient group is not solvable, then every solvable subgroup containing B is contained in B.