Interval arrow multiplicities in the supported graded category #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalArrowFinite
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(m : ℕ)
:
FiniteDimensional k (S.standardFormIntervalAlgebra m)
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.intervalArrowNoetherian
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(m : ℕ)
:
IsNoetherianRing (S.standardFormIntervalAlgebra m)ᵐᵒᵖ
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInterval_arrowMultiplicity_eq_irreducible_finrank
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(m : ℕ)
(T : FiniteIndecomposableSkeleton k (S.standardFormIntervalAlgebra m))
(source target : Fin T.n)
:
FiniteTauMatrix.arrowMultiplicity T.finiteTauCategoryData.toFiniteRightTauCategoryData source target = Module.finrank k
(CategoricalIrreducible.Space k ((S.standardFormIntervalAlgebraEquivalence m).functor.obj (T.fgObj source))
((S.standardFormIntervalAlgebraEquivalence m).functor.obj (T.fgObj target)))
For any complete interval-algebra skeleton, the official arrow count is the intrinsic quotient dimension of its images in supported graded modules.