Documentation

Q2Presentation.Induction.TargetKmodRRoute164Closers

Route164 target `K/R` projection/action closers #

Route163's target frontier contains nine Route161 split atoms: a raw lower projection function, its hom laws, pointwise fibres/specs, two pointwise kernel tests, and selected representatives with their action law.

This sidecar lowers that split to a coherent concrete projection/action surface:

a monoid lower projection Y -> B.C;
surjectivity of that projection;
kernel identification with the selected subgroup K;
the selected representative action law for representatives chosen from surjectivity.

The Route161 packets are then theorem-level, and the downstream decoration-kernel provider can use the Route164 data without invoking any Route151, Route28, Route146, or Route161 residual declarations.

Route164 concrete projection/action atoms #

structure Q2Presentation.Induction.TargetKmodRRoute164Closers.CentralCoverTargetRoute164LowerProjectionMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Route164 concrete lower projection map Y -> C = B.C.

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

Instances For

structure Q2Presentation.Induction.TargetKmodRRoute164Closers.CentralCoverTargetRoute164LowerProjectionSurjectivityData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) :

Route164 surjectivity for the selected lower projection.

lowerProjection_surj : Function.Surjective ⇑M.lowerProjection

Instances For

structure Q2Presentation.Induction.TargetKmodRRoute164Closers.CentralCoverTargetRoute164LowerProjectionKernelData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) :

Route164 kernel identification for the selected lower projection.

lowerProjection_ker : D.Ksub = M.lowerProjection.ker

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.route164QuotientRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) (c : B.C) :

Representative selected from the Route164 surjectivity packet.

Equations

Q2Presentation.Induction.TargetKmodRRoute164Closers.route164QuotientRepresentative B D M S c = Classical.choose ⋯

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute164Closers.route164QuotientRepresentative_spec {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) (c : B.C) :

M.lowerProjection (route164QuotientRepresentative B D M S c) = c

The selected Route164 representative maps to its lower class.

structure Q2Presentation.Induction.TargetKmodRRoute164Closers.CentralCoverTargetRoute164RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) :

Route164 selected-representative action law on K/R.

representative_action_realizes_conjugation (c : B.C) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM c) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D (route164QuotientRepresentative B D M S c) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

Instances For

Route164 residual names #

axiom Q2Presentation.Induction.TargetKmodRRoute164Closers.centralCover_targetRoute164LowerProjectionMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetRoute164LowerProjectionMapData B D)

Route164 residual: concrete lower projection map Y -> B.C.

axiom Q2Presentation.Induction.TargetKmodRRoute164Closers.centralCover_targetRoute164LowerProjectionSurjectivityData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) :

Nonempty (CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M)

Route164 residual: the concrete lower projection is onto.

axiom Q2Presentation.Induction.TargetKmodRRoute164Closers.centralCover_targetRoute164LowerProjectionKernelData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) :

Nonempty (CentralCoverTargetRoute164LowerProjectionKernelData B D M)

Route164 residual: the lower projection has kernel K.

axiom Q2Presentation.Induction.TargetKmodRRoute164Closers.centralCover_targetRoute164RepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) :

Nonempty (CentralCoverTargetRoute164RepresentativeActionData B D M S)

Route164 residual: selected lower-class representatives realize the B.C action on the literal quotient K/R.

Transport-final and Route161 adapters #

def Q2Presentation.Induction.TargetKmodRRoute164Closers.lowerProjectionData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) (K : CentralCoverTargetRoute164LowerProjectionKernelData B D M) :

TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Transport-final lower projection data assembled from Route164.

Equations

Q2Presentation.Induction.TargetKmodRRoute164Closers.lowerProjectionData_of_route164 B D M S K = { lowerProjection := M.lowerProjection, lowerProjection_surj := ⋯, lowerProjection_ker := ⋯ }

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.representativeActionBridgeData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) (K : CentralCoverTargetRoute164LowerProjectionKernelData B D M) (A : CentralCoverTargetRoute164RepresentativeActionData B D M S) :

TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (lowerProjectionData_of_route164 B D M S K)

Same-tower representative bridge assembled from Route164.

Equations

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

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.route161LowerProjectionFunctionData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) :

TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionFunctionData B D

Route161 raw function packet from the Route164 monoid map.

Equations

Q2Presentation.Induction.TargetKmodRRoute164Closers.route161LowerProjectionFunctionData_of_route164 B D M = { lowerProjectionFun := ⇑M.lowerProjection }

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.route161LowerProjectionHomData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) :

TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionHomData B D (route161LowerProjectionFunctionData_of_route164 B D M)

Route161 hom-law packet from the Route164 monoid map.

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.route161LowerProjectionPreimageData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) (c : B.C) :

TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionPreimageData B D (route161LowerProjectionFunctionData_of_route164 B D M) c

Route161 fibre witness from Route164 surjectivity.

Equations

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

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.route161LowerProjectionPreimageSpecData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) (c : B.C) :

TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionPreimageSpecData B D (route161LowerProjectionFunctionData_of_route164 B D M) c (route161LowerProjectionPreimageData_of_route164 B D M S c)

Route161 fibre spec from the Route164 representative section law.

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.route161KsubProjectionTrivialData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (K : CentralCoverTargetRoute164LowerProjectionKernelData B D M) :

TargetKmodRRoute161Closers.CentralCoverTargetRoute161KsubProjectionTrivialData B D (route161LowerProjectionFunctionData_of_route164 B D M)

Route161 pointwise K <= ker from the Route164 kernel equality.

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.route161ProjectionTrivialLeKsubData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (K : CentralCoverTargetRoute164LowerProjectionKernelData B D M) :

TargetKmodRRoute161Closers.CentralCoverTargetRoute161ProjectionTrivialLeKsubData B D (route161LowerProjectionFunctionData_of_route164 B D M)

Route161 pointwise ker <= K from the Route164 kernel equality.

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.route161RepresentativeData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) :

TargetKmodRRoute161Closers.CentralCoverTargetRoute161RepresentativeData B D (route161LowerProjectionFunctionData_of_route164 B D M)

Route161 representative packet from Route164 selected representatives.

Equations

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

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.route161RepresentativeSectionData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) :

TargetKmodRRoute161Closers.CentralCoverTargetRoute161RepresentativeSectionData B D (route161LowerProjectionFunctionData_of_route164 B D M) (route161RepresentativeData_of_route164 B D M S)

Route161 representative section law from Route164 surjectivity.

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.TargetKmodRRoute164Closers.route161RepresentativeActionData_of_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (M : CentralCoverTargetRoute164LowerProjectionMapData B D) (S : CentralCoverTargetRoute164LowerProjectionSurjectivityData B D M) (A : CentralCoverTargetRoute164RepresentativeActionData B D M S) :

TargetKmodRRoute161Closers.CentralCoverTargetRoute161RepresentativeActionData B D (route161LowerProjectionFunctionData_of_route164 B D M) (route161RepresentativeData_of_route164 B D M S)

Route161 representative action packet from the Route164 action law.

Equations

⋯ = ⋯

Instances For

structure Q2Presentation.Induction.TargetKmodRRoute164Closers.CentralCoverTargetRoute164AsRoute161Data {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Coherent Route161 split packet supplied theorem-level by Route164 data.

lowerProjectionFunctionData : TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionFunctionData B D
lowerProjectionHomData : TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionHomData B D self.lowerProjectionFunctionData
lowerProjectionPreimageData (c : B.C) : TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionPreimageData B D self.lowerProjectionFunctionData c
lowerProjectionPreimageSpecData (c : B.C) : TargetKmodRRoute161Closers.CentralCoverTargetRoute161LowerProjectionPreimageSpecData B D self.lowerProjectionFunctionData c (self.lowerProjectionPreimageData c)
ksubProjectionTrivialData : TargetKmodRRoute161Closers.CentralCoverTargetRoute161KsubProjectionTrivialData B D self.lowerProjectionFunctionData
projectionTrivialLeKsubData : TargetKmodRRoute161Closers.CentralCoverTargetRoute161ProjectionTrivialLeKsubData B D self.lowerProjectionFunctionData
representativeData : TargetKmodRRoute161Closers.CentralCoverTargetRoute161RepresentativeData B D self.lowerProjectionFunctionData
representativeSectionData : TargetKmodRRoute161Closers.CentralCoverTargetRoute161RepresentativeSectionData B D self.lowerProjectionFunctionData self.representativeData
representativeActionData : TargetKmodRRoute161Closers.CentralCoverTargetRoute161RepresentativeActionData B D self.lowerProjectionFunctionData self.representativeData

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute164Closers.centralCover_targetRoute161Data_from_route164Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetRoute164AsRoute161Data B D)

Route164 proves the full coherent Route161 split packet without using any Route161 residual declaration.

Route164 downstream target provider #

theorem Q2Presentation.Induction.TargetKmodRRoute164Closers.centralCover_targetKmodRProjectedConjugationActionData_from_route164Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty ((P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) ×' TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

Route164 projected-action provider in the transport-final surface.

theorem Q2Presentation.Induction.TargetKmodRRoute164Closers.centralCover_targetKmodRQuotientActionData_from_route164Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

Route164 quotient-action provider.

theorem Q2Presentation.Induction.TargetKmodRRoute164Closers.centralCover_targetDecorationKernelData_from_route164Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetDecorationKernelData B D)

Route164 drop-in target decoration-kernel provider.

theorem Q2Presentation.Induction.TargetKmodRRoute164Closers.centralCover_targetDecorationKernelData_from_route152Closers_route164 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetDecorationKernelData B D)

Name mirroring the Route161 call site for a one-line replacement.

theorem Q2Presentation.Induction.TargetKmodRRoute164Closers.centralCover_targetCanonicalFramedQuotientData_from_route164Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

Convenience framed-quotient provider through Route164.