Sharp upper-set heights in a zero-excess primitive factor #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_sink_eq_card_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)
:
B.directFactorHeight (S.primitiveMultiplicityInput D).sink = Fintype.card B.ProjectivePoset
Zero excess makes the direct sink height equal to the size of the poset.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directSchurLevel_line_eq_card_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)
(U : Finset B.ProjectivePoset)
(hU : IsUpperSet ↑U)
:
B.directFactorSchurLevel (PosetSpace.line k B.ProjectivePoset (↑U) hU) = U.card
Every upper-set line has its support cardinality as direct height in the equality case.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_lineLabel_eq_card_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)
(U : Finset B.ProjectivePoset)
(hU : IsUpperSet ↑U)
:
B.directFactorHeight (B.directFactorSchurLabel (PosetSpace.line k B.ProjectivePoset (↑U) hU) ⋯) = U.card
The actual selected factor representative of an upper-set line has height equal to the support cardinality.