Target-tower packet closers

This sidecar supplies theorem-level finite-group closers for the refined Section 8 target/proper-image packets in ElementaryTowerResiduals.lean.

The current MinimalBlock interface still does not construct the realized normal subgroups R <= K <= L_Y inside an arbitrary target. Accordingly this file does not assert the five live packet axioms. Instead it proves the quotient-map and exact-sequence/cardinality parts once the missing concrete subgroups, framed quotient targets, and restriction maps are supplied as data.

Manuscript anchors:

• eq:targettower: Y -> B = Y/R -> C = Y/K;
• eq:Mstage / eq:Mdescent: the exact sequences on marked kernels for proper exact-image subgroups.

General finite-group closers

def Q2Presentation.Induction.TargetTowerClosers.quotientMapOfLEHom {G : Type u_1} [Group G] {R K : Subgroup G} [R.Normal] [K.Normal] (hRK : R ≤ K) : G ⧸ R →* G ⧸ K

The canonical quotient map G/R -> G/K induced by R <= K.

Equations

• Q2Presentation.Induction.TargetTowerClosers.quotientMapOfLEHom hRK = QuotientGroup.map R K (MonoidHom.id G) hRK

@[simp]

theorem Q2Presentation.Induction.TargetTowerClosers.quotientMapOfLEHom_mk {G : Type u_1} [Group G] {R K : Subgroup G} [R.Normal] [K.Normal] (hRK : R ≤ K) (g : G) : (quotientMapOfLEHom hRK) ((QuotientGroup.mk' R) g) = (QuotientGroup.mk' K) g

theorem Q2Presentation.Induction.TargetTowerClosers.quotientMapOfLEHom_surjective {G : Type u_1} [Group G] {R K : Subgroup G} [R.Normal] [K.Normal] (hRK : R ≤ K) : Function.Surjective ⇑(quotientMapOfLEHom hRK)

The quotient map G/R -> G/K is onto.

theorem Q2Presentation.Induction.TargetTowerClosers.quotientMapOfLEHom_ker {G : Type u_1} [Group G] {R K : Subgroup G} [R.Normal] [K.Normal] (hRK : R ≤ K) : (quotientMapOfLEHom hRK).ker = Subgroup.map (QuotientGroup.mk' R) K

The kernel of G/R -> G/K is the image of K in G/R.

theorem Q2Presentation.Induction.TargetTowerClosers.card_domain_eq_card_ker_mul_card_of_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (hf : Function.Surjective ⇑f) : Nat.card G = Nat.card ↥f.ker * Nat.card H

Cardinality of the middle quotient in a finite exact sequence.

theorem Q2Presentation.Induction.TargetTowerClosers.two_mul_card_le_of_subgroup_lt_top {G : Type u_1} [Group G] [Finite G] (K : Subgroup G) (hK : K < ⊤) : 2 * Nat.card ↥K ≤ Nat.card G

A proper subgroup of a finite group has at most half the cardinality.

Target quotient-map packet from canonical quotient equivalences

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

Framed quotient children whose underlying groups are equivalent to the canonical quotients Y/R and Y/K.

From this data the maps Y -> B, Y -> C, and B -> C, their kernels, surjectivity, and commutativity are theorem-level finite quotient facts.

• 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.targetQuotientMapsData_of_childEquivs {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (D : CentralCoverTargetQuotientChildEquivData B S) : CentralCoverTargetQuotientMapsData B S

The target quotient-map packet reassembled from canonical quotient equivalences for Y/R and Y/K.

Equations

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

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

Nonempty version of targetQuotientMapsData_of_childEquivs, matching the shape of the residual packet it refines.

Target tower cardinality packet from exact sequences on marked kernels

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

Concrete exact-sequence data on the marked kernels in the target tower.

The two restriction maps are the theorem-level content behind |L_B| |R| = |L_Y| and |L_B| = |ker(B -> C)| |L_C|; the final equivalence identifies ker(B -> C) with the abstract elementary layer M.

• topMarkedMap : ↥p.fst.LY →* ↥Q.middleChild.fst.LY
• topMarkedMap_surj : Function.Surjective ⇑self.topMarkedMap
• topMarkedKernelEquivR : ↥self.topMarkedMap.ker ≃* ↥S.Rsub
• middleMarkedMap : ↥Q.middleChild.fst.LY →* ↥Q.lowerChild.fst.LY
• middleMarkedMap_surj : Function.Surjective ⇑self.middleMarkedMap
• middleMarkedKernelEquiv : ↥self.middleMarkedMap.ker ≃* ↥Q.middleToLower.ker
• middleKernelEquivM : ↥Q.middleToLower.ker ≃* Multiplicative B.M

def Q2Presentation.Induction.targetTowerCardinalityData_of_markedExact {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetTowerMarkedExactData B S Q) : CentralCoverTargetTowerCardinalityData B S Q

Reassemble target-tower cardinalities from exact sequences on marked kernels.

Equations

• ⋯ = ⋯

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

Nonempty version of targetTowerCardinalityData_of_markedExact.

Integrated target quotient tower from concrete quotient witnesses

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

Refined residual: the framed quotient targets Y/R and Y/K are the canonical quotient groups from a fixed subgroup tower.

This is the remaining construction content behind eq:targettower after the quotient-map algebra has been proved theorem-level in this file.

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

Refined residual: exact sequences on the marked kernels of Y -> Y/R -> Y/K, including the identification of ker(Y/R -> Y/K) with the elementary module M.

The cardinal identities in CentralCoverTargetTowerCardinalityData are derived from this packet by theorem-level finite group cardinality lemmas.

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

Quotient-tower data assembled using canonical quotient maps and exact sequences, rather than the older quotient-map/cardinality residual axioms.

theorem Q2Presentation.Induction.centralCover_elementaryLowerTarget_from_targetClosers {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryLowerTarget B)

Lower-target data assembled from the theorem-level quotient-tower closer.

Proper-image kernel bounds and exact-sequence cardinalities

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

Concrete kernel-part subgroups together with the finite-group reason that each is at most half of the elementary layer.

• kernelPart : CentralCoverElementaryProperExactImageSubgroups T → Subgroup ↥T.middleToLower.ker
• kernelPart_proper (i : CentralCoverElementaryProperExactImageSubgroups T) : self.kernelPart i < ⊤
• middleKernelEquivM : ↥T.middleToLower.ker ≃* Multiplicative B.M

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

Reassemble the proper-image kernel-subgroup packet from concrete kernel parts, properness, and the kernel/module equivalence.

Equations

• Q2Presentation.Induction.elementaryProperImageKernelSubgroupData_of_boundData B T D = { kernelPart := D.kernelPart, kernelPart_bound := ⋯ }

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

Nonempty version of elementaryProperImageKernelSubgroupData_of_boundData.

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

Concrete exact sequence on each proper exact-image marked kernel: J ∩ L_B -> L_C, with kernel identified with the selected J ∩ M.

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

def Q2Presentation.Induction.elementaryProperImageExactSequenceData_of_restrictedExact {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) (D : CentralCoverElementaryProperImageRestrictedExactData B T K) : CentralCoverElementaryProperImageExactSequenceData B T K

Reassemble the proper-image exact-sequence cardinality packet from the restricted exact sequences on J ∩ L_B.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.centralCover_elementaryProperImageExactSequenceData_from_restrictedExact {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) : Nonempty (CentralCoverElementaryProperImageRestrictedExactData B T K) → Nonempty (CentralCoverElementaryProperImageExactSequenceData B T K)

Nonempty version of elementaryProperImageExactSequenceData_of_restrictedExact.

Integrated proper-image family from exact-sequence witnesses

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

Refined residual: for each proper exact-image subgroup, choose the concrete subgroup representing J ∩ M and prove it is proper in the elementary kernel.

The old packet's cardinal bound is then a theorem-level consequence of two_mul_card_le_of_subgroup_lt_top.

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

Refined residual: exact sequences 1 -> J ∩ M -> J ∩ L_B -> L_C -> 1 for the proper exact-image children.

The old child-measure equality is derived from these restricted exact sequences by theorem-level cardinality.

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

Proper-image cardinality data assembled from concrete kernel bounds and restricted exact sequences, rather than the older cardinal-only residual packets.

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

Proper-image family assembled from the target closer packets.

theorem Q2Presentation.Induction.centralCover_elementaryProperImageChildrenData_from_targetClosers {p : FramedPair} (B : MinimalBlock p) : Nonempty (CentralCoverElementaryProperImageChildrenData B)

Proper-image children assembled from the target closer packets.

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

Elementary-stage children assembled from the target closer packets.

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

Central-cover child data assembled with the target closer packets and the existing theorem-level scalar/phase strata.

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

Partial recipe assembled with the target closer packets.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_targetClosers {p : FramedPair} (B : MinimalBlock p) : Nonempty (CoverRealization B)

Cover realization assembled with target closer packets.