Candidate exact-image residual refinements

This sidecar refines the three candidate exact-image packets isolated in CandidateLiftPartitionCardinality.lean.

The current tower API exposes the finite quotient maps in the target tower, but not enough boundary-frame compatibility to construct the candidate exact-image maps outright. The packets below therefore keep the missing data concrete:

• a surjective profinite postcomposition map from the top target to the middle quotient, together with the boundary-frame compatibility needed to send top boundary-framed maps to middle boundary-framed maps;
• a finite obstruction index, its map to the middle exact-image source, and the R-valued obstruction map on that same index;
• the finite cardinality statement whose choice-free content is the Frattini exact-image lift partition.

Exact-image base quotient

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

Boundary-compatible postcomposition through the realized quotient Y -> B = Y/R.

This is the concrete datum currently missing from CentralCoverElementaryQuotientTowerData: a profinite morphism induced by the finite quotient map, its surjectivity, and the exact boundary-frame equality needed to postcompose a candidate top exact-image map into the middle boundary-framed source set.

• topToMiddleHom : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of p.fst.Y) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of T.middleChild.fst.Y)
• topToMiddle_surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.topToMiddleHom)
• topToMiddle_agrees (y : p.fst.Y) : (ProfiniteGrp.Hom.hom self.topToMiddleHom) y = T.topToMiddle y
• boundary_compat (f : centralCoverCandidateSource) (γ : ↑GammaA.toProfinite.toTop) : T.middleChild.fst.qYMap ((ProfiniteGrp.Hom.hom self.topToMiddleHom) ((ProfiniteGrp.Hom.hom (↑f).hom) γ)) = (ProfiniteGrp.Hom.hom T.middleChild.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) γ)

def Q2Presentation.Induction.CentralCoverCandidateBoundaryPostcompData.baseOfTop {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateBoundaryPostcompData B T) : centralCoverCandidateSource → centralCoverCandidateMiddleSource T

Postcompose a top candidate exact-image map with the boundary-compatible quotient map to obtain a middle candidate exact-image map.

Equations

• D.baseOfTop f = ⟨{ hom := CategoryTheory.CategoryStruct.comp (↑f).hom D.topToMiddleHom, surj := ⋯ }, ⋯⟩

def Q2Presentation.Induction.CentralCoverCandidateBoundaryPostcompData.exactImageBaseQuotient {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateBoundaryPostcompData B T) : CentralCoverCandidateExactImageBaseQuotientData B T

Reassemble the original base-quotient packet from concrete boundary-compatible postcomposition data.

Equations

• D.exactImageBaseQuotient = { baseOfTop := D.baseOfTop }

theorem Q2Presentation.Induction.centralCover_candidateExactImageBaseQuotientData_of_boundaryPostcomp {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateBoundaryPostcompData B T) : Nonempty (CentralCoverCandidateExactImageBaseQuotientData B T)

Replacement theorem for centralCover_candidateExactImageBaseQuotientData, conditional on the concrete boundary-compatible postcomposition packet.

Obstruction index to middle exact-image base

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

The finite exact-image obstruction index, with its forgetful map to the middle exact-image source set.

This separates the index and its base map from the obstruction function itself.

• X : Type
• finX : Fintype self.X
• indexToBase : self.X → centralCoverCandidateMiddleSource T

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

The R-valued obstruction map on a fixed candidate exact-image index.

• obstruction : I.X → B.obstructionSpace

def Q2Presentation.Induction.CentralCoverCandidateObstructionIndexBaseData.sourceObstructionData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (I : CentralCoverCandidateObstructionIndexBaseData B T) (O : CentralCoverCandidateObstructionMapData B T I) : CentralCoverSourceObstructionData B centralCoverCandidateSource

Reassemble source obstruction data from a fixed finite index and obstruction map.

Equations

• I.sourceObstructionData O = { X := I.X, finX := I.finX, o := O.obstruction }

def Q2Presentation.Induction.CentralCoverCandidateObstructionIndexBaseData.obstructionIndexToBase {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (I : CentralCoverCandidateObstructionIndexBaseData B T) (O : CentralCoverCandidateObstructionMapData B T I) : CentralCoverCandidateObstructionIndexToBaseMapData B T

Reassemble the original obstruction-index-to-base packet from the split finite index/base map and obstruction map.

Equations

• I.obstructionIndexToBase O = { O := I.sourceObstructionData O, indexToBase := fun (x : { x : (I.sourceObstructionData O).X // (I.sourceObstructionData O).o x = 0 }) => I.indexToBase ↑x }

theorem Q2Presentation.Induction.centralCover_candidateObstructionIndexToBaseMapData_of_indexBase {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (I : CentralCoverCandidateObstructionIndexBaseData B T) (O : CentralCoverCandidateObstructionMapData B T I) : Nonempty (CentralCoverCandidateObstructionIndexToBaseMapData B T)

Replacement theorem for centralCover_candidateObstructionIndexToBaseMapData, conditional on the finite obstruction index/base map and its obstruction map.

Frattini exact-image partition

structure Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageCardinalityData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (O : CentralCoverSourceObstructionData B centralCoverCandidateSource) (Z : CentralCoverSourceCocycleData B) (F : CentralCoverSourceLiftFibers B centralCoverCandidateSource O Z) : Prop

Cardinal form of the candidate Frattini exact-image partition for a fixed obstruction datum, cocycle datum, and lift-fibre family.

This is the exact finite statement needed to recover the partition by liftPartition_of_cardinality, using the already-proved finiteness of the candidate boundary-framed source.

• card_eq : Nat.card centralCoverCandidateSource = Nat.card ((x : { x : O.X // O.o x = 0 }) × F.Lift x)

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageCardinalityData.liftPartitionCardinality {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {O : CentralCoverSourceObstructionData B centralCoverCandidateSource} {Z : CentralCoverSourceCocycleData B} {F : CentralCoverSourceLiftFibers B centralCoverCandidateSource O Z} (D : CentralCoverCandidateFrattiniExactImageCardinalityData B T O Z F) : CentralCoverSourceLiftPartitionCardinality B centralCoverCandidateSource O Z F

Convert the candidate Frattini cardinal statement into the existing generic lift-partition cardinality interface.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageCardinalityData.frattiniExactImage {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {O : CentralCoverSourceObstructionData B centralCoverCandidateSource} {Z : CentralCoverSourceCocycleData B} {F : CentralCoverSourceLiftFibers B centralCoverCandidateSource O Z} (D : CentralCoverCandidateFrattiniExactImageCardinalityData B T O Z F) : CentralCoverCandidateFrattiniExactImageSurjectivityData B T O Z F

Recover the Frattini exact-image partition from its finite cardinal form.

Equations

• D.frattiniExactImage = { partition := Q2Presentation.Induction.liftPartition_of_cardinality B Q2Presentation.Induction.centralCoverCandidateSource O Z F ⋯ }

theorem Q2Presentation.Induction.centralCover_candidateFrattiniExactImageSurjectivityData_of_cardinality {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (O : CentralCoverSourceObstructionData B centralCoverCandidateSource) (Z : CentralCoverSourceCocycleData B) (F : CentralCoverSourceLiftFibers B centralCoverCandidateSource O Z) (D : CentralCoverCandidateFrattiniExactImageCardinalityData B T O Z F) : Nonempty (CentralCoverCandidateFrattiniExactImageSurjectivityData B T O Z F)

Replacement theorem for centralCover_candidateFrattiniExactImageSurjectivityData, conditional on the finite cardinality statement for this exact obstruction/fibre packet.

Full candidate semantic packet from refined residuals

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

All refined candidate exact-image residuals for a realized elementary tower.

The affine fibre torsor remains theorem-level in CandidateLiftPartitionCardinality.lean; this packet only contains the three exact-image pieces still missing from the current API.

• basePostcomp : CentralCoverCandidateBoundaryPostcompData B T
• obstructionIndexBase : CentralCoverCandidateObstructionIndexBaseData B T
• obstructionMap : CentralCoverCandidateObstructionMapData B T self.obstructionIndexBase
• frattiniCardinality : let O := self.obstructionIndexBase.sourceObstructionData self.obstructionMap; let A := centralCover_candidateCanonicalAffineFiberTorsorData B O; CentralCoverCandidateFrattiniExactImageCardinalityData B T O A.Z A.F

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

Refined residual: the concrete candidate exact-image data for a fixed realized elementary tower.

This single packet replaces the three older candidate exact-image packet axioms in the final route. Its fields are concrete maps, finite indices, obstruction maps, and cardinality statements; there are no bare Prop marker fields.

def Q2Presentation.Induction.CentralCoverCandidateExactImageResidualData.obstructionIndexToBase {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateExactImageResidualData B T) : CentralCoverCandidateObstructionIndexToBaseMapData B T

The obstruction-index-to-base packet reassembled from the refined residual.

Equations

• D.obstructionIndexToBase = D.obstructionIndexBase.obstructionIndexToBase D.obstructionMap

def Q2Presentation.Induction.CentralCoverCandidateExactImageResidualData.affineFiberTorsor {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateExactImageResidualData B T) : CentralCoverCandidateAffineFiberTorsorData B D.obstructionIndexToBase.O

The canonical affine fibre torsor attached to the refined obstruction data.

Equations

• D.affineFiberTorsor = Q2Presentation.Induction.centralCover_candidateCanonicalAffineFiberTorsorData B D.obstructionIndexToBase.O

def Q2Presentation.Induction.CentralCoverCandidateExactImageResidualData.frattiniExactImage {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateExactImageResidualData B T) : CentralCoverCandidateFrattiniExactImageSurjectivityData B T D.obstructionIndexToBase.O D.affineFiberTorsor.Z D.affineFiberTorsor.F

The Frattini exact-image partition reassembled from the refined cardinal residual.

Equations

• D.frattiniExactImage = Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageCardinalityData.frattiniExactImage ⋯

def Q2Presentation.Induction.CentralCoverCandidateExactImageResidualData.rLiftSemanticData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} (D : CentralCoverCandidateExactImageResidualData B T) : CentralCoverCandidateRLiftSemanticData B T

Reassemble the existing semantic R-lift packet from the refined candidate exact-image residuals.

Equations

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

theorem Q2Presentation.Induction.centralCover_candidateRLiftSemanticData_of_exactImageResiduals {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateExactImageResidualData B T) : Nonempty (CentralCoverCandidateRLiftSemanticData B T)

Refined replacement for centralCover_candidateRLiftSemanticData, using only the concrete candidate exact-image residual packet from this sidecar.

theorem Q2Presentation.Induction.centralCover_candidateLiftPartitionData_of_exactImageResiduals {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateExactImageResidualData B T) : Nonempty (CentralCoverCandidateLiftPartitionData B)

Coherent candidate lift-partition data reassembled from the refined candidate exact-image residuals.