Route21 actual bridge for the target K/R tower

Route20 exposed the two remaining target same-tower facts as broad packets:

• identify the abstract lower action group B.C with the literal quotient Y/K;
• prove that the abstract action B.actM is conjugation-induced on K/R.

This sidecar keeps the same downstream route20 surface available, but replaces those two broad assumptions by a stricter manuscript-shaped bridge:

• a concrete projection Y -> B.C with kernel exactly K, hence an explicit first-isomorphism-theorem identification Y/K ~= B.C;
• one representative in each lower class whose action realizes conjugation on K/R.

The upgrade from selected representatives to all ambient representatives is theorem-level: TargetKmodRInnerConjugationClosed already proves inner conjugation by K is trivial on K/R from the realized bridge K/R ~= M.

Route21 manuscript-shaped residual packets

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

Route21 lower bridge: the abstract lower action group B.C is reached by the actual quotient projection from Y, with kernel K. The explicit identification Y/K ~= B.C is derived from this packet by the first isomorphism theorem below.

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

structure Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.CentralCoverTargetRoute21RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) : Type

Route21 representative action bridge. It asks only for one representative of each lower class, instead of the route20 all-ambient-representatives action law.

• quotientRepresentative : B.C → p.fst.Y
• lowerProjection_quotientRepresentative (c : B.C) : P.lowerProjection (self.quotientRepresentative c) = c
• representative_action_realizes_conjugation (c : B.C) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM c) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (self.quotientRepresentative c) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

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

Route21 provenance keeps the concrete lower projection and its representative action law tied together.

• lowerProjectionBridge : CentralCoverTargetRoute21LowerProjectionBridgeData B D
• representativeAction : CentralCoverTargetRoute21RepresentativeActionData B D self.lowerProjectionBridge

Conversions to the existing actual same-tower bridge surface

def Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.lowerProjectionData_of_route21LowerProjectionBridge {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Convert route21 lower projection data to the transport-final projection packet.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.lowerProjectionBridgeData_of_route21LowerProjectionBridge {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D

Convert route21 lower projection data to the bridge-closer projection packet.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.canonicalLowerQuotientEquivData_of_route21LowerProjectionBridge {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) : TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D

The explicit Y/K ~= B.C identification induced by the route21 lower projection.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.route20LowerQuotientIdentificationData_of_route21LowerProjectionBridge {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) : TargetKmodRRoute20ActualProofs.CentralCoverTargetRoute20LowerQuotientIdentificationData B D

Route20's lower-identification packet, built theorem-level from the route21 projection bridge.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.representativeActionBridgeData_of_route21 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) (A : CentralCoverTargetRoute21RepresentativeActionData B D P) : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (lowerProjectionData_of_route21LowerProjectionBridge B D P)

Convert the route21 representative action law to the bridge-closer packet for the induced lower projection.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.projectedConjugationActionData_of_route21 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) (A : CentralCoverTargetRoute21RepresentativeActionData B D P) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route21LowerProjectionBridge B D P)

Route21 projected conjugation action: the selected-representative bridge is upgraded to all ambient representatives using the closed inner-conjugation theorem for K/R.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.ambientActionData_of_route21 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) (A : CentralCoverTargetRoute21RepresentativeActionData B D P) : TargetKmodRSameTowerActualClosers.CentralCoverTargetKmodRAmbientActionData B D (lowerProjectionData_of_route21LowerProjectionBridge B D P)

Route21 ambient action packet on the actual same-tower surface.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.route20ActMInducedConjugationData_of_route21 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) (A : CentralCoverTargetRoute21RepresentativeActionData B D P) : TargetKmodRRoute20ActualProofs.CentralCoverTargetRoute20ActMInducedConjugationData B D (route20LowerQuotientIdentificationData_of_route21LowerProjectionBridge B D P)

Route20's induced-conjugation packet, for the lower quotient identification canonically induced by the route21 projection bridge.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.quotientActionData_of_route21 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) (A : CentralCoverTargetRoute21RepresentativeActionData B D P) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Route21 quotient-action packet, using the projection-induced lower quotient equivalence and the theorem-level all-representatives action.

Equations

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

Route21 residual names

axiom Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.centralCover_targetRoute21LowerProjectionBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute21LowerProjectionBridgeData B D)

Route21 residual 1: construct the actual lower projection Y -> B.C and prove its kernel is K, yielding B.C = Y/K.

axiom Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.centralCover_targetRoute21RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) : Nonempty (CentralCoverTargetRoute21RepresentativeActionData B D P)

Route21 residual 2: choose one representative of each lower class and prove that representative's action on K/R realizes B.actM. Inner conjugation by K then promotes this to the route20 all-representatives law.

Route-ready hooks

theorem Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.centralCover_targetRoute21ActualBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute21ActualBridgeData B D)

Route21 bridge provenance from the two strictly finer packets.

theorem Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.centralCover_targetCanonicalLowerQuotientEquivData_from_route21 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRSameTowerActualClosers.CentralCoverTargetCanonicalLowerQuotientEquivData B D)

Route21 replacement for route20's lower-quotient identification hook.

theorem Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.centralCover_targetRoute20ActMInducedConjugationData_from_route21 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute21LowerProjectionBridgeData B D) : Nonempty (TargetKmodRRoute20ActualProofs.CentralCoverTargetRoute20ActMInducedConjugationData B D (route20LowerQuotientIdentificationData_of_route21LowerProjectionBridge B D P))

Route21 replacement for route20's induced-conjugation action hook, stated for the route21-induced lower quotient identification.

theorem Q2Presentation.Induction.TargetKmodRRoute21ActualProofs.centralCover_targetRoute20ActualProvenanceData_from_route21 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute20ActualProofs.CentralCoverTargetRoute20ActualProvenanceData B D)

Route21 provenance on route20's surface. This is useful for auditing that the two old route20 target residual names are no longer used.

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

Direct route21 quotient-action provider for the target K/R branch.

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

Route21 decoration-kernel provider, suitable for the later route21 integrated file to call in place of the route20 target hook.

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

Convenience framed-quotient provider downstream of the route21 target hook.