Zero excess implies one-dimensional Schur poset spaces #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directPoset_no_threeAntichain
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(hz :
DirectedDeletion.intrinsicEulerExcess
(FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D))) = 0)
(a b c : B.ProjectivePoset)
:
¬PosetSpace.IsThreeAntichain a b c
The two-square argument rules out three pairwise incomparable elements.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directSchur_finrank_eq_one_of_excess_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(hz :
DirectedDeletion.intrinsicEulerExcess
(FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D))) = 0)
(X : PosetSpace.Obj k B.ProjectivePoset)
(hX : PosetSpace.IsSchur k B.ProjectivePoset X)
:
Module.finrank k X.carrier = 1
The sharp direct height, two upper-set squares, and a basis adapted to two filtrations imply that every Schur poset space is one-dimensional.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directMultiplicity_eq_one_of_excess_zero
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{e : A}
{D : PrimitiveIdempotentData e}
(B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D))
(hz :
DirectedDeletion.intrinsicEulerExcess
(FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D))) = 0)
(x : S.SurvivingLabel (S.primitiveKilledLabels D))
:
S.primitiveMultiplicity D ↑x = 1
Zero intrinsic excess forces multiplicity one for every actual surviving indecomposable, using the generated-relations realization.