Documentation

Q2Presentation.Induction.TargetKmodRRoute157Closers

Route157 target K/R quotient/action closers #

Route156's target branch reaches TargetKmodRRoute152Closers.centralCover_targetDecorationKernelData_from_route152Closers, whose non-local target frontier is the two Route28 atoms:

This sidecar supplies a drop-in decoration-kernel provider with the same downstream target, but it does not call those Route28 axioms. Instead it uses the concrete lower projection/action facts isolated in Route151:

The first bridge below also shows how those lower projection facts imply the Route28 lower-action surface for any Route28 lower quotient map. The second bridge proves the Route28 representative-action surface for the Route157 selected projection. The main provider uses the still lower projected-action path directly, so its axiom frontier avoids both Route28 target leaves and the broader Route146 quotient/action leaves.

Route151 lower projection as the Route157 selected projection #

source
def Q2Presentation.Induction.TargetKmodRRoute157Closers.lowerProjectionData_of_route157Projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionMapData B D) (HKle : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKsubLeKerData B D P) (HKge : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKerLeKsubData B D P) :
TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

Route157's selected lower projection, assembled from the concrete Route151 map and the two kernel inclusions. Surjectivity is supplied pointwise by the Route151 fibre atom.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Q2Presentation.Induction.TargetKmodRRoute157Closers.route28LowerActionEquivData_of_route157Projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerQuotientMapData B D) (P : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionMapData B D) (HKle : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKsubLeKerData B D P) (HKge : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKerLeKsubData B D P) :
    TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerActionEquivData B D Q

    The Route151 lower projection identifies any Route28 lower child with B.C, because both maps are quotients of Y by the same subgroup K.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Q2Presentation.Induction.TargetKmodRRoute157Closers.centralCover_targetRoute28LowerActionEquivData_from_route157Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerQuotientMapData B D) :
      Nonempty (TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28LowerActionEquivData B D Q)

      Route157 replacement for Route28's lower-action equivalence atom.

      Route28 representative surface for the Route157 selected projection #

      source
      def Q2Presentation.Induction.TargetKmodRRoute157Closers.route28RepresentativeActionData_of_route157Projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionMapData B D) (HKle : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKsubLeKerData B D P) (HKge : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKerLeKsubData B D P) (A : TargetKmodRRoute151Closers.CentralCoverTargetRoute151ProjectedRepresentativeActionData B D P) (S : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeSectionData B D (lowerProjectionData_of_route157Projection B D P HKle HKge)) :
      TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeActionData B D (lowerProjectionData_of_route157Projection B D P HKle HKge) S

      Route151's projected action gives the Route28 selected-representative action packet for the Route157 selected projection.

      Equations
      • ⋯ = ⋯
      Instances For
        source
        theorem Q2Presentation.Induction.TargetKmodRRoute157Closers.centralCover_targetRoute28RepresentativeActionData_from_route157Projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionMapData B D) (HKle : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKsubLeKerData B D P) (HKge : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKerLeKsubData B D P) (S : TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeSectionData B D (lowerProjectionData_of_route157Projection B D P HKle HKge)) :
        Nonempty (TargetKmodRRoute28BridgeProofs.CentralCoverTargetRoute28RepresentativeActionData B D (lowerProjectionData_of_route157Projection B D P HKle HKge) S)

        Route157 bridge to Route28's representative-action surface, restricted to the Route157 selected projection.

        Direct lower target path for the Route152 decoration-kernel consumer #

        source
        def Q2Presentation.Induction.TargetKmodRRoute157Closers.projectedConjugationActionData_of_route157Projection {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionMapData B D) (HKle : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKsubLeKerData B D P) (HKge : TargetKmodRRoute151Closers.CentralCoverTargetRoute151LowerProjectionKerLeKsubData B D P) (A : TargetKmodRRoute151Closers.CentralCoverTargetRoute151ProjectedRepresentativeActionData B D P) :
        TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D (lowerProjectionData_of_route157Projection B D P HKle HKge)

        Convert the Route151 projected action into the transport-final projected conjugation packet for the Route157 selected projection.

        Equations
        • ⋯ = ⋯
        Instances For
          source
          theorem Q2Presentation.Induction.TargetKmodRRoute157Closers.centralCover_targetKmodRProjectedConjugationActionData_from_route157Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
          Nonempty ((P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) ×' TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

          Route157 projected-action provider. This is the lower target path used by the drop-in decoration-kernel theorem.

          source
          theorem Q2Presentation.Induction.TargetKmodRRoute157Closers.centralCover_targetKmodRQuotientActionData_from_route157Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
          Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

          Route157 quotient-action provider.

          source
          theorem Q2Presentation.Induction.TargetKmodRRoute157Closers.centralCover_targetDecorationKernelData_from_route157Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
          Nonempty (CentralCoverTargetDecorationKernelData B D)

          Drop-in decoration-kernel provider for the current Route152 target call site, with the Route28 target leaves replaced by lower projection/action facts.

          source
          theorem Q2Presentation.Induction.TargetKmodRRoute157Closers.centralCover_targetDecorationKernelData_from_route152Closers_route157 {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
          Nonempty (CentralCoverTargetDecorationKernelData B D)

          Name that mirrors the Route152 call site for one-line replacement.

          source
          theorem Q2Presentation.Induction.TargetKmodRRoute157Closers.centralCover_targetCanonicalFramedQuotientData_from_route157Closers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) :
          Nonempty (CentralCoverTargetCanonicalFramedQuotientData B D)

          Convenience framed-quotient provider through Route157.