The finite interval algebra of the graded standard form

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardIntervalAlgebraBaseFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : FiniteDimensional k (S.standardFormAlgebra ⋯)

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalAlgebra {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) : Type u

The finite interval algebra for the actual graded standard form.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalAlgebra_finiteDimensional {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)

The standard-form interval algebra is finite dimensional.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalAlgebraEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) : FGModuleCat (S.standardFormIntervalAlgebra m)ᵐᵒᵖ ≌ S.standardFormSupportedCategory m

Modules over the standard-form interval algebra realize exactly the actual supported graded modules.