Positive grading transported to Schur poset spaces

The primitive factor is equivalent to the category of finite poset spaces. Every Schur poset space pulls back to a nonzero object with only scalar endomorphisms, hence to one selected indecomposable factor label. Transporting the concrete standard-factor level along this label gives the positive grading needed for the realization-length bound.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.exists_standardFactorLabelIso_of_isSchur {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) (X : PosetSpace.Obj k B.ProjectivePoset) (hX : PosetSpace.IsSchur k B.ProjectivePoset X) : ∃ (x : S.SurvivingLabel K), Nonempty (B.posetSpaceEquivalence.inverse.obj X ≅ S.factorObject K x)

A Schur poset space pulls back along the primitive equivalence to one selected indecomposable factor object.

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

The selected factor label representing a Schur poset space.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorSchurIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) (X : PosetSpace.Obj k B.ProjectivePoset) (hX : PosetSpace.IsSchur k B.ProjectivePoset X) : B.posetSpaceEquivalence.inverse.obj X ≅ S.factorObject K (B.standardFactorSchurLabel X hX)

The pullback of a Schur poset space is isomorphic to its selected factor label.

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

The concrete factor level transported to a Schur poset space. Its value away from the Schur locus is irrelevant to the positive-grading interface.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorSchurLevel_of_isSchur {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) (X : PosetSpace.Obj k B.ProjectivePoset) (hX : PosetSpace.IsSchur k B.ProjectivePoset X) : B.standardFactorSchurLevel X = B.standardFactorLevel (B.standardFactorSchurLabel X hX)

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

The concrete standard-factor grading transports across the completed poset-space equivalence to a positive grading on every Schur poset space.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorRealization_length_bound {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) : ARCount.projectiveCount (S.factorFiniteTauCategoryData K).IsProjective - 1 ≤ ↑B.standardFactorLength

The projective-poset realization gives the manuscript's lower bound on the length of the concrete factor grading.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorIntrinsicEulerExcess_nonnegative {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) : 0 ≤ DirectedDeletion.intrinsicEulerExcess (FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData K))

The concrete translation recurrence and completed poset-space grading prove nonnegativity of the intrinsic Euler excess of the primitive factor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorIntrinsicEulerExcess_eq_zero_iff {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) : DirectedDeletion.intrinsicEulerExcess (FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData K)) = 0 ↔ ↑B.standardFactorLength = ARCount.projectiveCount (S.factorFiniteTauCategoryData K).IsProjective - 1

Vanishing intrinsic factor excess is exactly sharpness of the concrete grading-length bound.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.standardFactorSchur_finrank_eq_one_of_intrinsicEulerExcess_eq_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} {K : Set (Fin S.n)} {D : S.PrimitiveMultiplicityInput K} (B : S.PrimitiveDirectedBoundaryData D) (hzero : DirectedDeletion.intrinsicEulerExcess (FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData K)) = 0) (X : PosetSpace.Obj k B.ProjectivePoset) (hX : PosetSpace.IsSchur k B.ProjectivePoset X) : Module.finrank k X.carrier = 1

Equality in the intrinsic factor estimate forces every Schur object in the completed poset-space realization to be one-dimensional.