Canonical target-decoration invariance

This sidecar refines the remaining target-decoration residual centralCover_targetDecorationCanonicalInvarianceData.

Manuscript anchor: §7 lem:decorationblock and §8 lem:covertransform. After TargetDecorationActualDescentProofs proves that the decoration kills R = Phi(K), the descended decoration on K/R is invariant for the actual quotient-conjugation action because thetaY is a homomorphism into an abelian target. The only remaining bridge is that the abstract action B.actM, transported through the selected equivalence K/R ~= M, is the quotient action induced by conjugation in Y/K.

def Q2Presentation.Induction.TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (y : p.fst.Y) (q : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)) : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)

Conjugation by an ambient element on the realized quotient K/R, represented as the image of K in Y/R.

Equations

• Q2Presentation.Induction.TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y q = ⟨((QuotientGroup.mk' D.Rsub) y)⁻¹ * ↑q * (QuotientGroup.mk' D.Rsub) y, ⋯⟩

theorem Q2Presentation.Induction.TargetDecorationCanonicalInvarianceProofs.quotientDecorationHom_conjugate {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (hR : D.Rsub ≤ p.fst.thetaY.ker) (y : p.fst.Y) (q : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)) : (TargetDecorationBlockMapActualProofs.quotientDecorationHom B D hR) (quotientConjugateKmodRPoint B D y q) = (TargetDecorationBlockMapActualProofs.quotientDecorationHom B D hR) q

The descended decoration on K/R is invariant under actual conjugation in the ambient target.

The strictly smaller bridge

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

The selected bridge K/R ~= M is compatible with the quotient action.

This is the remaining manuscript-shaped datum: B.actM is not an arbitrary linear action on the abstract module M; under D.KmodR_equivM, it is induced by conjugation by representatives of the lower quotient C = Y/K.

• quotientRepresentative : B.C → p.fst.Y
• action_compat (c : B.C) (m : B.M) : D.KmodR_equivM.symm (Multiplicative.ofAdd ((B.actM c) m)) = quotientConjugateKmodRPoint B D (self.quotientRepresentative c) (D.KmodR_equivM.symm (Multiplicative.ofAdd m))

def Q2Presentation.Induction.TargetDecorationCanonicalInvarianceProofs.canonicalInvarianceData_of_kmodRActionCompatibility {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (A : CentralCoverTargetKmodRActionCompatibilityData B D) : TargetDecorationActualDescentProofs.CentralCoverTargetDecorationCanonicalInvarianceData B D

The action-compatibility bridge proves the current canonical-invariance packet. The only group-theoretic computation used here is conjugation invariance of a homomorphism into the abelian decoration target.

Equations

• ⋯ = ⋯

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

Strictly smaller residual replacing centralCover_targetDecorationCanonicalInvarianceData.

It asks only that the selected K/R ~= M bridge intertwines the canonical quotient-conjugation action with the abstract action B.actM.

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

Route-ready replacement for the current canonical-invariance residual.

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

Actual decoration descent reassembled from the action-compatibility bridge.

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

Decoration-kernel closure through the action-compatibility bridge.

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

Canonical framed quotient closure through the action-compatibility bridge.