§7 block structure and Lemma 7.1 (simple head)

Split off from GQ2.SectionSeven. This file provides the definition layer of the paper's §7:

• Scalar stacks (IsScalarStack) and the Frattini-like subgroup Φ(K) (frattiniLike) with its containment/normality API;
• the §7 minimal block MinimalBlock (S ◁ P ◁ Y, P ≤ L) with its radical field MinimalBlock.frattiniK (R = Φ(K)) and the existence theorem exists_minimalBlock;
• Lemma 7.1 (simple head): the head, radical and dual-invariants clauses (lemma_7_1_head, lemma_7_1_radical, lemma_7_1_dual).

See GQ2.SectionSeven for the umbrella module docstring.

Scalar stacks and the block structure

def GQ2.SectionSeven.IsScalarStack {Y : Type} [Group Y] (L : Subgroup Y) : Prop

Scalar stack (§7 opening): a normal chain ⊥ = c₀ ≤ c₁ ≤ ⋯ ≤ c_n = L (each cᵢ ◁ Y) whose successive layers are acted on trivially by Y (⁅y, x⁆ ∈ cᵢ for x ∈ cᵢ₊₁) — i.e. every chief factor of L is the trivial (scalar) module. The §7 block exists exactly when the marked kernel is not a scalar stack; the scalar regime is §9.1/9.2's case.

Equations

• One or more equations did not get rendered due to their size.

def GQ2.SectionSeven.frattiniLike {Y : Type} [Group Y] (K : Subgroup Y) : Subgroup Y

Φ-like subgroup: the subgroup of Y generated by the squares and commutators of the elements of K. For K ◁ Y a finite 2-group this is the Frattini subgroup Φ(K) = K²[K,K] of K, as a subgroup of Y (normal in Y, being characteristic in K).

Equations

• GQ2.SectionSeven.frattiniLike K = Subgroup.closure ({x : Y | ∃ k ∈ K, x = k * k} ∪ {x : Y | ∃ k ∈ K, ∃ l ∈ K, x = k * l * k⁻¹ * l⁻¹})

theorem GQ2.SectionSeven.frattiniLike_le {Y : Type} [Group Y] (K : Subgroup Y) : frattiniLike K ≤ K

Φ(K) ≤ K (the generators are squares and commutators of elements of K).

theorem GQ2.SectionSeven.frattiniLike_eq_map {Y : Type} [Group Y] (P : Subgroup Y) : frattiniLike P = Subgroup.map P.subtype (Subgroup.closure ({x : ↥P | ∃ (k : ↥P), x = k * k} ∪ {x : ↥P | ∃ (k : ↥P) (l : ↥P), x = k * l * k⁻¹ * l⁻¹}))

Φ(P) is the image of the subtype-level Frattini-like subgroup of ↥P — the bridge that lets quotient arguments run inside ↥P without closure inductions.

theorem GQ2.SectionSeven.frattiniLike_normal {Y : Type} [Group Y] (K : Subgroup Y) (hK : K.Normal) : (frattiniLike K).Normal

For K ◁ Y, Φ(K) is normal in Y (conjugation permutes the generating set).

structure GQ2.SectionSeven.MinimalBlock {Y : Type} [Group Y] (L : Subgroup Y) : Type

The §7 minimal block (§7 opening): S ◁ P ◁ Y with P ≤ L, everything below S scalar, V = P/S a nontrivial simple Y-chief factor, and K ◁ Y minimal with KS = P.

• hL : L.Normal

  The marked kernel is normal (a GQ2.MarkedTarget guarantee, carried so the block is self-contained).

• h2L : IsPGroup 2 ↥L

  The marked kernel is a 2-group — the paper's standing "marked normal 2-subgroup" hypothesis. It is necessary: without it, take Y = S₃, L = P = K = A₃, S = ⊥; all other fields hold but Φ(A₃) = A₃ ≰ K ⊓ S.

• S : Subgroup Y

  The scalar socle S.

• P : Subgroup Y

  The layer top P.

• K : Subgroup Y

  The minimal generator K.

• hS : self.S.Normal
• hP : self.P.Normal
• hK : self.K.Normal
• hPL : self.P ≤ L
• hSP : self.S < self.P
• scalar_below : IsScalarStack self.S

  All chief factors below S are trivial.

• chief (X : Subgroup Y) : X.Normal → self.S ≤ X → X ≤ self.P → X = self.S ∨ X = self.P

  P/S is a chief factor: no Y-normal subgroup strictly between.

• nontrivial_action : ∃ (y : Y), ∃ p ∈ self.P, y * p * y⁻¹ * p⁻¹ ∉ self.S

  V = P/S is a nontrivial module: some Y-conjugation moves P nontrivially mod S.

• hKP : self.K ≤ self.P
• gen : self.K ⊔ self.S = self.P

  KS = P.

• minimal (K' : Subgroup Y) : K'.Normal → K' ≤ self.K → K' ⊔ self.S = self.P → K' = self.K

  Minimality of K among Y-normal subgroups with K'S = P.

def GQ2.SectionSeven.MinimalBlock.frattiniK {Y : Type} [Group Y] {L : Subgroup Y} (B : MinimalBlock L) : Subgroup Y

R = Φ(K).

Equations

• B.frattiniK = GQ2.SectionSeven.frattiniLike B.K

theorem GQ2.SectionSeven.exists_minimalBlock {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (hL : L.Normal) (h2 : IsPGroup 2 ↥L) (h : ¬IsScalarStack L) : Nonempty (MinimalBlock L)

Existence of the block (§7 opening, "Choose …"): if the marked kernel L (a normal finite 2-group, GQ2.MarkedTarget's L_Y) is not a scalar stack, a minimal block exists. [the §§6–7 statement; proof the §§6–7 proof layer.]

Lemma 7.1 (simple head)

theorem GQ2.SectionSeven.lemma_7_1_head {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : MinimalBlock L) : B.frattiniK ≤ B.K ⊓ B.S

Lemma 7.1, head clause — recorded in its load-bearing form R ≤ K ∩ S (the paper's "Since K/(K∩S) ≅ V is elementary abelian, R ≤ K∩S; the displayed sequence follows"): given gen : K ⊔ S = P, the exact sequence 0 → T₀ → M → V → 0 and the head identification M/T₀ ≅ V are then the second isomorphism theorem (QuotientGroup.quotientInfEquivProdNormalQuotient), which Mathlib supplies — so the inclusion is the §7-specific content. [the §§6–7 statement; proof the §§6–7 proof layer.]

theorem GQ2.SectionSeven.lemma_7_1_radical {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : MinimalBlock L) (X : Subgroup Y) (hX : X.Normal) (_hRX : B.frattiniK ≤ X) (hXK : X < B.K) (hmax : ∀ (X' : Subgroup Y), X'.Normal → X < X' → X' ≤ B.K → X' = B.K) : X = B.K ⊓ B.S ⊔ B.frattiniK

Lemma 7.1, radical clause: T₀ = (K ∩ S)·R is the unique maximal Y-normal subgroup of K above R — i.e. T₀ = rad_{𝔽₂[C]} M and M/T₀ is the unique simple head. [the §§6–7 statement; proof the §§6–7 proof layer: the head clause collapses the right-hand side to K ⊓ S; the chief dichotomy on X ⊔ S then leaves two branches — = P dies by K's minimality, = S pins X = K ⊓ S by X's maximality (a strict inclusion would force K ≤ S, hence P = S). Stated after the head clause, which it consumes.]

theorem GQ2.SectionSeven.lemma_7_1_dual {Y : Type} [Group Y] {L : Subgroup Y} (B : MinimalBlock L) : ¬∃ (X : Subgroup Y), X.Normal ∧ B.frattiniK ≤ X ∧ X ≤ B.K ∧ (X.subgroupOf B.K).index = 2

Lemma 7.1, dual-invariants clause: (M^∨)^C = 0 — K has no Y-normal subgroup of index 2 above R (a nonzero invariant functional on M would be its kernel). [the §§6–7 statement; proof the §§6–7 proof layer — chief-dichotomy on X ⊔ S + minimality; the X ⊔ S = S branch pins |P/S| = 2, whence the Y-action mod S is trivial, contradicting nontrivial_action. Finiteness-free.]