Source normalization of the direct factor height #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeight_source_incoming_zero
{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)
:
∑ X : S.SurvivingLabel K,
FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData X D.source = 0
The source mesh equation has zero incoming contribution.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorArrow_source_false
{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)
(X : S.SurvivingLabel K)
:
¬directFactorArrow X D.source
No official arrow ends at the distinguished source.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorHeight_source
{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)
:
B.directFactorHeight D.source = 0
The actual direct height is normalized to zero at P.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorHeight_eq_zero_iff
{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)
:
B.directFactorHeight Y = 0 ↔ Y = D.source
A vertex of height zero must be the distinguished source.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactor_source_reaches
{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)
:
Relation.ReflTransGen directFactorArrow D.source Y
Every surviving vertex is reached from P by official arrows.