Route200 Section 7 combined kernel provider

Combines the two independent Route199 Section 7 lowerings:

• Frattini/least-kernel data from Section7KernelRoute199FrattiniClosers;
• raw quotient/simple-head data from Section7KernelRoute199RawClosers.

structure Q2Presentation.Induction.Section7KernelRoute200Closers.KernelRoute200LayerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

• least : MinimalBlockKernelLeastOverChiefData chief
• frattini : MinimalBlockKernelModuleConcreteFrattiniData self.least
• rawTower : MinimalBlockKernelRawQuotientTowerData self.least ⋯
• rawSimple : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData self.rawTower.rawData.rawTowerData

def Q2Presentation.Induction.Section7KernelRoute200Closers.KernelRoute200LayerData.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute200LayerData chief) : MinimalBlockKernelModuleConcreteProvenanceData chief

Equations

• D.concreteProvenanceData = Q2Presentation.Induction.Section7KernelRoute167Closers.concreteProvenanceDataOfRawQuotientTower D.least ⋯ D.rawTower

def Q2Presentation.Induction.Section7KernelRoute200Closers.KernelRoute200LayerData.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute200LayerData chief) : MinimalBlockLowerGroupModuleData chief

Equations

• D.lowerGroupModuleData = Q2Presentation.Induction.minimalBlock_lowerFromConcreteProvenance D.concreteProvenanceData

def Q2Presentation.Induction.Section7KernelRoute200Closers.KernelRoute200LayerData.invariantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute200LayerData chief) : MinimalBlockInvariantActualProofs2Data D.lowerGroupModuleData.rawTowerData

Equations

• D.invariantActualData = id (Q2Presentation.Induction.MinimalBlockInvariantRoute112Closers.invariantActualProofs2Data_of_rawSimpleHeadSemanticData ⋯)

def Q2Presentation.Induction.Section7KernelRoute200Closers.KernelRoute200LayerData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute200LayerData chief) : MinimalBlockGroupTowerData p chief

Equations

• D.groupTowerData = D.lowerGroupModuleData.groupTowerData ⋯ ⋯

theorem Q2Presentation.Induction.Section7KernelRoute200Closers.kernelRoute200LayerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute200LayerData chief)

theorem Q2Presentation.Induction.Section7KernelRoute200Closers.minimalBlock_groupTowerData_from_section7KernelRoute200Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)