A finite rank increasing along primitive factor arrows #
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeightRank
{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)}
{D : S.PrimitiveMultiplicityInput K}
(B : S.PrimitiveDirectedBoundaryData D)
(x : S.SurvivingLabel K)
:
ℕ
Number of ambient labels strictly earlier in the directed order.
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeightRank_lt_of_hom
{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}
(f : S.factorObject K x ⟶ S.factorObject K y)
(hf : f ≠ 0)
(hniso : ¬CategoryTheory.IsIso f)
:
B.directHeightRank x < B.directHeightRank y
A nonzero nonisomorphism of the factor strictly increases ambient rank.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directHeightRank_lt_of_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 : FiniteTauMatrix.arrowMultiplicity (S.factorFiniteTauCategoryData K).toFiniteRightTauCategoryData x y ≠ 0)
:
B.directHeightRank x < B.directHeightRank y
Each nonzero official arrow multiplicity supplies an irreducible component, hence strictly increases the rank.