Identifying interval algebras with principal-projective tuples

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalIntervalAlgebraTupleEquiv {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) (r : ℕ) : principalIntervalAlgebra R ⋯ e he0 he r ≃ₐ[k] CategoryTheory.End (principalIntervalTuple R ⋯ e he0 r)

The interval algebra used for module classification equals the direct principal-projective tuple algebra used for separated blocks.

noncomputable def MagnitudeConjecture.Graded.FiniteGradedModule.principalSeparatedBlockAlgebraEquiv {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) (hneg : ∀ d < 0, R.component d = ⊥) (h : ℕ) (hupper : ∀ (d : ℤ), ↑h < d → R.component d = ⊥) (r q : ℕ) : CategoryTheory.End (principalSeparatedBlockTuple R ⋯ e he0 r h q) ≃ₐ[k] Fin q → principalIntervalAlgebra R ⋯ e he0 he r

The algebra of separated translated blocks is the product of the actual small interval algebras.