Concrete candidate exact-image closers

This sidecar pushes the four candidate-side Section 8 packets from CandidateExactImagePacketClosers.lean down to smaller theorem-facing data.

The split follows reference/q2_manuscript.tex, Section 8:

• the finite quotient map Y -> B = Y/R supplies the profinite postcomposition morphism; only the boundary-frame compatibility remains as semantic data (lem:covertransform);
• the exact-image base index can be the finite set of middle boundary-framed exact-image maps itself (def:Xgamma);
• the obstruction map is an explicit evaluation on that finite index (lem:obstructionseparation);
• the Frattini/cardinality packet follows from an actual exact-image equivalence/partition (prop:finalfourier), rather than a bare cardinal equality.

No theorem below uses the four packet axioms from CandidateExactImagePacketClosers.lean.

Finite quotient postcomposition

def Q2Presentation.Induction.centralCover_candidateFiniteQuotientPostcompHom {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of p.fst.Y) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of T.middleChild.fst.Y)

The profinite morphism induced by the finite quotient map Y -> B = Y/R already present in CentralCoverElementaryQuotientTowerData.

Equations

• Q2Presentation.Induction.centralCover_candidateFiniteQuotientPostcompHom B T = ProfiniteGrp.ofFiniteGrpHom (FiniteGrp.ofHom T.topToMiddle)

@[simp]

theorem Q2Presentation.Induction.centralCover_candidateFiniteQuotientPostcompHom_apply {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (y : p.fst.Y) : (ProfiniteGrp.Hom.hom (centralCover_candidateFiniteQuotientPostcompHom B T)) y = T.topToMiddle y

theorem Q2Presentation.Induction.centralCover_candidateFiniteQuotientPostcompHom_surjective {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : Function.Surjective ⇑(ProfiniteGrp.Hom.hom (centralCover_candidateFiniteQuotientPostcompHom B T))

Surjectivity of the profinite postcomposition morphism is exactly the surjectivity of the finite quotient map stored in the elementary tower.

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

The remaining semantic content of boundary-compatible postcomposition: postcomposing a top candidate boundary-framed exact-image map along the finite quotient Y -> B still satisfies the middle boundary frame.

• boundary_compat (f : centralCoverCandidateSource) (γ : ↑GammaA.toProfinite.toTop) : T.middleChild.fst.qYMap (T.topToMiddle ((ProfiniteGrp.Hom.hom (↑f).hom) γ)) = (ProfiniteGrp.Hom.hom T.middleChild.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) γ)

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

Reassemble the old boundary-postcomposition structure from the finite quotient morphism and the remaining boundary-compatibility proof.

Equations

• D.boundaryPostcompData = { topToMiddleHom := Q2Presentation.Induction.centralCover_candidateFiniteQuotientPostcompHom B T, topToMiddle_surj := ⋯, topToMiddle_agrees := ⋯, boundary_compat := ⋯ }

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

Boundary-postcomposition packet reduced to finite quotient postcomposition plus the boundary-frame compatibility statement.

Exact-image middle index and obstruction evaluation

def Q2Presentation.Induction.centralCover_candidateMiddleExactImageIndexBaseData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) : CentralCoverCandidateObstructionIndexBaseData B T

Concrete exact-image index: use the middle boundary-framed exact-image source itself, with the identity forgetful map. Finiteness is theorem-level because GammaA is topologically finitely generated and the target is finite.

Equations

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

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

The finite obstruction-index/base-map packet is closed by taking the middle exact-image source as its own finite index.

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

Explicit obstruction evaluation on a fixed candidate exact-image index.

• obstruction : I.X → B.obstructionSpace

def Q2Presentation.Induction.CentralCoverCandidateObstructionEvaluationData.obstructionMapData {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {I : CentralCoverCandidateObstructionIndexBaseData B T} (D : CentralCoverCandidateObstructionEvaluationData B T I) : CentralCoverCandidateObstructionMapData B T I

Repackage an explicit obstruction evaluation as the existing obstruction-map packet.

Equations

• D.obstructionMapData = { obstruction := D.obstruction }

theorem Q2Presentation.Induction.centralCover_candidateObstructionMapData_from_evaluation {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (I : CentralCoverCandidateObstructionIndexBaseData B T) (D : CentralCoverCandidateObstructionEvaluationData B T I) : Nonempty (CentralCoverCandidateObstructionMapData B T I)

The obstruction-map packet is just an explicit R-valued evaluation on the chosen finite exact-image index.

def Q2Presentation.Induction.centralCover_candidateMiddleObstructionData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)) : CentralCoverSourceObstructionData B centralCoverCandidateSource

Obstruction data obtained from the concrete middle exact-image index and an explicit obstruction evaluation on it.

Equations

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

def Q2Presentation.Induction.centralCover_candidateMiddleAffineFiberTorsorData {p : FramedPair} (B : MinimalBlock p) (T : CentralCoverElementaryQuotientTowerData B) (D : CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)) : CentralCoverCandidateAffineFiberTorsorData B (centralCover_candidateMiddleObstructionData B T D)

Canonical affine-fibre torsor attached to the concrete middle obstruction data. The affine torsor itself is already theorem-level in the current API.

Equations

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

Frattini exact-image equivalence

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

Exact-image equivalence form of the Frattini packet.

This is the semantic object behind the cardinality statement: the top candidate boundary-framed exact-image maps are partitioned by unobstructed middle exact-image data and their regular R-lift fibres.

• equiv : centralCoverCandidateSource ≃ (x : { x : O.X // O.o x = 0 }) × F.Lift x

def Q2Presentation.Induction.CentralCoverCandidateFrattiniExactImageEquivData.partition {p : FramedPair} {B : MinimalBlock p} {T : CentralCoverElementaryQuotientTowerData B} {O : CentralCoverSourceObstructionData B centralCoverCandidateSource} {Z : CentralCoverSourceCocycleData B} {F : CentralCoverSourceLiftFibers B centralCoverCandidateSource O Z} (D : CentralCoverCandidateFrattiniExactImageEquivData B T O Z F) : CentralCoverSourceLiftPartition B centralCoverCandidateSource O Z F

The exact-image partition carried by an equivalence.

Equations

• D.partition = { bij := D.equiv }

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

Cardinality shadow of an actual exact-image equivalence.

Equations

• ⋯ = ⋯

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

Frattini exact-image surjectivity/partition carried by an equivalence.

Equations

• D.frattiniExactImage = { partition := D.partition }

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

The Frattini cardinality packet follows from an actual exact-image equivalence.

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

The stronger partition/surjectivity packet also follows directly from the same exact-image equivalence, without using a cardinality-to-equivalence choice.

Full concrete reassembly

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

The concrete candidate-side data left after theorem-level reassembly: boundary compatibility for finite quotient postcomposition, an explicit obstruction evaluation on the closed middle exact-image index, and an actual Frattini exact-image equivalence for the canonical affine fibres.

• boundaryCompatibility : CentralCoverCandidateBoundaryCompatibilityData B T
• obstructionEvaluation : CentralCoverCandidateObstructionEvaluationData B T (centralCover_candidateMiddleExactImageIndexBaseData B T)
• frattiniEquiv : CentralCoverCandidateFrattiniExactImageEquivData B T (centralCover_candidateMiddleObstructionData B T self.obstructionEvaluation) (centralCover_candidateMiddleAffineFiberTorsorData B T self.obstructionEvaluation).Z (centralCover_candidateMiddleAffineFiberTorsorData B T self.obstructionEvaluation).F

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

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

This is the manuscript-facing content behind the candidate side of lem:covertransform, lem:obstructionseparation, and prop:finalfourier: boundary-compatible quotient postcomposition, explicit obstruction evaluation, and an actual Frattini exact-image equivalence.

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

Reassemble the current aggregate exact-image residual from the concrete candidate-side data in this sidecar.

Equations

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

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

Aggregate candidate exact-image residual reassembled from the concrete candidate-side data in this sidecar.

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

Candidate semantic R-lift data routed through the concrete sidecar data.

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

Coherent candidate lift-partition data routed through the concrete sidecar data.

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

Aggregate candidate exact-image residual reassembled from the single concrete candidate data packet.

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

Candidate semantic R-lift data reassembled from the concrete candidate data packet.

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

Coherent candidate lift-partition data reassembled from the concrete candidate data packet.