Actual target decoration block-map construction

This sidecar strictly narrows the current Section 8 residual centralCover_targetDecorationBlockMapData.

Manuscript anchor: §8, lem:decorationblock. Once the decoration kills the Frattini layer R, it has a canonical descent to the actual quotient K/R. The concrete target packet already identifies that quotient with the abstract module M. This file builds the descended linear map and proves its agreement with thetaY on K.

The only residual left here is the semantic compatibility between the abstract C-action B.actM and conjugation on the realized quotient K/R; this is recorded as invariance of the canonical descended map, not as an arbitrary choice of block map.

def Q2Presentation.Induction.TargetDecorationBlockMapActualProofs.quotientDecorationHom {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (hR : D.Rsub ≤ p.fst.thetaY.ker) : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub) →* Multiplicative p.fst.E

If thetaY kills R, it descends canonically to the image of K in Y/R.

Equations

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

@[simp]

theorem Q2Presentation.Induction.TargetDecorationBlockMapActualProofs.quotientDecorationHom_kmodRPoint {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (hR : D.Rsub ≤ p.fst.thetaY.ker) (k : ↥D.Ksub) : (quotientDecorationHom B D hR) (TargetDecorationKernelProofs.kmodRPoint B D k) = p.fst.thetaY ↑k

def Q2Presentation.Induction.TargetDecorationBlockMapActualProofs.transportedDecorationHom {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (hR : D.Rsub ≤ p.fst.thetaY.ker) : Multiplicative B.M →* Multiplicative p.fst.E

Transport the descended quotient hom across the concrete equivalence K/R ≃ M.

Equations

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

def Q2Presentation.Induction.TargetDecorationBlockMapActualProofs.transportedDecorationAddHom {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (hR : D.Rsub ≤ p.fst.thetaY.ker) : B.M →+ p.fst.E

The transported multiplicative hom, read additively.

Equations

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

def Q2Presentation.Induction.TargetDecorationBlockMapActualProofs.transportedDecorationLinearMap {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (hR : D.Rsub ≤ p.fst.thetaY.ker) : B.M →ₗ[ZMod 2] p.fst.E

The canonical descended decoration map M -> E.

Equations

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

@[simp]

theorem Q2Presentation.Induction.TargetDecorationBlockMapActualProofs.transportedDecorationLinearMap_apply {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (hR : D.Rsub ≤ p.fst.thetaY.ker) (m : B.M) : (transportedDecorationLinearMap B D hR) m = Multiplicative.toAdd ((transportedDecorationHom B D hR) (Multiplicative.ofAdd m))

theorem Q2Presentation.Induction.TargetDecorationBlockMapActualProofs.transportedDecorationLinearMap_agrees_on_K {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (hR : D.Rsub ≤ p.fst.thetaY.ker) (k : ↥D.Ksub) : p.fst.thetaY ↑k = Multiplicative.ofAdd ((transportedDecorationLinearMap B D hR) (TargetDecorationKernelProofs.kmodRVector B D k))

The canonical descended linear map agrees with thetaY on the realized subgroup K.

The narrowed residual

structure Q2Presentation.Induction.TargetDecorationBlockMapActualProofs.CentralCoverTargetDecorationActualDescentData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Prop

Narrow actual-descent packet.

Compared with CentralCoverTargetDecorationBlockMapData, this no longer asks for an arbitrary descended block map or for agreement with thetaY. The map and agreement are constructed above from the single descent condition R <= ker(thetaY). The remaining semantic content is exactly that this canonical descended map is invariant for the abstract C-action on M.

• Rsub_le_thetaY_ker : D.Rsub ≤ p.fst.thetaY.ker
• canonical_blockMap_invariant (c : B.C) : transportedDecorationLinearMap B D ⋯ ∘ₗ ↑(B.actM c) = transportedDecorationLinearMap B D ⋯

def Q2Presentation.Induction.TargetDecorationBlockMapActualProofs.blockMapData_of_actualDescent {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetDecorationActualDescentData B D) : TargetDecorationKernelProofs.CentralCoverTargetDecorationBlockMapData B D

Rebuild the current block-map packet from the canonical actual descent.

Equations

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

axiom Q2Presentation.Induction.centralCover_targetDecorationActualDescentData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationBlockMapActualProofs.CentralCoverTargetDecorationActualDescentData B D)

Narrow residual replacing centralCover_targetDecorationBlockMapData.

It asks only for:

• the Frattini-layer descent condition R <= ker(thetaY);
• invariance of the canonical descended map under the abstract C-action.

The descended linear map and its agreement with thetaY on K are now theorems, not residual fields.

theorem Q2Presentation.Induction.centralCover_targetDecorationBlockMapData_proven {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationKernelProofs.CentralCoverTargetDecorationBlockMapData B D)

Route-ready replacement for the current block-map residual, using the narrow actual-descent packet.

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

Decoration-kernel closure routed through the narrowed actual-descent packet, without using centralCover_targetDecorationBlockMapData.

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

Canonical framed quotient closure routed through the narrowed actual-descent packet, without using centralCover_targetDecorationBlockMapData.