theorem GQ2.commutator_P_le_S {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) : ⁅B.P, B.P⁆ ≤ B.S

Linchpin of the block descent (the §9 induction): the layer top P is abelian mod the scalar socle S — ⁅P, P⁆ ≤ S. ⁅P,P⁆ ⊔ S is Y-normal between S and P, so by the chief condition it is S or P; if P, then P̄ = P/S would be a perfect nontrivial finite 2-group, impossible (2-groups are nilpotent, IsPerfect.not_isNilpotent).

@[reducible]

noncomputable def GQ2.blockPS_commGroup {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) : CommGroup (↥B.P ⧸ B.S.subgroupOf B.P)

V = P/S is abelian (CommGroup), from ⁅P,P⁆ ≤ S (commutator_P_le_S).

Equations

• GQ2.blockPS_commGroup B = { toGroup := inferInstance, mul_comm := ⋯ }

@[reducible]

noncomputable def GQ2.blockActVY {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) : DistribMulAction Y (Additive (↥B.P ⧸ B.S.subgroupOf B.P))

The Y-conjugation action on Additive(P/S) as a DistribMulAction (the conjugation blockAction is by group automorphisms — QuotientGroup.map of conjHom — so it distributes over +).

Equations

• GQ2.blockActVY B = { toMulAction := GQ2.blockAction B.S B.P ⋯ ⋯, smul_zero := ⋯, smul_add := ⋯ }

theorem GQ2.blockK_smul_eq {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) {k : Y} (hk : k ∈ B.K) (q : ↥B.P ⧸ B.S.subgroupOf B.P) : k • q = q

K acts trivially on V = P/S ([K,P] ≤ ⁅P,P⁆ ≤ S): the key fact that lets the Y-conjugation action descend to Y/K.

@[reducible]

noncomputable def GQ2.blockActV {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) : DistribMulAction (Y ⧸ B.K) (Additive (↥B.P ⧸ B.S.subgroupOf B.P))

The descended Y/K-action on V = P/S — actV. The Y-conjugation action (blockActVY) descends because K acts trivially (blockK_smul_eq).

Equations

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

The descent surjection M_B ↠ V = P/S

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

M_B = image of K in Y/R.

Equations

• GQ2.blockMB B = Subgroup.map (QuotientGroup.mk' B.frattiniK) B.K

noncomputable def GQ2.blockKappa {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [B.frattiniK.Normal] : ↥B.K →* ↥(blockMB B)

The corestricted surjection κ' : K ↠ M_B, k ↦ [k]_R.

Equations

• GQ2.blockKappa B = ((QuotientGroup.mk' B.frattiniK).comp B.K.subtype).codRestrict (GQ2.blockMB B) ⋯

theorem GQ2.blockKappa_surjective {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [B.frattiniK.Normal] : Function.Surjective ⇑(blockKappa B)

noncomputable def GQ2.blockAlpha {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] : ↥B.K →* ↥B.P ⧸ B.S.subgroupOf B.P

α : K →* P/S, k ↦ [k]_S (via K ≤ P).

Equations

• GQ2.blockAlpha B = (QuotientGroup.mk' (B.S.subgroupOf B.P)).comp (Subgroup.inclusion ⋯)

theorem GQ2.blockAlpha_apply {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (k : ↥B.K) : (blockAlpha B) k = ↑((Subgroup.inclusion ⋯) k)

theorem GQ2.blockAlpha_eq_one_iff {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (k : ↥B.K) : (blockAlpha B) k = 1 ↔ ↑k ∈ B.S

theorem GQ2.blockKappa_ker_le_alpha {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [B.frattiniK.Normal] [(B.S.subgroupOf B.P).Normal] : (blockKappa B).ker ≤ (blockAlpha B).ker

ker κ' ≤ ker α: if [k]_R = 1 then k ∈ R ≤ S, so [k]_S = 1.

noncomputable def GQ2.blockDescend {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [B.frattiniK.Normal] [(B.S.subgroupOf B.P).Normal] : ↥(blockMB B) →* ↥B.P ⧸ B.S.subgroupOf B.P

The descent surjection M_B ↠ P/S.

Equations

• GQ2.blockDescend B = (QuotientGroup.lift (GQ2.blockKappa B).ker (GQ2.blockAlpha B) ⋯).comp (QuotientGroup.quotientKerEquivOfSurjective (GQ2.blockKappa B) ⋯).symm.toMonoidHom

theorem GQ2.blockDescend_kappa {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [B.frattiniK.Normal] [(B.S.subgroupOf B.P).Normal] (k : ↥B.K) : (blockDescend B) ((blockKappa B) k) = (blockAlpha B) k

The characterizing identity: descend ∘ κ' = α.

theorem GQ2.blockDescend_surjective {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [B.frattiniK.Normal] [(B.S.subgroupOf B.P).Normal] : Function.Surjective ⇑(blockDescend B)

descend is surjective onto P/S: every [p]_S is hit, because KS = P (B.gen) lets us replace p by a K-representative.

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

T_B = image of K ⊓ S ⊔ RinY/R(theBlockFrameImpl` definition).

Equations

• GQ2.blockTBsub B = Subgroup.map (QuotientGroup.mk' B.frattiniK) (B.K ⊓ B.S ⊔ B.frattiniK)

theorem GQ2.blockDescend_ker {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [B.frattiniK.Normal] [(B.S.subgroupOf B.P).Normal] (m : ↥(blockMB B)) : (blockDescend B) m = 1 ↔ ↑m ∈ blockTBsub B

ker descend = T_B: descend m = 1 ↔ m ∈ T_B. Both sides reduce to k ∈ S for a K-representative k of m, using R ≤ K ⊓ S (lemma_7_1_head) to collapse T_B to the image of K ⊓ S.

noncomputable def GQ2.blockPiBC {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [B.frattiniK.Normal] [B.K.Normal] : Y ⧸ B.frattiniK →* Y ⧸ B.K

The C-stage projection π_{BC} : Y/R ↠ Y/K (the BlockFrameImpl definition).

Equations

• GQ2.blockPiBC B = QuotientGroup.map B.frattiniK B.K (MonoidHom.id Y) ⋯

theorem GQ2.blockActV_mk' {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (y : Y) (v : Additive (↥B.P ⧸ B.S.subgroupOf B.P)) : (QuotientGroup.mk' B.K) y • v = y • v

Y/K-action on mk' K y reduces to the Y-action of y.

theorem GQ2.blockActVY_mk {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (y : Y) (p : ↥B.P) : y • Additive.ofMul ↑p = Additive.ofMul ↑((conjHom B.P ⋯ y) p)

The Y-action of y on ⟦p⟧ computes as ⟦y p y⁻¹⟧.

theorem GQ2.blockDescend_conj {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [B.frattiniK.Normal] [(B.S.subgroupOf B.P).Normal] (bb : Y ⧸ B.frattiniK) (m : ↥(blockMB B)) (hm : bb * ↑m * bb⁻¹ ∈ blockMB B) : (blockPiBC B) bb • Additive.ofMul ((blockDescend B) m) = Additive.ofMul ((blockDescend B) ⟨bb * ↑m * bb⁻¹, hm⟩)

descend intertwines B-conjugation with the C-stage action (descend_conj): for the Y/K-action on V = P/S, descend(b·m·b⁻¹) = π_{BC}(b) • descend(m). Proved by lifting m and b to K- and Y-representatives and reducing both sides to ⟦y k y⁻¹⟧_S.