The primitive poset-space equivalence

The concrete restricted Yoneda functor is faithful and full, and Iyama saturation proves that its image is closed under subobjects. The distinguished sink represents full-support envelopes, so the functor is essentially surjective and hence an equivalence. No realization hypothesis remains.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.equivalenceData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) : R.representableData.EquivalenceData

Fullness, faithfulness, and the saturated-image realization assemble the literal equivalence data for restricted Yoneda.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.equivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) : S.FactorCategory K ≌ PosetSpace.Obj k T

The literal primitive factor is equivalent to the category of finite T-spaces.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.schurRealizationFamily {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} {T : Type u} [Fintype T] [PartialOrder T] [IsAlgClosed k] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (hsink : D.multiplicity ↑D.sink = 1) : PosetSpace.SchurRealizationFamily k T (S.SurvivingLabel K)

Every selected indecomposable becomes a Schur T-space and its total dimension is its primitive multiplicity.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.posetSpaceEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} [IsAlgClosed k] (B : S.PrimitiveDirectedBoundaryData D) : S.FactorCategory K ≌ PosetSpace.Obj k B.ProjectivePoset

The canonical primitive representable functor is unconditionally the literal poset-space equivalence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.schurRealizationFamily {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} [IsAlgClosed k] (B : S.PrimitiveDirectedBoundaryData D) : PosetSpace.SchurRealizationFamily k B.ProjectivePoset (S.SurvivingLabel K)

Canonical Schur realization family for the primitive factor; its multiplicity function is definitionally the manuscript's d_X.