Route152 target K/R quotient/action closers

Route152 lowers the two compact Route146 target leaves:

• TargetKmodRRoute146BridgeClosers.centralCover_targetRoute146LowerQuotientEquivData;
• TargetKmodRRoute146BridgeClosers.centralCover_targetRoute146LiteralRepresentativeActionData.

The lower target is Route34's theorem-level literal quotient Y/K. The only remaining lower-side semantic datum is Route28's identification of that child with the abstract action group B.C. The representative-action leaf is then rebuilt from Route28's selected-representative action packet and the closed inner-conjugation theorem for K/R.

Literal lower quotient Y/K

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute152Closers.route152LowerQuotientMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerQuotientMapData B D

Route152 uses Route34's theorem-level literal quotient map Y -> Y/K as the lower target in the manuscript tower.

Equations

• Q2Presentation.Induction.TargetKmodRRoute152Closers.route152LowerQuotientMapData B D = Q2Presentation.Induction.TargetKmodRRoute34BridgeProofs.lowerQuotientMapData_of_route34 B D

def Q2Presentation.Induction.TargetKmodRRoute152Closers.route146LowerQuotientEquivData_of_route152LowerAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerActionEquivData B D (route152LowerQuotientMapData B D)) : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D

Route28's lower-action equivalence for the Route34 literal lower child is exactly Route146's compact Y/K ~= B.C quotient datum.

Equations

• Q2Presentation.Induction.TargetKmodRRoute152Closers.route146LowerQuotientEquivData_of_route152LowerAction B D E = { lowerActionEquiv := E.lowerActionEquiv }

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

Route152 replacement for the Route146 lower quotient leaf.

The only non-local target fact left here is Route28's manuscript-shaped identification of the literal lower quotient child Y/K with B.C.

Literal representative action

def Q2Presentation.Induction.TargetKmodRRoute152Closers.route28LowerActionEquivData_of_route146LowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D) : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerActionEquivData B D (route152LowerQuotientMapData B D)

View an arbitrary Route146 quotient equivalence as Route28 lower-action data for Route34's literal lower quotient child.

Equations

• Q2Presentation.Induction.TargetKmodRRoute152Closers.route28LowerActionEquivData_of_route146LowerQuotientEquiv B D E = { lowerActionEquiv := E.lowerActionEquiv }

def Q2Presentation.Induction.TargetKmodRRoute152Closers.lowerProjectionData_of_route152LowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The concrete lower projection Y -> B.C induced by a Route146 selected equivalence Y/K ~= B.C.

Equations

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

theorem Q2Presentation.Induction.TargetKmodRRoute152Closers.lowerProjectionData_of_route152LowerQuotientEquiv_literalRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D) (q : p.fst.Y ⧸ D.Ksub) : (lowerProjectionData_of_route152LowerQuotientEquiv B D E).lowerProjection (TargetKmodRRoute146BridgeClosers.literalQuotientRepresentative B D q) = E.lowerActionEquiv q

The Route152 lower projection sends the theorem-level literal representative of q : Y/K to the selected abstract lower class.

def Q2Presentation.Induction.TargetKmodRRoute152Closers.route146LiteralRepresentativeActionData_of_route152ProjectedAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LowerQuotientEquivData B D) (A : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route152LowerQuotientEquiv B D E)) : TargetKmodRRoute146BridgeClosers.CentralCoverTargetRoute146LiteralRepresentativeActionData B D E

Convert projected conjugation through the Route152 lower projection into Route146's literal-representative action packet.

Equations

• ⋯ = ⋯

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

Route152 replacement for the Route146 literal representative-action leaf.

The only non-local target fact left here is Route28's selected-representative action law for the lower projection induced by the supplied quotient equivalence; same-coset independence is theorem-level from K/R ~= M.

Route146-shaped bridge and downstream providers

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

Route146 bridge data assembled from the Route152-lowered quotient/action facts.

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

Route152 quotient-action provider through the Route146 bridge surface.

Equations

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

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

Route152 replacement for the target K/R quotient-action hook.

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

Drop-in decoration-kernel provider for downstream central-cover recursion.

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

Convenience framed-quotient provider downstream of the Route152 target closer.