Marked canonical quotient closers

This sidecar refines the current target quotient/marked exactness layer used in the final Section 8 route.

Manuscript anchors:

• Section 7, eq:targettower: Y -> B = Y/R -> C = Y/K and M = K/R;
• Section 8, eq:Mstage/eq:Mdescent: exactness of L_Y -> L_B -> L_C and the middle-kernel identification.

The current quotient-child API records equivalences with the quotient groups, but it still does not state how the quotient targets' marked kernels are the images of the original marked kernel. Accordingly, this file replaces the coarser target residual names by smaller packets:

• middle and lower canonical quotient targets are separate;
• marked maps are restrictions of the ambient quotient maps, with agreement fields;
• marked-kernel identifications are separate from the marked map construction;
• the kernel-image equivalence is split into a hom and a bijectivity packet.

Canonical quotient targets, split by quotient level

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

The middle framed target canonically realizing Y/R.

• middleChild : FramedPair
• middleEquiv : p.fst.Y ⧸ D.Rsub ≃* self.middleChild.fst.Y

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

The lower framed target canonically realizing Y/K.

• lowerChild : FramedPair
• lowerEquiv : p.fst.Y ⧸ D.Ksub ≃* self.lowerChild.fst.Y

def Q2Presentation.Induction.targetCanonicalQuotientData_of_middleLower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetCanonicalMiddleQuotientData B D) (L : CentralCoverTargetCanonicalLowerQuotientData B D) : CentralCoverTargetCanonicalQuotientData B D

Reassemble the current canonical quotient-target packet from the two quotient levels.

Equations

• Q2Presentation.Induction.targetCanonicalQuotientData_of_middleLower B D M L = { middleChild := M.middleChild, lowerChild := L.lowerChild, middleEquiv := M.middleEquiv, lowerEquiv := L.lowerEquiv }

axiom Q2Presentation.Induction.centralCover_targetCanonicalMiddleQuotientData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetCanonicalMiddleQuotientData B D)

Smaller residual: construct the canonical middle quotient target Y/R.

axiom Q2Presentation.Induction.centralCover_targetCanonicalLowerQuotientData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetCanonicalLowerQuotientData B D)

Smaller residual: construct the canonical lower quotient target Y/K.

theorem Q2Presentation.Induction.centralCover_targetCanonicalQuotientData_from_markedQuotientClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetCanonicalQuotientData B D)

Replacement for centralCover_targetCanonicalQuotientData, assembled from separate middle and lower quotient target packets.

theorem Q2Presentation.Induction.centralCover_targetQuotientChildConcreteData_from_markedQuotientClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetQuotientChildConcreteData B (targetSubgroupTowerData_of_concrete B D))

Quotient-child concrete data from the split canonical quotient packets.

Top marked-kernel exact sequence, split into restriction and kernel

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

The marked map L_Y -> L_B is the restriction of the ambient quotient map Y -> B = Y/R.

• topMarkedMap : ↥p.fst.LY →* ↥Q.middleChild.fst.LY
• topMarkedMap_surj : Function.Surjective ⇑self.topMarkedMap
• topMarkedMap_agrees (x : ↥p.fst.LY) : ↑(self.topMarkedMap x) = Q.topToMiddle ↑x

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

The kernel of the restricted top marked map is R.

• topMarkedKernelEquivR : ↥D.topMarkedMap.ker ≃* ↥S.Rsub

def Q2Presentation.Induction.targetTopMarkedMapData_of_restriction {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetTopMarkedRestrictionData B S Q) : CentralCoverTargetTopMarkedMapData B S Q

Equations

• Q2Presentation.Induction.targetTopMarkedMapData_of_restriction B S Q D = { topMarkedMap := D.topMarkedMap, topMarkedMap_surj := ⋯ }

def Q2Presentation.Induction.targetTopMarkedKernelData_of_restriction {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetTopMarkedRestrictionData B S Q) (K : CentralCoverTargetTopMarkedKernelOfRestrictionData B S Q D) : CentralCoverTargetTopMarkedKernelData B S Q (targetTopMarkedMapData_of_restriction B S Q D)

Equations

• Q2Presentation.Induction.targetTopMarkedKernelData_of_restriction B S Q D K = { topMarkedKernelEquivR := K.topMarkedKernelEquivR }

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

Smaller residual: construct the top marked restriction map and prove it is surjective, together with agreement with the ambient quotient map.

axiom Q2Presentation.Induction.centralCover_targetTopMarkedKernelOfRestrictionData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetTopMarkedRestrictionData B S Q) : Nonempty (CentralCoverTargetTopMarkedKernelOfRestrictionData B S Q D)

Smaller residual: identify the kernel of the selected top marked restriction map with R.

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

Top marked exactness assembled without the old top marked map/kernel residual names.

Middle marked-kernel exact sequence, split into restriction and kernel

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

The marked map L_B -> L_C is the restriction of the ambient quotient map B -> C.

• middleMarkedMap : ↥Q.middleChild.fst.LY →* ↥Q.lowerChild.fst.LY
• middleMarkedMap_surj : Function.Surjective ⇑self.middleMarkedMap
• middleMarkedMap_agrees (x : ↥Q.middleChild.fst.LY) : ↑(self.middleMarkedMap x) = Q.middleToLower ↑x

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

The kernel of the restricted middle marked map is the ambient middle kernel.

• middleMarkedKernelEquiv : ↥D.middleMarkedMap.ker ≃* ↥Q.middleToLower.ker

def Q2Presentation.Induction.targetMiddleMarkedMapData_of_restriction {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleMarkedRestrictionData B S Q) : CentralCoverTargetMiddleMarkedMapData B S Q

Equations

• Q2Presentation.Induction.targetMiddleMarkedMapData_of_restriction B S Q D = { middleMarkedMap := D.middleMarkedMap, middleMarkedMap_surj := ⋯ }

def Q2Presentation.Induction.targetMiddleMarkedKernelData_of_restriction {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleMarkedRestrictionData B S Q) (K : CentralCoverTargetMiddleMarkedKernelOfRestrictionData B S Q D) : CentralCoverTargetMiddleMarkedKernelData B S Q (targetMiddleMarkedMapData_of_restriction B S Q D)

Equations

• Q2Presentation.Induction.targetMiddleMarkedKernelData_of_restriction B S Q D K = { middleMarkedKernelEquiv := K.middleMarkedKernelEquiv }

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

Smaller residual: construct the middle marked restriction map and prove it is surjective, together with agreement with the ambient quotient map.

axiom Q2Presentation.Induction.centralCover_targetMiddleMarkedKernelOfRestrictionData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleMarkedRestrictionData B S Q) : Nonempty (CentralCoverTargetMiddleMarkedKernelOfRestrictionData B S Q D)

Smaller residual: identify the kernel of the middle marked restriction map with the ambient kernel of B -> C.

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

Middle marked exactness assembled without the old middle marked map/kernel residual names.

Middle kernel image, split into a hom and bijectivity

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

A canonical comparison hom from ker(B -> C) to the quotient image of K inside Y/R.

• middleKernelImageHom : ↥Q.middleToLower.ker →* ↥(Subgroup.map (QuotientGroup.mk' S.Rsub) S.Ksub)

structure Q2Presentation.Induction.CentralCoverTargetMiddleKernelImageBijectiveData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleKernelImageHomData B S Q) : Prop

The middle-kernel comparison hom is bijective.

• middleKernelImageHom_bijective : Function.Bijective ⇑D.middleKernelImageHom

def Q2Presentation.Induction.targetMiddleKernelImageData_of_homBijective {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleKernelImageHomData B S Q) (H : CentralCoverTargetMiddleKernelImageBijectiveData B S Q D) : CentralCoverTargetMiddleKernelImageData B S Q

Reassemble the current kernel-image equivalence from a comparison hom and bijectivity.

Equations

• Q2Presentation.Induction.targetMiddleKernelImageData_of_homBijective B S Q D H = { middleKernelImageEquiv := MulEquiv.ofBijective D.middleKernelImageHom ⋯ }

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

Smaller residual: construct the comparison hom ker(B -> C) -> K/R.

axiom Q2Presentation.Induction.centralCover_targetMiddleKernelImageBijectiveData {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (D : CentralCoverTargetMiddleKernelImageHomData B S Q) : Nonempty (CentralCoverTargetMiddleKernelImageBijectiveData B S Q D)

Smaller residual: prove the comparison hom ker(B -> C) -> K/R is bijective.

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

Middle-kernel image data assembled without the old image residual name.

theorem Q2Presentation.Induction.centralCover_targetMiddleKernelIdentificationData_from_markedQuotientClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetQuotientMapsData B (targetSubgroupTowerData_of_concrete B D)) : Nonempty (CentralCoverTargetMiddleKernelIdentificationData B (targetSubgroupTowerData_of_concrete B D) Q)

Middle-kernel identification assembled from the split kernel-image packets and concrete K/R ~= M provenance.

Canonical quotient tower and final route

theorem Q2Presentation.Induction.centralCover_targetCanonicalQuotientTowerData_from_selfGroupTower_markedQuotientClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (R : MinimalBlockPreheadExtraspecialRadicalData F) : Nonempty (CentralCoverTargetCanonicalQuotientTowerData (G.toMinimalBlock h F A R))

Canonical target quotient data for the minimal block built from a Section 7 group tower, routed through the split quotient and marked exactness packets in this file.

theorem Q2Presentation.Induction.centralCover_realization_proven_fine_from_selfGroupTowerMarkedQuotientClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (R : MinimalBlockPreheadExtraspecialRadicalData F) : Nonempty (CoverRealization (G.toMinimalBlock h F A R))

Cover realization for the specific block produced by a Section 7 group tower, using the marked canonical quotient route above.

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_targetMarkedQuotientClosers (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Nonterminal branch routed through the split marked canonical quotient layer.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_targetMarkedQuotientClosers (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

Recursive branch using the split marked canonical quotient nonterminal route.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_targetMarkedQuotientClosers (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

Recursion step using the split marked canonical quotient nonterminal branch.

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_targetMarkedQuotientClosers (p : FramedPair) : framedCountA p = framedCountQ p

Boundary-framed counts equal through the split marked canonical quotient route.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_targetMarkedQuotientClosers (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Equal finite surjection counts through the split marked canonical quotient route.