Assembly of the proved raw §7 tower fields

This file packages the concrete objects already built over the corrected first chief factor and the selected KernelMinimal:

• R = Additive Phi(K) with the descended C = Y/K action (Section7RawRLayer);
• M = Additive (K/Phi(K)), T = (K cap S)/Phi(K), and the descended C-action (Section7ConcreteObjects, Section7SimpleHeadRadical);
• head nontriviality and (M^vee)^C = 0.

The remaining field of Sec7RawTowerPacket is the ambient quotient-image bridge Subgroup.map (QuotientGroup.mk' (kernelFrattini K)) K.Ksub ~= Multiplicative M.

def Q2Presentation.Induction.sec7RawModuleData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : MinimalBlockRawModuleData p chief.toNonScalarChiefFactor

The raw finite objects in the corrected §7 tower.

Equations

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

def Q2Presentation.Induction.sec7RawActionData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : MinimalBlockRawActionData (sec7RawModuleData chief K)

The descended C-actions on R and M, with stability of T.

Equations

• Q2Presentation.Induction.sec7RawActionData chief K = { actR := Q2Presentation.Induction.towerActR chief K, actM := Q2Presentation.Induction.towerActM K, T_stable := ⋯ }

def Q2Presentation.Induction.sec7RawTowerData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : MinimalBlockRawTowerData p chief.toNonScalarChiefFactor

The assembled raw tower data from the concrete objects and actions.

Equations

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

def Q2Presentation.Induction.sec7HeadNontrivialData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : MinimalBlockHeadNontrivialData (sec7RawTowerData chief K)

The nonzero simple-head field of lem:simplehead.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.sec7DualInvariantData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : MinimalBlockDualInvariantVanishesData (sec7RawTowerData chief K)

The dual-invariant vanishing field (M^vee)^C = 0.

Equations

• ⋯ = ⋯