Frattini nongeneration for frattiniLike

The finite-2-group nongeneration property of Φ(K) = K²[K,K] (SectionSeven.frattiniLike): H ⊔ Φ(K) = K forces H = K. Every maximal subgroup of the finite 2-group K is normal of index 2, so its quotient is ℤ/2 — abelian of exponent 2 — and therefore contains all squares and commutators; a proper H lies under some maximal subgroup, which then also contains H ⊔ Φ(K).

Consequence (eq_top_of_map_frattini_quotient_top): in the §8 recursion, an R-lift whose image maps onto Y/R = Y/Φ(K) is automatically surjective — the paper's Frattini argument in the proof of Prop 8.9 ("if its image J maps onto Y/R, then (J ∩ K)R = K; because R = Φ(K), the Frattini argument forces J ∩ K = K, and hence J = Y").

All std-3; no axioms.

theorem GQ2.sq_mem_frattiniLike {Y : Type} [Group Y] {K : Subgroup Y} {k : Y} (hk : k ∈ K) : k * k ∈ SectionSeven.frattiniLike K

Squares of K-elements lie in Φ(K) (they are half of its generating set).

theorem GQ2.comm_mem_frattiniLike {Y : Type} [Group Y] {K : Subgroup Y} {k l : Y} (hk : k ∈ K) (hl : l ∈ K) : k * l * k⁻¹ * l⁻¹ ∈ SectionSeven.frattiniLike K

Commutators of K-elements lie in Φ(K) (the other half of its generating set).

theorem GQ2.frattiniLike_nongen {Y : Type} [Group Y] [Finite Y] {K H : Subgroup Y} (h2K : IsPGroup 2 ↥K) (hHK : H ≤ K) (hsup : H ⊔ SectionSeven.frattiniLike K = K) : H = K

Frattini nongeneration for the finite 2-group K: a subgroup H ≤ K with H ⊔ Φ(K) = K is all of K. (Φ(K) = K²[K,K] = frattiniLike K.)

theorem GQ2.eq_top_of_map_frattini_quotient_top {Y : Type} [Group Y] [Finite Y] {B : Type} [Group B] (piB : Y →* B) {K : Subgroup Y} (h2K : IsPGroup 2 ↥K) (hker : piB.ker = SectionSeven.frattiniLike K) (hRK : SectionSeven.frattiniLike K ≤ K) [hRn : (SectionSeven.frattiniLike K).Normal] {J : Subgroup Y} (hJtop : Subgroup.map piB J = ⊤) : J = ⊤

The §8 R-lift surjectivity (paper, proof of Prop 8.9): if J ≤ Y maps onto Y/R for R = Φ(K) a normal subgroup with R ≤ K and K a 2-group inside the marked kernel, then J = ⊤. Route: J ⊔ R = ⊤ (image onto the quotient, R normal), the Dedekind step K = (J ⊓ K) ⊔ R (elementwise, R ≤ K and R normal), nongeneration forces J ⊓ K = K, so R ≤ K ≤ J and J = J ⊔ R = ⊤.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Prop 8.9 = ⟦thm-closedrecursion⟧ (= theorem 8.17 in current tex)