Route151 target K/R quotient/action closers

Route150 leaves two compact target-side atoms from TargetKmodRRoute146BridgeClosers:

• centralCover_targetRoute146LowerQuotientEquivData;
• centralCover_targetRoute146LiteralRepresentativeActionData.

This sidecar lowers that pair to concrete Section 8 quotient/action compatibility facts:

• a lower projection Y -> B.C;
• pointwise lower-projection fibres and the two kernel inclusions identifying the kernel with K;
• compatibility between a selected Y/K ~= B.C equivalence and the projection;
• the projected B.C-action on M = K/R as quotient conjugation.

The exported providers have the same theorem-level target surfaces as the two Route150 leaves, but their axiom dependencies are the finer Route151 residuals.

Route151 residual packets

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

Route151 lower projection map Y -> C, with C represented by the abstract action group B.C.

Manuscript anchor: §7 target tower Y -> C = Y/K, used in §8 exact-image and phase-cover recursion.

• lowerProjection : p.fst.Y →* B.C

structure Q2Presentation.Induction.TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionSurjFiberData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) (c : B.C) : Type

Route151 pointwise fibre of the lower projection.

• preimage : p.fst.Y
• lowerProjection_preimage : P.lowerProjection self.preimage = c

structure Q2Presentation.Induction.TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKsubLeKerData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) : Prop

Route151 lower-projection kernel inclusion K <= ker(Y -> C).

• ksub_le_ker : D.Ksub ≤ P.lowerProjection.ker

structure Q2Presentation.Induction.TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKerLeKsubData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) : Prop

Route151 lower-projection kernel inclusion ker(Y -> C) <= K.

• ker_le_ksub : P.lowerProjection.ker ≤ D.Ksub

structure Q2Presentation.Induction.TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerEquivProjectionCompatibilityData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) (E : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D) : Prop

Route151 compatibility between an externally selected lower quotient equivalence Y/K ~= B.C and the concrete lower projection.

This is the exact compatibility needed when the Route146 literal-action packet is stated for an arbitrary selected quotient equivalence.

• lowerActionEquiv_agrees_projection (y : p.fst.Y) : E.lowerActionEquiv (TargetKmodRActionProofs.lowerQuotientClass B D y) = P.lowerProjection y

structure Q2Presentation.Induction.TargetKmodRRoute151Closers.CentralCoverTargetRoute151ProjectedRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) : Prop

Route151 projected representative-action law.

This is the §8 action compatibility fact: after projecting an ambient element to Y/K, the abstract B.C action on M is conjugation 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))

Route151 residual names

axiom Q2Presentation.Induction.TargetKmodRRoute151Closers.centralCover_targetRoute151LowerProjectionMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (CentralCoverTargetRoute151LowerProjectionMapData B D)

Route151 residual: concrete lower projection Y -> C = Y/K, with codomain represented by B.C.

axiom Q2Presentation.Induction.TargetKmodRRoute151Closers.centralCover_targetRoute151LowerProjectionSurjFiberData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) (c : B.C) : Nonempty (CentralCoverTargetRoute151LowerProjectionSurjFiberData B D P c)

Route151 residual: a pointwise fibre of the concrete lower projection.

axiom Q2Presentation.Induction.TargetKmodRRoute151Closers.centralCover_targetRoute151LowerProjectionKsubLeKerData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) : Nonempty (CentralCoverTargetRoute151LowerProjectionKsubLeKerData B D P)

Route151 residual: K <= ker(Y -> C).

axiom Q2Presentation.Induction.TargetKmodRRoute151Closers.centralCover_targetRoute151LowerProjectionKerLeKsubData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) : Nonempty (CentralCoverTargetRoute151LowerProjectionKerLeKsubData B D P)

Route151 residual: ker(Y -> C) <= K.

axiom Q2Presentation.Induction.TargetKmodRRoute151Closers.centralCover_targetRoute151LowerEquivProjectionCompatibilityData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) (E : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D) : Nonempty (CentralCoverTargetRoute151LowerEquivProjectionCompatibilityData B D P E)

Route151 residual: a selected quotient equivalence agrees with the concrete lower projection.

axiom Q2Presentation.Induction.TargetKmodRRoute151Closers.centralCover_targetRoute151ProjectedRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) : Nonempty (CentralCoverTargetRoute151ProjectedRepresentativeActionData B D P)

Route151 residual: projected B.C action on K/R is quotient conjugation.

Reassembly of the compact Route146 target leaves

def Q2Presentation.Induction.TargetKmodRRoute151Closers.lowerProjectionData_of_route151Pieces {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) (HK₁ : CentralCoverTargetRoute151LowerProjectionKsubLeKerData B D P) (HK₂ : CentralCoverTargetRoute151LowerProjectionKerLeKsubData B D P) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Assemble the transport-final lower projection packet from Route151 pointwise lower-projection residuals.

Equations

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

def Q2Presentation.Induction.TargetKmodRRoute151Closers.route146LowerQuotientEquivData_of_route151Projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D

The Route151 lower projection induces the compact Route146 quotient equivalence Y/K ~= B.C.

Equations

• Q2Presentation.Induction.TargetKmodRRoute151Closers.route146LowerQuotientEquivData_of_route151Projection B D P = { lowerActionEquiv := QuotientGroup.liftEquiv D.Ksub ⋯ ⋯ }

theorem Q2Presentation.Induction.TargetKmodRRoute151Closers.centralCover_targetRoute146LowerQuotientEquivData_from_route151Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D)

Route151 replacement for the Route150 lower quotient leaf.

def Q2Presentation.Induction.TargetKmodRRoute151Closers.route146LiteralRepresentativeActionData_of_route151ProjectionAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D) (P : CentralCoverTargetRoute151LowerProjectionMapData B D) (C : CentralCoverTargetRoute151LowerEquivProjectionCompatibilityData B D P E) (A : CentralCoverTargetRoute151ProjectedRepresentativeActionData B D P) : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LiteralRepresentativeActionData B D E

Assemble the compact Route146 literal representative-action packet from Route151 projection compatibility and projected action.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.TargetKmodRRoute151Closers.centralCover_targetRoute146LiteralRepresentativeActionData_from_route151Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D) : Nonempty (TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LiteralRepresentativeActionData B D E)

Route151 replacement for the Route150 literal representative-action leaf.

Route146/Route150-shaped drop-in providers

theorem Q2Presentation.Induction.TargetKmodRRoute151Closers.centralCover_targetRoute146BridgeData_from_route151Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146BridgeData B D)

Route146 bridge packet with both compact fields supplied by Route151 residuals.

def Q2Presentation.Induction.TargetKmodRRoute151Closers.quotientActionData_of_route151BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146BridgeData B D) : TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Target quotient-action provider with the Route150 target compact pair replaced by Route151 residuals.

Equations

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

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

Route151 quotient-action provider.

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

Route151 drop-in target decoration-kernel provider.

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

Route151 canonical framed quotient provider.