k(Γ_A) is finite-dimensional

graded-category.tex, eq. (2.15) of the proof of Proposition 2.10: "dim C(X, Y) = ∑_n dim J^n(X, Y)/J^{n+1}(X, Y) = dim Hom_A(X, Y). It follows from the finite radical filtration." By Proposition 2.6(3) the Hom spaces of k(Γ_A) are the direct sums of their degree parts, which are the radical layers; these vanish from the nilpotency index of the radical on.

instance MultiplicativeBasisDeformations.IndSkeleton.finiteDimensional_degreePart {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (d : ℕ) (x y : S.ARVertex) : FiniteDimensional k ↥(ScalarMeshCategory.degreePart (S.arCoefficients b) d x y)

theorem MultiplicativeBasisDeformations.IndSkeleton.degreePart_eq_bot {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) {N : ℕ} (hN : ∀ (X Y : S.Ind), S.radPow N X Y = ⊥) {d : ℕ} (hd : N ≤ d) (x y : S.ARVertex) : ScalarMeshCategory.degreePart (S.arCoefficients b) d x y = ⊥

theorem MultiplicativeBasisDeformations.IndSkeleton.finiteDimensional_meshHom {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x y : S.ARVertex) : FiniteDimensional k (S.meshObj b x ⟶ S.meshObj b y)

The Hom spaces of k(Γ_A) are finite-dimensional.