Interval category modules and the actual interval algebra

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalCategoryAlgebraEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (m : ℕ) : CoveringHom.FiniteDimensionalModuleCategory k ≌ FGModuleCat (principalIntervalAlgebra R ⋯ e he0 he m)ᵐᵒᵖ

The finite functor modules are precisely right modules over the interval matrix algebra.

instance MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalCategoryAlgebraEquivalence_additive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] (R : VectorGrading k A) (hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j)) {ι : Type} [Fintype ι] (e : ι → A) (he0 : ∀ (i : ι), e i ∈ R.component 0) (he : ∀ (i : ι), e i * e i = e i) (m : ℕ) : (principalIntervalCategoryAlgebraEquivalence R ⋯ e he0 he m).functor.Additive