More concrete target-tower closers

This sidecar pushes the Section 8 target/proper-image packets one layer closer to the finite subgroup data used in the manuscript.

Manuscript anchors:

• eq:targettower: R = Phi(K), K <= L_Y, K/R ≃ M, and the quotient children Y/R, Y/K;
• eq:Mstage / eq:Mdescent: the marked-kernel exact sequences and the literal J ∩ M kernels for proper exact-image subgroups;
• lem:strictdecrease: proper exact-image kernels are proper in the elementary kernel because J < B but J -> C is onto.

The file deliberately does not route the root theorem through these new packets. It supplies theorem-level reassembly lemmas from smaller semantic packets, so a future capstone reroute can replace the current target/proper-image residual names by these more concrete ones.

General subgroup facts for the literal J ∩ M kernels

theorem Q2Presentation.Induction.TargetTowerConcreteClosers.subgroup_eq_top_of_ker_le_of_surjective_restrict {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (J : Subgroup G) (hJ : Function.Surjective ⇑(f.comp J.subtype)) (hker : f.ker ≤ J) : J = ⊤

If a subgroup maps onto the quotient and contains the kernel, then it is the whole domain. This is the finite-group reason that a proper exact-image subgroup J < B has J ∩ ker(B -> C) < ker(B -> C).

Subgroup provenance for R = Phi(K) and K/R ≃ M

structure Q2Presentation.Induction.CentralCoverTargetSubgroupConcreteData {p : FramedPair} (B : MinimalBlock p) : Type

Concrete subgroup provenance behind centralCover_targetSubgroupTowerData.

This is the manuscript-level target tower before quotient children are attached: R = Phi(K), R <= K <= L_Y, normality in Y, nontrivial R, and the identification of the elementary quotient K/R with the abstract module M. The quotient K/R is represented as the image of K in Y/R.

• Rsub : Subgroup p.fst.Y
• Ksub : Subgroup p.fst.Y
• Rsub_normal : self.Rsub.Normal
• Ksub_normal : self.Ksub.Normal
• Rsub_le_Ksub : self.Rsub ≤ self.Ksub
• Ksub_le_LY : self.Ksub ≤ p.fst.LY
• Rsub_card_gt_one : 1 < Nat.card ↥self.Rsub
• Rsub_eq_frattini : self.Rsub = Subgroup.map self.Ksub.subtype (frattini ↥self.Ksub)
• KmodR_equivM : ↥(Subgroup.map (QuotientGroup.mk' self.Rsub) self.Ksub) ≃* Multiplicative B.M

def Q2Presentation.Induction.targetSubgroupTowerData_of_concrete {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : CentralCoverTargetSubgroupTowerData B

Project the concrete subgroup provenance to the current target-subgroup packet.

Equations

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

theorem Q2Presentation.Induction.centralCover_targetSubgroupTowerData_from_concrete {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverTargetSubgroupConcreteData B) → Nonempty (CentralCoverTargetSubgroupTowerData B)

Nonempty reassembly of centralCover_targetSubgroupTowerData from literal R = Phi(K) / K/R ≃ M provenance.

structure Q2Presentation.Induction.CentralCoverTargetSubgroupProvenanceData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) : Type

Extra provenance attached to an already selected subgroup tower.

• Rsub_eq_frattini : S.Rsub = Subgroup.map S.Ksub.subtype (frattini ↥S.Ksub)
• KmodR_equivM : ↥(Subgroup.map (QuotientGroup.mk' S.Rsub) S.Ksub) ≃* Multiplicative B.M

def Q2Presentation.Induction.targetSubgroupProvenanceData_of_concrete {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : CentralCoverTargetSubgroupProvenanceData B (targetSubgroupTowerData_of_concrete B D)

The provenance fields carried by concrete subgroup data.

Equations

• Q2Presentation.Induction.targetSubgroupProvenanceData_of_concrete B D = { Rsub_eq_frattini := ⋯, KmodR_equivM := D.KmodR_equivM }

Quotient children from concrete quotient/provenance data

structure Q2Presentation.Induction.CentralCoverTargetQuotientChildConcreteData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) extends Q2Presentation.Induction.CentralCoverTargetSubgroupProvenanceData B S : Type 1

Framed quotient children plus the subgroup provenance fields that identify the tower as the manuscript's Y/R -> Y/K. The existing packet consumes only the quotient equivalences; the extra fields record the concrete semantics.

• Rsub_eq_frattini : S.Rsub = Subgroup.map S.Ksub.subtype (frattini ↥S.Ksub)
• KmodR_equivM : ↥(Subgroup.map (QuotientGroup.mk' S.Rsub) S.Ksub) ≃* Multiplicative B.M
• middleChild : FramedPair
• lowerChild : FramedPair
• middleEquiv : p.fst.Y ⧸ S.Rsub ≃* self.middleChild.fst.Y
• lowerEquiv : p.fst.Y ⧸ S.Ksub ≃* self.lowerChild.fst.Y

def Q2Presentation.Induction.targetQuotientChildEquivData_of_concrete {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (D : CentralCoverTargetQuotientChildConcreteData B S) : CentralCoverTargetQuotientChildEquivData B S

Forget the extra provenance and recover the quotient-child equivalence packet used by TargetTowerPacketClosers.

Equations

• Q2Presentation.Induction.targetQuotientChildEquivData_of_concrete B S D = { middleChild := D.middleChild, lowerChild := D.lowerChild, middleEquiv := D.middleEquiv, lowerEquiv := D.lowerEquiv }

theorem Q2Presentation.Induction.centralCover_targetQuotientChildEquivData_from_concrete {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) : Nonempty (CentralCoverTargetQuotientChildConcreteData B S) → Nonempty (CentralCoverTargetQuotientChildEquivData B S)

Nonempty reassembly of centralCover_targetQuotientChildEquivData from concrete quotient-child data with provenance.

Marked-kernel exactness split into top, middle, and M identification

structure Q2Presentation.Induction.CentralCoverTargetTopMarkedExactData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Type

Exactness of the marked-kernel map L_Y -> L_B, with kernel R.

• topMarkedMap : ↥p.fst.LY →* ↥Q.middleChild.fst.LY
• topMarkedMap_surj : Function.Surjective ⇑self.topMarkedMap
• topMarkedKernelEquivR : ↥self.topMarkedMap.ker ≃* ↥S.Rsub

structure Q2Presentation.Induction.CentralCoverTargetMiddleMarkedExactData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Type

Exactness of the marked-kernel map L_B -> L_C, with kernel the kernel of B -> C.

• middleMarkedMap : ↥Q.middleChild.fst.LY →* ↥Q.lowerChild.fst.LY
• middleMarkedMap_surj : Function.Surjective ⇑self.middleMarkedMap
• middleMarkedKernelEquiv : ↥self.middleMarkedMap.ker ≃* ↥Q.middleToLower.ker

structure Q2Presentation.Induction.CentralCoverTargetMiddleKernelIdentificationData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Type

Identification of ker(B -> C) with the elementary layer M = K/R.

• middleKernelEquivM : ↥Q.middleToLower.ker ≃* Multiplicative B.M

def Q2Presentation.Induction.targetTowerMarkedExactData_of_parts {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (Top : CentralCoverTargetTopMarkedExactData B S Q) (Mid : CentralCoverTargetMiddleMarkedExactData B S Q) (Ker : CentralCoverTargetMiddleKernelIdentificationData B S Q) : CentralCoverTargetTowerMarkedExactData B S Q

Reassemble the marked exactness packet from its three semantic pieces.

Equations

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

theorem Q2Presentation.Induction.centralCover_targetTowerMarkedExactData_from_parts {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetTopMarkedExactData B S Q) → Nonempty (CentralCoverTargetMiddleMarkedExactData B S Q) → Nonempty (CentralCoverTargetMiddleKernelIdentificationData B S Q) → Nonempty (CentralCoverTargetTowerMarkedExactData B S Q)

Nonempty reassembly of the current marked exactness packet from the three smaller exact-sequence packets.

Literal J ∩ M data for proper exact-image children

def Q2Presentation.Induction.elementaryProperImageLiteralKernelPart {p : FramedPair} {B : MinimalBlock p} (T : CentralCoverElementaryQuotientTowerData B) (i : CentralCoverElementaryProperExactImageSubgroups T) : Subgroup ↥T.middleToLower.ker

The literal subgroup J ∩ ker(B -> C) inside ker(B -> C). Via the separate kernel identification this is the manuscript's J ∩ M.

Equations

• Q2Presentation.Induction.elementaryProperImageLiteralKernelPart T i = (↑i).subgroupOf T.middleToLower.ker

theorem Q2Presentation.Induction.elementaryProperImageLiteralKernelPart_proper {p : FramedPair} {B : MinimalBlock p} (T : CentralCoverElementaryQuotientTowerData B) (i : CentralCoverElementaryProperExactImageSubgroups T) : elementaryProperImageLiteralKernelPart T i < ⊤

For a proper exact-image subgroup J < B mapping onto C, the literal kernel J ∩ ker(B -> C) is proper in ker(B -> C).

structure Q2Presentation.Induction.CentralCoverElementaryProperImageLiteralKernelData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Type

Semantic data needed to turn literal intersections J ∩ ker(B -> C) into the current kernel-bound packet: only the identification ker(B -> C) ≃ M is left as data; properness is proved above.

• middleKernelEquivM : ↥T.middleToLower.ker ≃* Multiplicative B.M

def Q2Presentation.Induction.elementaryProperImageKernelBoundData_of_literalIntersections {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverElementaryProperImageLiteralKernelData B T) : CentralCoverElementaryProperImageKernelBoundData B T

Reassemble the current proper-image kernel-bound packet using the literal subgroups J ∩ ker(B -> C).

Equations

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

theorem Q2Presentation.Induction.centralCover_elementaryProperImageKernelBoundData_from_literalIntersections {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageLiteralKernelData B T) → Nonempty (CentralCoverElementaryProperImageKernelBoundData B T)

Nonempty reassembly of centralCover_elementaryProperImageKernelBoundData from literal J ∩ M data.

Restricted exact sequences split into maps and kernel identifications

structure Q2Presentation.Induction.CentralCoverElementaryProperImageRestrictedMapsData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) : Type

The restricted maps J ∩ L_B -> L_C and their surjectivity.

• restrictedMap (i : CentralCoverElementaryProperExactImageSubgroups T) : ↥(T.middleChild.fst.LY.subgroupOf ↑i) →* ↥T.lowerChild.fst.LY
• restrictedMap_surj (i : CentralCoverElementaryProperExactImageSubgroups T) : Function.Surjective ⇑(self.restrictedMap i)

structure Q2Presentation.Induction.CentralCoverElementaryProperImageRestrictedKernelIdentificationData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) (D : CentralCoverElementaryProperImageRestrictedMapsData B T K) : Type

The kernel identifications for the restricted exact sequences.

• restrictedKernelEquiv (i : CentralCoverElementaryProperExactImageSubgroups T) : ↥(D.restrictedMap i).ker ≃* ↥(K.kernelPart i)

def Q2Presentation.Induction.elementaryProperImageRestrictedExactData_of_parts {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) (Maps : CentralCoverElementaryProperImageRestrictedMapsData B T K) (Kers : CentralCoverElementaryProperImageRestrictedKernelIdentificationData B T K Maps) : CentralCoverElementaryProperImageRestrictedExactData B T K

Reassemble the restricted exact-sequence packet from restricted maps and their kernel identifications.

Equations

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

theorem Q2Presentation.Induction.centralCover_elementaryProperImageRestrictedExactData_from_parts {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) : (∃ (Maps : CentralCoverElementaryProperImageRestrictedMapsData B T K), Nonempty (CentralCoverElementaryProperImageRestrictedKernelIdentificationData B T K Maps)) → Nonempty (CentralCoverElementaryProperImageRestrictedExactData B T K)

Nonempty reassembly of the current restricted exact-sequence packet from separate map-surjectivity and kernel-identification packets.

Optional residual names at the more concrete layer

axiom Q2Presentation.Induction.centralCover_targetSubgroupConcreteData {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverTargetSubgroupConcreteData B)

More concrete residual: subgroup provenance with literal R = Phi(K) and K/R ≃ M.

axiom Q2Presentation.Induction.centralCover_targetQuotientChildConcreteData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) : Nonempty (CentralCoverTargetQuotientChildConcreteData B S)

More concrete residual: quotient children compatible with the selected subgroup provenance.

axiom Q2Presentation.Induction.centralCover_targetTopMarkedExactData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetTopMarkedExactData B S Q)

More concrete residual: top marked-kernel exact sequence.

axiom Q2Presentation.Induction.centralCover_targetMiddleMarkedExactData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetMiddleMarkedExactData B S Q)

More concrete residual: middle marked-kernel exact sequence.

axiom Q2Presentation.Induction.centralCover_targetMiddleKernelIdentificationData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetMiddleKernelIdentificationData B S Q)

More concrete residual: ker(B -> C) ≃ M.

axiom Q2Presentation.Induction.centralCover_elementaryProperImageLiteralKernelData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageLiteralKernelData B T)

More concrete residual: literal proper-image kernels J ∩ M.

axiom Q2Presentation.Induction.centralCover_elementaryProperImageRestrictedMapsData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) : Nonempty (CentralCoverElementaryProperImageRestrictedMapsData B T K)

More concrete residual: restricted maps J ∩ L_B -> L_C.

axiom Q2Presentation.Induction.centralCover_elementaryProperImageRestrictedKernelIdentificationData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) (Maps : CentralCoverElementaryProperImageRestrictedMapsData B T K) : Nonempty (CentralCoverElementaryProperImageRestrictedKernelIdentificationData B T K Maps)

More concrete residual: kernels of the restricted maps are the selected literal J ∩ M subgroups.

Reassembly using only the more concrete residual names

theorem Q2Presentation.Induction.centralCover_targetTowerMarkedExactData_from_concreteExactData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) : Nonempty (CentralCoverTargetTowerMarkedExactData B S Q)

Marked exactness reassembled from the split top/middle/kernel packets.

theorem Q2Presentation.Induction.centralCover_elementaryQuotientTowerData_from_concreteClosers {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryQuotientTowerData B)

Quotient tower reassembled from concrete subgroup, quotient-child, and marked-exactness packets.

theorem Q2Presentation.Induction.centralCover_elementaryProperImageCardinalityData_from_concreteClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageCardinalityData B T)

Proper-image cardinality data reassembled from literal J ∩ M kernels and restricted exact sequences.

theorem Q2Presentation.Induction.centralCover_elementaryStageChildren_from_concreteClosers {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryStageChildren B)

Elementary-stage children reassembled from the concrete target/proper-image closers in this file.

theorem Q2Presentation.Induction.centralCover_childrenData_from_concreteTargetClosers {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverChildrenData B)

Central-cover child data assembled with the concrete target/proper-image closers in this file and the existing theorem-level scalar/phase strata.

theorem Q2Presentation.Induction.centralCover_partialRecipe_fine_from_concreteTargetClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverLiftTorsorData B) : Nonempty (CentralCoverPartialRecipe B T)

Partial recipe assembled with the concrete target/proper-image closers.