Documentation

Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers

Route147 same-tower target pointwise closers #

Route147 currently uses the Route146 pointwise target atoms:

a raw lower projection map, fibres, and two kernel inclusions;
a representative selector, pointwise section equalities, and pointwise representative-action equalities.

This sidecar ties those pointwise packets to the literal same-tower quotient semantics already isolated in TargetKmodRRoute146BridgeClosers: the lower target is Y/K, identified with B.C, and representatives are the theorem-level representatives of literal Y/K classes. Six pointwise atoms are therefore theorem-level from the quotient equivalence; the action pointwise atom is reduced to the literal representative-action atom.

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.CentralCoverTargetRoute147LowerQuotientEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Equations

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

Instances For

@[reducible, inline]

abbrev Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.CentralCoverTargetRoute147LiteralRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) :

Equations

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

Instances For

Pointwise projection packets from the literal quotient #

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.lowerProjectionMapBridgeData_of_lowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) :

TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionMapBridgeData B D

Route147 closes the raw pointwise map packet from a literal lower quotient equivalence Y/K ~= B.C.

Equations

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

Instances For

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.lowerProjectionSurjFiberBridgeData_of_lowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) (c : B.C) :

TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionSurjFiberBridgeData B D (lowerProjectionMapBridgeData_of_lowerQuotientEquiv B D E) c

Route147 closes each pointwise fibre of the selected lower projection.

Equations

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

Instances For

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.lowerProjectionKsubLeKerBridgeData_of_lowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) :

TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionKsubLeKerBridgeData B D (lowerProjectionMapBridgeData_of_lowerQuotientEquiv B D E)

Route147 closes K <= ker(lowerProjection) for the selected quotient map.

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.lowerProjectionKerLeKsubBridgeData_of_lowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) :

TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionKerLeKsubBridgeData B D (lowerProjectionMapBridgeData_of_lowerQuotientEquiv B D E)

Route147 closes ker(lowerProjection) <= K for the selected quotient map.

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.lowerProjectionBridgeData_of_route147Pointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) :

TargetKmodRSameTowerBridgeClosers.CentralCoverTargetLowerProjectionBridgeData B D

The selected pointwise projection pieces reassemble the lower projection bridge without using the Route146 pointwise axioms.

Equations

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

Instances For

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.lowerProjectionData_of_route147LowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) :

TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Equations

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

Instances For

Pointwise representative packets from literal representatives #

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.representativeSelectorBridgeData_of_lowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) :

TargetKmodRRoute146SameTowerClosers.CentralCoverTargetKmodRRepresentativeSelectorBridgeData B D (lowerProjectionData_of_route147LowerQuotientEquiv B D E)

Route147 closes the selector packet by selecting representatives of literal Y/K classes through the quotient equivalence.

Equations

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

Instances For

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.representativeSectionAtBridgeData_of_lowerQuotientEquiv {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) (c : B.C) :

TargetKmodRRoute146SameTowerClosers.CentralCoverTargetKmodRRepresentativeSectionAtBridgeData B D (lowerProjectionData_of_route147LowerQuotientEquiv B D E) (representativeSelectorBridgeData_of_lowerQuotientEquiv B D E) c

Route147 closes the pointwise section equality for the selected literal representative.

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.representativeActionAtBridgeData_of_literal {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) (A : CentralCoverTargetRoute147LiteralRepresentativeActionData B D E) (c : B.C) (m : B.M) :

TargetKmodRRoute146SameTowerClosers.CentralCoverTargetKmodRRepresentativeActionAtBridgeData B D (lowerProjectionData_of_route147LowerQuotientEquiv B D E) (representativeSelectorBridgeData_of_lowerQuotientEquiv B D E) c m

Route147 lowers the pointwise action equality to the literal representative-action atom.

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.representativeActionBridgeData_of_route147Pointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) (A : CentralCoverTargetRoute147LiteralRepresentativeActionData B D E) :

TargetKmodRSameTowerBridgeClosers.CentralCoverTargetKmodRRepresentativeActionBridgeData B D (lowerProjectionData_of_route147LowerQuotientEquiv B D E)

The selected pointwise representative pieces reassemble the representative bridge without using the Route146 pointwise selector/section/action axioms.

Equations

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

Instances For

Public replacement theorems for the Route147 pointwise surface #

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetLowerProjectionMapBridgeData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionMapBridgeData B D)

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetLowerProjectionSurjFiberBridgeData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) (c : B.C) :

Nonempty (TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionSurjFiberBridgeData B D (lowerProjectionMapBridgeData_of_lowerQuotientEquiv B D E) c)

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetLowerProjectionKsubLeKerBridgeData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) :

Nonempty (TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionKsubLeKerBridgeData B D (lowerProjectionMapBridgeData_of_lowerQuotientEquiv B D E))

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetLowerProjectionKerLeKsubBridgeData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) :

Nonempty (TargetKmodRRoute146SameTowerClosers.CentralCoverTargetLowerProjectionKerLeKsubBridgeData B D (lowerProjectionMapBridgeData_of_lowerQuotientEquiv B D E))

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetKmodRRepresentativeSelectorBridgeData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) :

Nonempty (TargetKmodRRoute146SameTowerClosers.CentralCoverTargetKmodRRepresentativeSelectorBridgeData B D (lowerProjectionData_of_route147LowerQuotientEquiv B D E))

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetKmodRRepresentativeSectionAtBridgeData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) (c : B.C) :

Nonempty (TargetKmodRRoute146SameTowerClosers.CentralCoverTargetKmodRRepresentativeSectionAtBridgeData B D (lowerProjectionData_of_route147LowerQuotientEquiv B D E) (representativeSelectorBridgeData_of_lowerQuotientEquiv B D E) c)

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetKmodRRepresentativeActionAtBridgeData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (E : CentralCoverTargetRoute147LowerQuotientEquivData B D) (c : B.C) (m : B.M) :

Nonempty (TargetKmodRRoute146SameTowerClosers.CentralCoverTargetKmodRRepresentativeActionAtBridgeData B D (lowerProjectionData_of_route147LowerQuotientEquiv B D E) (representativeSelectorBridgeData_of_lowerQuotientEquiv B D E) c m)

Drop-in provider #

structure Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.CentralCoverTargetRoute147SameTowerPointwiseData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Route147 pointwise data bundled around the same literal quotient identification.

lowerQuotientEquivData : CentralCoverTargetRoute147LowerQuotientEquivData B D
literalRepresentativeActionData : CentralCoverTargetRoute147LiteralRepresentativeActionData B D self.lowerQuotientEquivData

Instances For

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.route146SameTowerBridgeData_of_route147Pointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute147SameTowerPointwiseData B D) :

TargetKmodRRoute146SameTowerClosers.CentralCoverTargetRoute146BridgeData B D

Equations

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

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetRoute147SameTowerPointwiseData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetRoute147SameTowerPointwiseData B D)

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetRoute146BridgeData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetKmodRRoute146SameTowerClosers.CentralCoverTargetRoute146BridgeData B D)

def Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.quotientActionData_of_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (H : CentralCoverTargetRoute147SameTowerPointwiseData B D) :

TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D

Equations

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

Instances For

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetKmodRQuotientActionData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetDecorationKernelData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetDecorationKernelData B D)

Drop-in target decoration-kernel provider for Route147 same-tower pointwise closers.

theorem Q2Presentation.Induction.TargetKmodRRoute147SameTowerPointwiseClosers.centralCover_targetCanonicalFramedQuotientData_from_route147SameTowerPointwise {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :

Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)