Fullness of the primitive incidence realization

The boundary generator used by the minimal-realization argument is reindexed as the root projective followed by the projectives of the finite poset. A map of represented poset spaces then lifts to a module map on its restricted Yoneda representables, and boundary-generator fullness lifts that module map to the required categorical morphism.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryFamilyIso {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] (R : S.PrimitiveProjectivePosetData D T) (q : Option T) : R.representableData.boundaryFamily q ≅ S.factorObject K ↑(R.projectiveEquiv.symm q)

The root-plus-poset boundary family is componentwise the original family of all factor tau-projectives, after reindexing by projectiveEquiv.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryGeneratorIso {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] (R : S.PrimitiveProjectivePosetData D T) : R.representableData.boundaryGenerator ≅ S.factorProjectiveGenerator K

The root-plus-poset boundary biproduct is isomorphic to the literal biproduct of all factor tau-projectives.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryRestrictedYoneda_faithful {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] (R : S.PrimitiveProjectivePosetData D T) : (CategoryTheory.preadditiveCoyonedaObj R.representableData.boundaryGenerator).Faithful

The root-plus-poset boundary generator remains faithful.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryGenerator_presentations {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] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) (X : S.FactorCategory K) : Nonempty (CategoryTheory.FiniteAddGeneratorPresentation R.representableData.boundaryGenerator X)

Every factor object has a two-term presentation by the reindexed root-plus-poset boundary generator.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.boundaryRestrictedYoneda_full {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] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) : (CategoryTheory.preadditiveCoyonedaObj R.representableData.boundaryGenerator).Full

Restricted Yoneda is full after the boundary generator is reindexed as the root followed by the projective poset.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePosetData.representable_full {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] (R : S.PrimitiveProjectivePosetData D T) (H : S.HasAcyclicNonzeroNonisomorphisms) : R.representableData.functor.Full

The concrete primitive representable functor to finite poset spaces is full.