Proper-image restriction actual closers

This sidecar attacks the three proper-image semantic residuals from ProperImageRestrictionSemanticClosers.lean without editing the routed files.

The key point is to keep the restricted maps tied to the actual quotient map T.middleToLower. A single actual middle restriction packet records:

• the marked restriction L_B -> L_C;
• surjectivity of that marked restriction;
• agreement with the ambient quotient map B -> C;
• the kernel comparison between the marked restriction and the ambient kernel.

From that semantic packet the three proper-image packets are theorem-level: ker(B -> C) <= L_B, J ∩ L_B maps into L_C, and J ∩ L_B -> L_C is surjective for every proper exact-image subgroup J < B mapping onto C.

Actual marked restriction of T.middleToLower

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

The actual marked-kernel restriction of the elementary quotient map B -> C.

This is the semantic datum behind the proper-image exact sequence: the map is not arbitrary, but agrees with T.middleToLower on underlying group elements.

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

def Q2Presentation.Induction.elementaryProperImageActualMiddleKernelInclusion {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverElementaryProperImageActualMiddleRestrictionData B T) : ↥D.middleMarkedMap.ker →* ↥T.middleToLower.ker

The inclusion from the kernel of the actual marked restriction into the ambient kernel of T.middleToLower.

Equations

• Q2Presentation.Induction.elementaryProperImageActualMiddleKernelInclusion D = { toFun := fun (x : ↥D.middleMarkedMap.ker) => ⟨↑↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem Q2Presentation.Induction.elementaryProperImageActualMiddleKernelInclusion_injective {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverElementaryProperImageActualMiddleRestrictionData B T) : Function.Injective ⇑(elementaryProperImageActualMiddleKernelInclusion D)

theorem Q2Presentation.Induction.elementaryProperImageActualMiddleKernelInclusion_surjective {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverElementaryProperImageActualMiddleRestrictionData B T) : Function.Surjective ⇑(elementaryProperImageActualMiddleKernelInclusion D)

Since the actual kernel inclusion is injective and the marked and ambient kernels are equivalent, the inclusion is onto. This is the finite-group step that turns the marked-restriction kernel comparison into ker(B -> C) <= L_B.

The three semantic packets, proved from the actual restriction

def Q2Presentation.Induction.elementaryProperImageMiddleKernelMarkedData_of_actualMiddleRestriction {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverElementaryProperImageActualMiddleRestrictionData B T) : CentralCoverElementaryProperImageMiddleKernelMarkedData B T

The ambient middle kernel is marked because it is the finite image of the actual marked-restriction kernel.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.elementaryProperImageMapsToLowerMarkedData_of_actualMiddleRestriction {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverElementaryProperImageActualMiddleRestrictionData B T) : CentralCoverElementaryProperImageMapsToLowerMarkedData B T

The actual quotient map sends every J ∩ L_B into L_C, because it agrees with the marked restriction L_B -> L_C.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.elementaryProperImageRestrictedSurjData_of_actualMiddleRestriction {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverElementaryProperImageActualMiddleRestrictionData B T) : CentralCoverElementaryProperImageRestrictedSurjData B T

The restricted proper-image map J ∩ L_B -> L_C is surjective.

Given y ∈ L_C, choose a marked lift x0 ∈ L_B using the actual marked restriction and choose j ∈ J using the proper-image assumption J -> C is onto. Their quotient lies in ker(B -> C), hence in L_B; therefore j is itself in L_B.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.elementaryProperImageCanonicalRestrictionData_of_actualMiddleRestriction {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverElementaryProperImageActualMiddleRestrictionData B T) : CentralCoverElementaryProperImageCanonicalRestrictionData B T

Reassemble the canonical restriction packet from the actual middle restriction, with no use of the three old semantic residual axioms.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.centralCover_elementaryProperImageMiddleKernelMarkedData_from_actualMiddleRestriction {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageActualMiddleRestrictionData B T) → Nonempty (CentralCoverElementaryProperImageMiddleKernelMarkedData B T)

theorem Q2Presentation.Induction.centralCover_elementaryProperImageMapsToLowerMarkedData_from_actualMiddleRestriction {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageActualMiddleRestrictionData B T) → Nonempty (CentralCoverElementaryProperImageMapsToLowerMarkedData B T)

theorem Q2Presentation.Induction.centralCover_elementaryProperImageRestrictedSurjData_from_actualMiddleRestriction {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageActualMiddleRestrictionData B T) → Nonempty (CentralCoverElementaryProperImageRestrictedSurjData B T)

theorem Q2Presentation.Induction.centralCover_elementaryProperImageCanonicalRestrictionData_from_actualMiddleRestriction {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Nonempty (CentralCoverElementaryProperImageActualMiddleRestrictionData B T) → Nonempty (CentralCoverElementaryProperImageCanonicalRestrictionData B T)

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

Proper-image cardinality data from the actual middle restriction and the existing middle-kernel equivalence. The downstream kernel calculation is the one in ProperImageExactClosers: the restricted-map kernel is the literal J ∩ ker(B -> C), then identified with J ∩ M.

Compatibility with the existing target-marked quotient packets

def Q2Presentation.Induction.elementaryProperImageActualMiddleRestrictionData_of_targetMiddleRestriction {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (C : CentralCoverTargetTowerCardinalityData B S Q) (D : CentralCoverTargetMiddleMarkedRestrictionData B S Q) (K : CentralCoverTargetMiddleMarkedKernelOfRestrictionData B S Q D) : CentralCoverElementaryProperImageActualMiddleRestrictionData B (elementaryQuotientTowerData_of_targetPackets B S Q C)

The target-marked quotient restriction packets produce the actual middle restriction packet for the elementary tower assembled from target packets.

Equations

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

theorem Q2Presentation.Induction.centralCover_elementaryProperImageCanonicalRestrictionData_from_targetMiddleRestriction {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (C : CentralCoverTargetTowerCardinalityData B S Q) (D : CentralCoverTargetMiddleMarkedRestrictionData B S Q) (K : CentralCoverTargetMiddleMarkedKernelOfRestrictionData B S Q D) : Nonempty (CentralCoverElementaryProperImageCanonicalRestrictionData B (elementaryQuotientTowerData_of_targetPackets B S Q C))

theorem Q2Presentation.Induction.centralCover_elementaryProperImageCanonicalRestrictionData_from_targetMarkedQuotientClosers {p : FramedPair} (B : MinimalBlock p) (S : CentralCoverTargetSubgroupTowerData B) (Q : CentralCoverTargetQuotientMapsData B S) (C : CentralCoverTargetTowerCardinalityData B S Q) : Nonempty (CentralCoverElementaryProperImageCanonicalRestrictionData B (elementaryQuotientTowerData_of_targetPackets B S Q C))

Closed target-packet version: the proper-image canonical restriction for a tower assembled from target packets follows from the existing target middle marked restriction packets, not from the three old proper-image residual names.