The radical layer T and head nontriviality (lem:simplehead, part 1)

Over the concrete §7 tower (Section7ConcreteObjects): the manuscript's T = (K ∩ S)/R ◁ M (l.3628) as a C-stable submodule of M = K/Φ(K), and the nontriviality of the head M/T:

• towerT K — the image of K ∩ S in M, as a ZMod 2-submodule;
• towerT_stable — conjugation stability (S = chief.lower is normal in Y);
• towerT_ne_top — T ≠ M: otherwise (K∩S) ⊔ Φ(K) = K, so by the Frattini non-generating property K ≤ S, whence K ⊔ S = S < P, contradicting KS = P;
• head_nontrivial — Nontrivial (M ⧸ T).

Everything here is proved — no axioms.

The radical layer T

@[reducible, inline]

abbrev Q2Presentation.Induction.kernelInterS {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Subgroup ↥K.Ksub

K ∩ S as a subgroup of the kernel.

Equations

• Q2Presentation.Induction.kernelInterS K = chief.lower.subgroupOf K.Ksub

def Q2Presentation.Induction.towerTgrp {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Subgroup (towerMgrp K)

The multiplicative image of K ∩ S in the Frattini quotient.

Equations

• Q2Presentation.Induction.towerTgrp K = Subgroup.map (QuotientGroup.mk' (frattini ↥K.Ksub)) (Q2Presentation.Induction.kernelInterS K)

def Q2Presentation.Induction.towerT {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Submodule (ZMod 2) (towerM K)

The manuscript's radical layer T = (K ∩ S)/R ◁ M (l.3628), as a ZMod 2-submodule of the additive module M.

Equations

• Q2Presentation.Induction.towerT K = (AddSubgroup.toZModSubmodule 2) (Subgroup.toAddSubgroup (Q2Presentation.Induction.towerTgrp K))

theorem Q2Presentation.Induction.mem_towerT_iff {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (m : towerM K) : m ∈ towerT K ↔ Additive.toMul m ∈ towerTgrp K

C-stability of T

theorem Q2Presentation.Induction.towerT_stable {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (c : towerC K) (m : towerM K) (hm : m ∈ towerT K) : ((towerActM K) c) m ∈ towerT K

The radical layer is stable under the conjugation action of C — S is normal in Y, so conjugation preserves K ∩ S.

Head nontriviality

theorem Q2Presentation.Induction.interS_sup_frattini_of_top {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (h : towerTgrp K = ⊤) : kernelInterS K ⊔ frattini ↥K.Ksub = ⊤

If the image of K ∩ S fills the Frattini quotient, then (K ∩ S) ⊔ Φ(K) = K inside the kernel.

theorem Q2Presentation.Induction.towerTgrp_ne_top {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : towerTgrp K ≠ ⊤

T ≠ M — the head is a genuine quotient: otherwise the Frattini non-generating property forces K ≤ S, contradicting K ⊔ S = P > S.

theorem Q2Presentation.Induction.towerT_ne_top {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : towerT K ≠ ⊤

T is a proper submodule of M.

theorem Q2Presentation.Induction.head_nontrivial {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Nontrivial (towerM K ⧸ towerT K)

The head is nontrivial (lem:simplehead): M/T ≠ 0.