Final transport packets for the target K/R action

This sidecar further decomposes the two residuals introduced by TargetKmodRQuotientActionFinalClosers:

• centralCover_targetLowerQuotientEquivData;
• centralCover_targetKmodRActionTransportData.

The replacement packets are tied directly to the manuscript tower Y -> B = Y/R -> C = Y/K and to conjugation on the literal quotient K/R:

• a concrete projection Y -> B.C with kernel K;
• compatibility of any selected Y/K ~= B.C equivalence with that projection;
• the assertion that the projected B.C-action on M is conjugation on K/R.

Smaller semantic packets

structure Q2Presentation.Induction.TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type

The abstract lower action group B.C is reached by the concrete lower projection Y -> C = Y/K.

This is a first-isomorphism-theorem packet: the map is onto and has kernel the selected subgroup K. The old residual equivalence Y/K ~= B.C follows from these two fields.

• lowerProjection : p.fst.Y →* B.C
• lowerProjection_surj : Function.Surjective ⇑self.lowerProjection
• lowerProjection_ker : D.Ksub = self.lowerProjection.ker

structure Q2Presentation.Induction.TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerEquivProjectionCompatibilityData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionData B D) (L : TargetKmodRQuotientActionFinalClosers.CentralCoverTargetLowerQuotientEquivData B D) : Prop

A selected lower quotient equivalence agrees with the concrete projection.

This packet is only needed when reconstructing the old action-transport residual for an arbitrary externally supplied equivalence L.

• lowerQuotientEquiv_agrees_projection (y : p.fst.Y) : L.lowerQuotientEquiv (TargetKmodRActionProofs.lowerQuotientClass B D y) = P.lowerProjection y

structure Q2Presentation.Induction.TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionData B D) : Prop

The projected action of the concrete lower group Y/K on M is the quotient-conjugation action on the literal quotient K/R.

• action_realizes_projected_conjugation (y : p.fst.Y) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (P.lowerProjection y)) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

Reassembly of the old two packets

def Q2Presentation.Induction.TargetKmodRActionTransportFinalProofs.lowerQuotientEquivData_of_projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionData B D) : TargetKmodRQuotientActionFinalClosers.CentralCoverTargetLowerQuotientEquivData B D

The concrete lower projection induces the old lower quotient equivalence packet by the first isomorphism theorem.

Equations

• Q2Presentation.Induction.TargetKmodRActionTransportFinalProofs.lowerQuotientEquivData_of_projection B D P = { lowerQuotientEquiv := QuotientGroup.liftEquiv D.Ksub ⋯ ⋯ }

theorem Q2Presentation.Induction.TargetKmodRActionTransportFinalProofs.lowerQuotientEquivData_of_projection_apply {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionData B D) (y : p.fst.Y) : (lowerQuotientEquivData_of_projection B D P).lowerQuotientEquiv (TargetKmodRActionProofs.lowerQuotientClass B D y) = P.lowerProjection y

The equivalence induced by a projection sends the class of y to the projection of y.

def Q2Presentation.Induction.TargetKmodRActionTransportFinalProofs.lowerEquivProjectionCompatibilityData_of_projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionData B D) : CentralCoverTargetLowerEquivProjectionCompatibilityData B D P (lowerQuotientEquivData_of_projection B D P)

The induced lower equivalence is automatically compatible with the concrete lower projection.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRActionTransportFinalProofs.actionTransportData_of_projectionCompatibility {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionData B D) (L : TargetKmodRQuotientActionFinalClosers.CentralCoverTargetLowerQuotientEquivData B D) (E : CentralCoverTargetLowerEquivProjectionCompatibilityData B D P L) (A : CentralCoverTargetKmodRProjectedConjugationActionData B D P) : TargetKmodRQuotientActionFinalClosers.CentralCoverTargetKmodRActionTransportData B D L

Assemble the old action-transport packet from projection compatibility and the projected conjugation action law.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRActionTransportFinalProofs.quotientActionData_of_projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionData B D) (A : CentralCoverTargetKmodRProjectedConjugationActionData B D P) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Directly assemble the quotient-action packet from the two semantic packets: lower projection and projected conjugation action.

Equations

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

New residual names and route-ready closures

axiom Q2Presentation.Induction.centralCover_targetLowerProjectionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D)

Smaller residual: construct the concrete lower projection Y -> B.C and prove its kernel is K.

axiom Q2Presentation.Induction.centralCover_targetLowerEquivProjectionCompatibilityData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (L : TargetKmodRQuotientActionFinalClosers.CentralCoverTargetLowerQuotientEquivData B D) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerEquivProjectionCompatibilityData B D P L)

Smaller residual: an externally selected lower quotient equivalence agrees with the concrete projection.

axiom Q2Presentation.Induction.centralCover_targetKmodRProjectedConjugationActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

Smaller residual: projected action through Y/K is conjugation on K/R.

theorem Q2Presentation.Induction.centralCover_targetLowerQuotientEquivData_from_transportFinalProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRQuotientActionFinalClosers.CentralCoverTargetLowerQuotientEquivData B D)

Replacement for centralCover_targetLowerQuotientEquivData, from the concrete lower projection.

theorem Q2Presentation.Induction.centralCover_targetKmodRActionTransportData_from_transportFinalProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (L : TargetKmodRQuotientActionFinalClosers.CentralCoverTargetLowerQuotientEquivData B D) : Nonempty (TargetKmodRQuotientActionFinalClosers.CentralCoverTargetKmodRActionTransportData B D L)

Replacement for centralCover_targetKmodRActionTransportData, decomposed into compatibility of the selected lower equivalence with the projection and the projected conjugation action law.

theorem Q2Presentation.Induction.centralCover_targetKmodRQuotientActionData_from_transportFinalProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

Quotient-action packet from the two route-selected semantic packets. This version does not need the arbitrary-equivalence compatibility residual because it uses the lower equivalence induced by the projection.

theorem Q2Presentation.Induction.centralCover_targetKmodRActionCompatibilityData_from_transportFinalProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationCanonicalInvarianceProofs.CentralCoverTargetKmodRActionCompatibilityData B D)

Downstream action-compatibility packet through the new transport-final decomposition.

theorem Q2Presentation.Induction.centralCover_targetDecorationCanonicalInvarianceData_from_transportFinalProofs {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationActualDescentProofs.CentralCoverTargetDecorationCanonicalInvarianceData B D)

Canonical target-decoration invariance through the transport-final decomposition.

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

Actual target-decoration descent through the transport-final decomposition.

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

Decoration-kernel closure through the transport-final decomposition.

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

Canonical framed quotient closure through the transport-final decomposition.