Direct heights on the actual primitive factor #
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directFactorArrow
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
{S : FiniteIndecomposableSkeleton k A}
{K : Set (Fin S.n)}
(X Y : S.SurvivingLabel K)
:
The official nonzero-arrow relation in the primitive factor.
Instances For
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorHeight
{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)
:
S.SurvivingLabel K → ℕ
Height constructed by predecessor induction, without standardness.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorHeight_arrow
{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 Y : S.SurvivingLabel K)
(h : directFactorArrow X Y)
:
B.directFactorHeight Y = B.directFactorHeight X + 1
Every actual arrow increases the direct height by one.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.directFactorArrow_rightMiddleLabel
{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)}
(Y : S.SurvivingLabel K)
(i : Fin (FiniteTauMatrix.rightMiddleArity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData Y))
:
Every nonempty chosen middle term provides a nonzero incoming arrow.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directFactorHeight_tauPlus
{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)
:
B.directFactorHeight ↑Y = B.directFactorHeight ((S.factorFiniteTauCategoryData K).tauPlus Y) + 2
Translation lowers the direct height by two.