Incoming boundary bounds for direct heights #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_incoming_le_one
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
(B : S.PrimitiveDirectedBoundaryData D)
(Y : S.SurvivingLabel K)
(hY : (S.factorFiniteTauCategoryData K).IsProjective Y)
:
∑ X : S.SurvivingLabel K,
FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData X Y ≤ 1
The positive coordinate mesh equation bounds the total incoming multiplicity at every projective boundary vertex by one.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_predecessor_unique
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
(B : S.PrimitiveDirectedBoundaryData D)
(Y : S.SurvivingLabel K)
(hY : (S.factorFiniteTauCategoryData K).IsProjective Y)
(X Z : S.SurvivingLabel K)
(hX : FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData X Y ≠ 0)
(hZ : FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData Z Y ≠ 0)
:
X = Z
In particular, a projective boundary vertex has at most one distinct predecessor in the official arrow relation.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_mesh_predecessor
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
(_B : S.PrimitiveDirectedBoundaryData D)
(Y : (S.factorFiniteTauCategoryData K).Nonprojective)
(X : S.SurvivingLabel K)
(hX : FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData X ↑Y ≠ 0)
:
Every predecessor of an interior vertex receives an arrow from its translate, by equality of the official mesh multiplicities.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_local_conditions
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
{D : S.PrimitiveMultiplicityInput K}
(B : S.PrimitiveDirectedBoundaryData D)
:
have E := fun (X Y : S.SurvivingLabel K) =>
FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData X Y ≠ 0;
∀ (Y : S.SurvivingLabel K),
(∀ (X Z : S.SurvivingLabel K), E X Y → E Z Y → X = Z) ∨ ∃ (t : S.SurvivingLabel K), ∀ (X : S.SurvivingLabel K), E X Y → E t X
The actual primitive factor satisfies the complete local predecessor hypothesis of the direct height induction.