Block-module infrastructure for §7

Reusable finite-group-theory layer for GQ2.SectionSeven.lemma_7_2 (and, later, §§8–9's scalar-regime arguments). Block-agnostic: everything is phrased for subgroups S ≤ P ≤ Y with the chief-factor / nontriviality hypotheses as explicit arguments, so MinimalBlock (in SectionSeven.lean) applies it without a dependency cycle.

Contents:

• comm_bot_of_scalarChain — a coprime odd group acting on a Y-central series is trivial (⁅Ñ, c n⁆ = ⊥). Mathlib lacks the coprime-action commutator theory; this is the special case §7 needs, proved by central-series induction. (Relocated from SectionSeven.lean, made public.)
• blockAction — the Y-conjugation MulAction on V = P/S = ↥P ⧸ (S.subgroupOf P).
• exists_odd_moving_general — since V is a nontrivial simple 𝔽₂[Y]-module (chief factor), the image Ȳ = Y/C_Y(V) is not a 2-group (a 2-group fixes a nonzero vector, contradicting the chief condition), so Y contains an odd-order element moving V. This replaces the paper's odd Hall lift — no Hall's theorem / Schur–Zassenhaus needed.

Coprime odd action on a central series

theorem GQ2.comm_bot_of_scalarChain (n : ℕ) {G : Type} [Group G] [Finite G] (Nt : Subgroup G) (c : ℕ → Subgroup G) : c 0 = ⊥ → (∀ (i : ℕ), c i ≤ c (i + 1)) → (∀ (i : ℕ) (g x : G), x ∈ c (i + 1) → g * x * g⁻¹ * x⁻¹ ∈ c i) → (Nat.card ↥Nt).Coprime (Nat.card ↥(c n)) → ⁅Nt, c n⁆ = ⊥

The Y-conjugation action on V = P/S

noncomputable def GQ2.conjHom {Y : Type} [Group Y] (P : Subgroup Y) (hP : P.Normal) (y : Y) : ↥P →* ↥P

Conjugation by y ∈ Y as an endomorphism of the normal subgroup P.

Equations

• GQ2.conjHom P hP y = { toFun := fun (p : ↥P) => ⟨y * ↑p * y⁻¹, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.conjHom_compat {Y : Type} [Group Y] (S P : Subgroup Y) (hS : S.Normal) (hP : P.Normal) (y : Y) : S.subgroupOf P ≤ Subgroup.comap (conjHom P hP y) (S.subgroupOf P)

@[reducible]

noncomputable def GQ2.blockAction {Y : Type} [Group Y] (S P : Subgroup Y) (hS : S.Normal) (hP : P.Normal) : MulAction Y (↥P ⧸ S.subgroupOf P)

The conjugation MulAction of Y on V = ↥P ⧸ (S.subgroupOf P). Marked reducible so y • ⟦p⟧ unfolds definitionally to QuotientGroup.map … ⟦p⟧ at the users.

Equations

• GQ2.blockAction S P hS hP = { smul := fun (y : Y) => ⇑(QuotientGroup.map (S.subgroupOf P) (S.subgroupOf P) (GQ2.conjHom P hP y) ⋯), mul_smul := ⋯, one_smul := ⋯ }

theorem GQ2.blockAction_smul_mk {Y : Type} [Group Y] (S P : Subgroup Y) (hS : S.Normal) (hP : P.Normal) (y : Y) (p : ↥P) : y • ↑p = ↑((conjHom P hP y) p)

noncomputable def GQ2.blockPerm {Y : Type} [Group Y] (S P : Subgroup Y) (hS : S.Normal) (hP : P.Normal) : Y →* Equiv.Perm (↥P ⧸ S.subgroupOf P)

The Y-conjugation action as a permutation representation Y →* Perm (P/S), built directly from QuotientGroup.map (so φ y ⟦p⟧ reduces to ⟦conjHom y p⟧ with no MulAction instance diamond — the form the p-group fixed-point count needs).

Equations

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

@[simp]

theorem GQ2.blockPerm_apply_mk {Y : Type} [Group Y] (S P : Subgroup Y) (hS : S.Normal) (hP : P.Normal) (y : Y) (p : ↥P) : ((blockPerm S P hS hP) y) ↑p = ↑((conjHom P hP y) p)

Existence of an odd-order element moving the chief factor

theorem GQ2.exists_odd_moving_general {Y : Type} [Group Y] [Finite Y] (S P : Subgroup Y) (hS : S.Normal) (hP : P.Normal) (hSP : S < P) (hP2 : IsPGroup 2 ↥P) (chief : ∀ (X : Subgroup Y), X.Normal → S ≤ X → X ≤ P → X = S ∨ X = P) (hnt : ∃ (y : Y), ∃ p ∈ P, y * p * y⁻¹ * p⁻¹ ∉ S) : ∃ (y : Y), Odd (orderOf y) ∧ ∃ p ∈ P, y * p * y⁻¹ * p⁻¹ ∉ S

An odd-order element moves the simple head V = P/S. Given the chief condition and a nontrivial Y-action, there is an odd-order y ∈ Y and a p ∈ P with [y, p] ∉ S. The paper's odd Hall lift is replaced by this p-group/Cauchy argument (no Hall / Schur–Zassenhaus). [the Lemma 7.2 proof.]