Target K/R action compatibility

This sidecar refines the residual centralCover_targetKmodRActionCompatibilityData.

Manuscript anchor: §7 eq:targettower and §8 lem:decorationblock / lem:covertransform. The selected abstract lower group B.C should be the actual quotient Y/K, and the selected action B.actM on the elementary module M = K/R should be the quotient action induced by right conjugation in Y.

The packet below is closer to that concrete tower than an arbitrary family of representatives: it supplies an equivalence Y/K ~= B.C and a pointwise equation for every ambient representative y : Y. Representatives for the older packet are then chosen from the quotient map.

def Q2Presentation.Induction.TargetKmodRActionProofs.lowerQuotientClass {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (y : p.fst.Y) : p.fst.Y ⧸ D.Ksub

The class of an ambient element in the lower quotient Y/K.

Equations

• Q2Presentation.Induction.TargetKmodRActionProofs.lowerQuotientClass B D y = (QuotientGroup.mk' D.Ksub) y

Concrete action-realization packet

structure Q2Presentation.Induction.TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type

Concrete provenance that the abstract C-action on M is the action induced from the lower quotient Y/K.

The equation is stated for every ambient representative y, not merely for a chosen representative of each class. This is the Lean form of the manuscript tower B = Y/R, C = Y/K, M = K/R, with the manuscript right-conjugation convention x^y = y⁻¹xy.

• lowerQuotientEquiv : p.fst.Y ⧸ D.Ksub ≃* B.C

  The abstract lower group in the minimal block is the actual quotient Y/K.

• action_realizes_conjugation (y : p.fst.Y) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM (self.lowerQuotientEquiv (lowerQuotientClass B D y))) m)) = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

  Transporting B.actM back along K/R ~= M gives right conjugation by any representative of the corresponding class in Y/K.

def Q2Presentation.Induction.TargetKmodRActionProofs.quotientRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetKmodRQuotientActionData B D) (c : B.C) : p.fst.Y

A representative of c : B.C, chosen through the concrete quotient equivalence Y/K ~= B.C.

Equations

• Q2Presentation.Induction.TargetKmodRActionProofs.quotientRepresentative B D A c = Classical.choose ⋯

theorem Q2Presentation.Induction.TargetKmodRActionProofs.lowerQuotientEquiv_quotientRepresentative {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetKmodRQuotientActionData B D) (c : B.C) : A.lowerQuotientEquiv (lowerQuotientClass B D (quotientRepresentative B D A c)) = c

After applying Y/K ~= B.C, the chosen representative is exactly c.

def Q2Presentation.Induction.TargetKmodRActionProofs.kmodRActionCompatibilityData_of_quotientAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetKmodRQuotientActionData B D) : TargetDecorationCanonicalInvarianceProofs.CentralCoverTargetKmodRActionCompatibilityData B D

The concrete quotient-action packet supplies the previous residual packet.

Equations

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

Route-ready reassembly

axiom Q2Presentation.Induction.centralCover_targetKmodRQuotientActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionProofs.CentralCoverTargetKmodRQuotientActionData B D)

Refined residual for the target K/R action bridge.

This is the concrete group-tower packet behind centralCover_targetKmodRActionCompatibilityData: it identifies the lower quotient as Y/K and states that B.actM is the quotient-conjugation action on K/R.

theorem Q2Presentation.Induction.centralCover_targetKmodRActionCompatibilityData_proven {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationCanonicalInvarianceProofs.CentralCoverTargetKmodRActionCompatibilityData B D)

The current target action-compatibility packet follows from the concrete quotient-action packet above.

theorem Q2Presentation.Induction.centralCover_targetDecorationCanonicalInvarianceData_from_kmodRQuotientAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationActualDescentProofs.CentralCoverTargetDecorationCanonicalInvarianceData B D)

Canonical target-decoration invariance routed through the concrete quotient action packet, without using the older action-compatibility axiom.

theorem Q2Presentation.Induction.centralCover_targetDecorationActualDescentData_from_kmodRQuotientAction {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetDecorationBlockMapActualProofs.CentralCoverTargetDecorationActualDescentData B D)

Actual target-decoration descent routed through the concrete quotient action.

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

Decoration-kernel closure routed through the concrete quotient action.

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

Canonical framed quotient closure routed through the concrete quotient action.