Semantic closers for the target Y/K projection and K/R action

This sidecar refines the two target-side packets left by TargetKmodRActionTransportFinalProofs:

• centralCover_targetLowerProjectionData;
• centralCover_targetKmodRProjectedConjugationActionData.

The lower projection is theorem-level once the canonical lower quotient map Y -> lowerChild and an equivalence from that lower child to the abstract action group B.C are supplied. The action packet is split into a representative-level conjugation law and the assertion that conjugation on K/R depends only on the lower quotient class.

Lower quotient map to the abstract action group

structure Q2Presentation.Induction.TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Type 1

The lower quotient map, before identifying the lower quotient target with the abstract action group B.C.

This is the Y -> C = Y/K part of the manuscript tower. Unlike CentralCoverTargetLowerProjectionData, the codomain is still a framed lower child rather than the abstract module-action group.

• lowerChild : FramedPair
• topToLower : p.fst.Y →* self.lowerChild.fst.Y
• topToLower_surj : Function.Surjective ⇑self.topToLower
• topToLower_ker : self.topToLower.ker = D.Ksub

structure Q2Presentation.Induction.TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetLowerQuotientMapData B D) : Type

Identify the concrete lower child with the abstract group through which B.actM is indexed.

• lowerActionEquiv : Q.lowerChild.fst.Y ≃* B.C

def Q2Presentation.Induction.TargetKmodRProjectionSemanticClosers.lowerQuotientMapData_of_targetQuotientMaps {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetQuotientMapsData B (targetSubgroupTowerData_of_concrete B D)) : CentralCoverTargetLowerQuotientMapData B D

Extract the lower quotient-map packet from a full target quotient-map packet. This is theorem-level bookkeeping from the existing canonical quotient API.

Equations

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

def Q2Presentation.Induction.TargetKmodRProjectionSemanticClosers.lowerQuotientMapData_of_framedQuotient {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (F : CentralCoverTargetCanonicalFramedQuotientData B D) : CentralCoverTargetLowerQuotientMapData B D

Build the lower quotient-map packet directly from a framed quotient witness.

Equations

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

def Q2Presentation.Induction.TargetKmodRProjectionSemanticClosers.lowerProjectionData_of_lowerQuotientMap {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : CentralCoverTargetLowerQuotientMapData B D) (E : CentralCoverTargetLowerActionEquivData B D Q) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D

The canonical lower projection Y -> B.C, assembled from the concrete lower quotient map and the lower-action equivalence.

Equations

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

Projected conjugation from representatives and class-independence

structure Q2Presentation.Induction.TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Type

The abstract B.C-action on M is conjugation on K/R for a coherent choice of representatives of lower quotient classes.

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

structure Q2Presentation.Induction.TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRConjugationClassIndependenceData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Prop

Conjugation on the literal quotient K/R depends only on the lower projection class in B.C.

Manuscript meaning: representatives differing by an element of K induce the same action on K/R, since inner conjugation by K is trivial modulo R = Phi(K).

• quotientConjugate_eq_of_same_projection (y z : p.fst.Y) (q : ↥(Subgroup.map (QuotientGroup.mk' D.Rsub) D.Ksub)) : P.lowerProjection y = P.lowerProjection z → TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D y q = TargetDecorationCanonicalInvarianceProofs.quotientConjugateKmodRPoint B D z q

def Q2Presentation.Induction.TargetKmodRProjectionSemanticClosers.projectedConjugationActionData_of_representatives {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) (A : CentralCoverTargetKmodRRepresentativeActionData B D P) (I : CentralCoverTargetKmodRConjugationClassIndependenceData B D P) : TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P

Assemble the projected conjugation packet from representative-level action compatibility and class-independence of conjugation on K/R.

Equations

• ⋯ = ⋯

Route-ready residual names and reassembly

axiom Q2Presentation.Induction.centralCover_targetLowerQuotientMapData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D)

Smaller residual: construct the lower quotient map Y -> Y/K as a framed lower child, with kernel K.

axiom Q2Presentation.Induction.centralCover_targetLowerActionEquivData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (Q : TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerQuotientMapData B D) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetLowerActionEquivData B D Q)

Smaller residual: identify the lower quotient child with the abstract action group B.C.

theorem Q2Presentation.Induction.centralCover_targetLowerProjectionData_from_projectionSemanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D)

Replacement for centralCover_targetLowerProjectionData, assembled from the lower quotient map and its identification with B.C.

axiom Q2Presentation.Induction.centralCover_targetKmodRRepresentativeActionData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRRepresentativeActionData B D P)

Smaller residual: representative-level action compatibility for the selected lower projection.

axiom Q2Presentation.Induction.centralCover_targetKmodRConjugationClassIndependenceData {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRProjectionSemanticClosers.CentralCoverTargetKmodRConjugationClassIndependenceData B D P)

Smaller residual: conjugation on K/R is independent of the chosen ambient representative of a lower quotient class.

theorem Q2Presentation.Induction.centralCover_targetKmodRProjectedConjugationActionData_from_projectionSemanticClosers {p : FramedPair} (B : MinimalBlock p) (D : CentralCoverTargetSubgroupConcreteData B) (P : TargetKmodRActionTransportFinalProofs.CentralCoverTargetLowerProjectionData B D) : Nonempty (TargetKmodRActionTransportFinalProofs.CentralCoverTargetKmodRProjectedConjugationActionData B D P)

Replacement for centralCover_targetKmodRProjectedConjugationActionData, assembled from representative action compatibility and class-independence.

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

Quotient-action packet through the semantic projection/action split.

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

Downstream action-compatibility packet through the semantic projection/action split.

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

Canonical target-decoration invariance through the semantic projection/action split.

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

Decoration-kernel closure through the semantic projection/action split.

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

Canonical framed quotient closure through the semantic projection/action split.