Proper-image exact closers

This sidecar refines the Section 8 proper-image packets from TargetTowerConcreteClosers.lean without editing existing files.

Manuscript anchors:

• eq:Mstage: partition the elementary lifts by exact image J < B;
• eq:Mdescent: use the exact sequence 1 -> J ∩ M -> J ∩ L_B -> L_C -> 1;
• proper-image subtraction: the exact-image kernel is the literal intersection J ∩ ker(B -> C), identified with J ∩ M.

The file avoids the three residual axiom names introduced in TargetTowerConcreteClosers.lean by proving the literal-kernel packet from the existing middle-kernel equivalence, and by replacing the arbitrary restricted map/kernel packets with a canonical restriction witness.

Literal proper-image kernels from the middle-kernel equivalence

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

The literal-kernel packet is just the already isolated identification ker(B -> C) ≃ M. The literal subgroups themselves are theorem-level: elementaryProperImageLiteralKernelPart T i = J ∩ ker(B -> C).

Equations

• Q2Presentation.Induction.elementaryProperImageLiteralKernelData_of_middleKernelEquiv D = { middleKernelEquivM := D.middleKernelEquivM }

theorem Q2Presentation.Induction.centralCover_elementaryProperImageLiteralKernelData_from_middleKernel {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : ↥T.middleToLower.ker ≃* Multiplicative B.M) : Nonempty (CentralCoverElementaryProperImageLiteralKernelData B T)

Direct version of the literal-kernel closer: once ker(B -> C) ≃ M is supplied, the packet is just that equivalence.

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

Replacement for the literal-kernel residual, routed through the earlier middle-kernel equivalence packet rather than the TargetTowerConcreteClosers proper-image residual.

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

Closed form using the existing middle-kernel equivalence residual. This theorem does not use the proper-image literal-kernel residual name.

Canonical restricted maps on J ∩ L_B

def Q2Presentation.Induction.elementaryProperImageRestrictedDomainVal {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {i : CentralCoverElementaryProperExactImageSubgroups T} (x : ↥(T.middleChild.fst.LY.subgroupOf ↑i)) : T.middleChild.fst.Y

Underlying element of the marked-kernel intersection J ∩ L_B.

Equations

• Q2Presentation.Induction.elementaryProperImageRestrictedDomainVal x = ↑↑x

structure Q2Presentation.Induction.CentralCoverElementaryProperImageCanonicalRestrictionData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Prop

Manuscript-faithful data saying that the quotient map B -> C restricts to the marked kernels in the proper exact-image strata.

The first field records the tower fact ker(B -> C) <= L_B, used to identify the kernel of the restricted map with the literal subgroup J ∩ ker(B -> C). The second and third fields say that the actual quotient map sends J ∩ L_B into L_C and is onto L_C.

• middleKernel_le_marked (z : ↥T.middleToLower.ker) : ↑z ∈ T.middleChild.fst.LY
• mapsToLowerMarked (i : CentralCoverElementaryProperExactImageSubgroups T) (x : ↥(T.middleChild.fst.LY.subgroupOf ↑i)) : T.middleToLower (elementaryProperImageRestrictedDomainVal x) ∈ T.lowerChild.fst.LY
• restricted_surj (i : CentralCoverElementaryProperExactImageSubgroups T) (y : ↥T.lowerChild.fst.LY) : ∃ (x : ↥(T.middleChild.fst.LY.subgroupOf ↑i)), T.middleToLower (elementaryProperImageRestrictedDomainVal x) = ↑y

def Q2Presentation.Induction.elementaryProperImageCanonicalRestrictedMap {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverElementaryProperImageCanonicalRestrictionData B T) (i : CentralCoverElementaryProperExactImageSubgroups T) : ↥(T.middleChild.fst.LY.subgroupOf ↑i) →* ↥T.lowerChild.fst.LY

The canonical restricted map J ∩ L_B -> L_C induced by B -> C.

Equations

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

def Q2Presentation.Induction.elementaryProperImageRestrictedMapsData_of_canonicalRestriction {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) (D : CentralCoverElementaryProperImageCanonicalRestrictionData B T) : CentralCoverElementaryProperImageRestrictedMapsData B T K

The canonical restrictions supply the restricted-map packet.

Equations

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

theorem Q2Presentation.Induction.centralCover_elementaryProperImageRestrictedMapsData_from_canonicalRestriction {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) : Nonempty (CentralCoverElementaryProperImageCanonicalRestrictionData B T) → Nonempty (CentralCoverElementaryProperImageRestrictedMapsData B T K)

Nonempty reassembly of the restricted-map packet from the canonical restriction witness.

@[reducible, inline]

abbrev Q2Presentation.Induction.CentralCoverElementaryProperImageMiddleRestrictionAgreementData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Prop

Alias for the canonical restriction witness, matching the manuscript point that the restricted maps are induced by T.middleToLower.

Equations

• Q2Presentation.Induction.CentralCoverElementaryProperImageMiddleRestrictionAgreementData B T = Q2Presentation.Induction.CentralCoverElementaryProperImageCanonicalRestrictionData B T

theorem Q2Presentation.Induction.centralCover_elementaryProperImageRestrictedMapsData_from_middleAgreement {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) : Nonempty (CentralCoverElementaryProperImageMiddleRestrictionAgreementData B T) → Nonempty (CentralCoverElementaryProperImageRestrictedMapsData B T K)

Pro-guided name for reassembling restricted maps from the middle-map agreement witness.

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

Semantic agreement: a restricted-map packet is actually the restriction of T.middleToLower on every proper exact-image marked kernel.

• restrictedMap_agrees (i : CentralCoverElementaryProperExactImageSubgroups T) (x : ↥(T.middleChild.fst.LY.subgroupOf ↑i)) : ↑((Maps.restrictedMap i) x) = T.middleToLower (elementaryProperImageRestrictedDomainVal x)

def Q2Presentation.Induction.elementaryProperImageRestrictedMapsAgreementData_of_canonicalRestriction {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) (D : CentralCoverElementaryProperImageCanonicalRestrictionData B T) : CentralCoverElementaryProperImageRestrictedMapsAgreementData B T K (elementaryProperImageRestrictedMapsData_of_canonicalRestriction B T K D)

The canonical restricted maps agree definitionally with T.middleToLower.

Equations

• ⋯ = ⋯

Kernel identification for the canonical restricted maps

def Q2Presentation.Induction.elementaryProperImageCanonicalRestrictedKernelEquiv {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverElementaryProperImageCanonicalRestrictionData B T) (i : CentralCoverElementaryProperExactImageSubgroups T) : ↥(elementaryProperImageCanonicalRestrictedMap D i).ker ≃* ↥(elementaryProperImageLiteralKernelPart T i)

The kernel of the canonical restricted map is the literal intersection J ∩ ker(B -> C).

Equations

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

def Q2Presentation.Induction.elementaryProperImageRestrictedKernelIdentificationData_of_canonicalRestriction {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Dlit : CentralCoverElementaryProperImageLiteralKernelData B T) (D : CentralCoverElementaryProperImageCanonicalRestrictionData B T) : have DkBound := elementaryProperImageKernelBoundData_of_literalIntersections B T Dlit; have K := elementaryProperImageKernelSubgroupData_of_boundData B T DkBound; have Maps := elementaryProperImageRestrictedMapsData_of_canonicalRestriction B T K D; CentralCoverElementaryProperImageRestrictedKernelIdentificationData B T K Maps

Kernel-identification packet for the canonical restricted maps and the literal kernel-subgroup choice.

Equations

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

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

Agreement that a selected kernel-part packet uses the literal subgroup J ∩ ker(B -> C).

• kernelPart_eq_literal (i : CentralCoverElementaryProperExactImageSubgroups T) : K.kernelPart i = elementaryProperImageLiteralKernelPart T i

def Q2Presentation.Induction.elementaryProperImageLiteralKernelAgreementData_of_literalIntersections {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (Dlit : CentralCoverElementaryProperImageLiteralKernelData B T) : have DkBound := elementaryProperImageKernelBoundData_of_literalIntersections B T Dlit; have K := elementaryProperImageKernelSubgroupData_of_boundData B T DkBound; CentralCoverElementaryProperImageLiteralKernelAgreementData B T K

The kernel-subgroup packet built from literal intersections has the required literal-kernel agreement by construction.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.elementaryProperImageRestrictedKernelEquiv_of_agreements {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {K : CentralCoverElementaryProperImageKernelSubgroupData B T} {Maps : CentralCoverElementaryProperImageRestrictedMapsData B T K} (middleKernel_le_marked : ∀ (z : ↥T.middleToLower.ker), ↑z ∈ T.middleChild.fst.LY) (MapAgree : CentralCoverElementaryProperImageRestrictedMapsAgreementData B T K Maps) (KerAgree : CentralCoverElementaryProperImageLiteralKernelAgreementData B T K) (i : CentralCoverElementaryProperExactImageSubgroups T) : ↥(Maps.restrictedMap i).ker ≃* ↥(K.kernelPart i)

If the maps agree with T.middleToLower, and the selected kernel parts are the literal intersections, then the restricted-map kernels are exactly J ∩ M.

Equations

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

theorem Q2Presentation.Induction.centralCover_elementaryProperImageRestrictedKernelIdentificationData_from_literalKernel {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (K : CentralCoverElementaryProperImageKernelSubgroupData B T) (Maps : CentralCoverElementaryProperImageRestrictedMapsData B T K) (middleKernel_le_marked : ∀ (z : ↥T.middleToLower.ker), ↑z ∈ T.middleChild.fst.LY) (MapAgree : CentralCoverElementaryProperImageRestrictedMapsAgreementData B T K Maps) (KerAgree : CentralCoverElementaryProperImageLiteralKernelAgreementData B T K) : Nonempty (CentralCoverElementaryProperImageRestrictedKernelIdentificationData B T K Maps)

Pro-guided kernel-identification reassembly from semantic map agreement and literal J ∩ M agreement.

Reassembly without the three TargetTowerConcreteClosers residual names

theorem Q2Presentation.Induction.centralCover_elementaryProperImageCardinalityData_from_exactClosers {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverMiddleKernelEquivData B T) → Nonempty (CentralCoverElementaryProperImageCanonicalRestrictionData B T) → Nonempty (CentralCoverElementaryProperImageCardinalityData B T)

Proper-image cardinality data from the middle-kernel equivalence and the canonical restricted exactness witness. The proof route avoids the three proper-image residual axiom names from TargetTowerConcreteClosers.lean.

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

Closed proper-image cardinality theorem using the existing middle-kernel equivalence residual plus a single canonical restriction residual.

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

Strongest closed reassembly theorem in this sidecar. Its axiom closure uses centralCover_middleKernelEquivData and the new canonical restriction residual, not the three proper-image residual names from TargetTowerConcreteClosers.lean.

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

Proper-image family data assembled through the exact closers in this file.