Documentation

Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers

Route146 same-tower target pointwise bridge closers #

Route145 lowers the target same-tower frontier to two bridge residuals:

a lower projection bridge Y -> B.C with kernel K;
a single-representative action bridge for K/R.

This Route146 sidecar keeps the same downstream quotient-action and decoration-kernel shapes, but decomposes those bridge residuals into smaller manuscript-shaped atoms: a raw projection map, pointwise fibres for surjectivity, two kernel inclusions, a representative selector, pointwise section equalities, and pointwise representative-action equalities.

Lower projection split into map, fibres, and kernel inclusions #

structure Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionMapBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Route146 raw lower projection map.

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

Instances For

structure Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionSurjFiberBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionMapBridgeData B D) (c : B.C) :

Route146 pointwise fibre of the lower projection.

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

Instances For

structure Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionKsubLeKerBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionMapBridgeData B D) :

Route146 kernel inclusion K <= ker(lowerProjection).

ksub_le_ker : D.Ksub ≤ P.lowerProjection.ker

Instances For

structure Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionKerLeKsubBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionMapBridgeData B D) :

Route146 kernel inclusion ker(lowerProjection) <= K.

ker_le_ksub : P.lowerProjection.ker ≤ D.Ksub

Instances For

axiom Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetLowerProjectionMapBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetLowerProjectionMapBridgeData B D)

Route146 target residual: the raw lower projection map.

axiom Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetLowerProjectionSurjFiberBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionMapBridgeData B D) (c : B.C) :

Nonempty (CentralCoverTargetLowerProjectionSurjFiberBridgeData B D P c)

Route146 target residual: one fibre of the lower projection.

axiom Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetLowerProjectionKsubLeKerBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionMapBridgeData B D) :

Nonempty (CentralCoverTargetLowerProjectionKsubLeKerBridgeData B D P)

Route146 target residual: inclusion K <= ker(lowerProjection).

axiom Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetLowerProjectionKerLeKsubBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionMapBridgeData B D) :

Nonempty (CentralCoverTargetLowerProjectionKerLeKsubBridgeData B D P)

Route146 target residual: inclusion ker(lowerProjection) <= K.

def Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.lowerProjectionBridgeData_of_route146Pieces {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : CentralCoverTargetLowerProjectionMapBridgeData B D) (HK₁ : CentralCoverTargetLowerProjectionKsubLeKerBridgeData B D P) (HK₂ : CentralCoverTargetLowerProjectionKerLeKsubBridgeData B D P) :

TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D

Assemble the Route145 projection bridge from Route146 pointwise projection pieces.

Equations

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

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetLowerProjectionBridgeData_from_route146SameTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D)

Route146 replacement for the Route145 lower-projection bridge leaf.

Representative action split into selector, section, and pointwise action #

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

Route146 selector of one representative in Y for each lower class.

quotientRepresentative : B.C → p.fst.Y

Instances For

structure Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.CentralCoverTargetKmodRRepresentativeSectionAtBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : CentralCoverTargetKmodRRepresentativeSelectorBridgeData B D P) (c : B.C) :

Route146 pointwise proof that the selector is a section of the lower projection.

lowerProjection_quotientRepresentative : P.lowerProjection (S.quotientRepresentative c) = c

Instances For

structure Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.CentralCoverTargetKmodRRepresentativeActionAtBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : CentralCoverTargetKmodRRepresentativeSelectorBridgeData B D P) (c : B.C) (m : B.M) :

Route146 pointwise representative-action equality on K/R.

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

Instances For

axiom Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetKmodRRepresentativeSelectorBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) :

Nonempty (CentralCoverTargetKmodRRepresentativeSelectorBridgeData B D P)

Route146 target residual: representative selector.

axiom Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetKmodRRepresentativeSectionAtBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : CentralCoverTargetKmodRRepresentativeSelectorBridgeData B D P) (c : B.C) :

Nonempty (CentralCoverTargetKmodRRepresentativeSectionAtBridgeData B D P S c)

Route146 target residual: pointwise section equality for the selected representative.

axiom Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetKmodRRepresentativeActionAtBridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : CentralCoverTargetKmodRRepresentativeSelectorBridgeData B D P) (c : B.C) (m : B.M) :

Nonempty (CentralCoverTargetKmodRRepresentativeActionAtBridgeData B D P S c m)

Route146 target residual: pointwise representative-action equality.

def Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.representativeActionBridgeData_of_route146Pieces {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (S : CentralCoverTargetKmodRRepresentativeSelectorBridgeData B D P) :

TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D P

Assemble the Route145 representative-action bridge from pointwise Route146 selector/section/action data.

Equations

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

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetKmodRRepresentativeActionBridgeData_from_route146SameTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) :

Nonempty (TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D P)

Route146 replacement for the Route145 representative-action bridge leaf.

Route146 same-tower target reassembly #

structure Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.CentralCoverTargetRoute146BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Route146 bundled target bridge data.

lowerProjectionBridgeData : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D
representativeActionBridgeData : TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D self.lowerProjectionBridgeData)

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetRoute146BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetRoute146BridgeData B D)

Assemble the Route146 bridge data from the pointwise residuals.

def Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.projectedConjugationActionData_of_route146BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute146BridgeData B D) :

TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (TargetKmodRSameTowerBridgeClosers.lowerProjectionData_of_bridge B D H.lowerProjectionBridgeData)

Projected conjugation data induced by the Route146 pointwise bridge.

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.quotientActionData_of_route146BridgeData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute146BridgeData B D) :

TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Quotient-action provider through the Route146 pointwise bridge.

Equations

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

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetKmodRQuotientActionData_from_route146SameTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

Route146 target quotient-action provider.

theorem Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetDecorationKernelData_from_route146SameTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetDecorationKernelData B D)

Drop-in target decoration-kernel provider for Route146.

theorem Q2Presentation.Induction.TargetKmodRRoute146SameTowerClosers.centralCover_targetCanonicalFramedQuotientData_from_route146SameTower {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

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