Graded Hom dimensions

eq:graded-hom-dimensions (graded-category.tex): dim C(X, Y) = ∑_n dim J^n(X, Y)/J^{n+1}(X, Y) = dim Hom_A(X, Y), "from the finite radical filtration". The first equality is the decomposition of the Hom spaces of k(Γ_A) into finitely many degree parts together with Proposition 2.6(3); the second is the telescoping of the radical filtration.

theorem MultiplicativeBasisDeformations.IndSkeleton.sum_finrank_layer {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (X Y : S.Ind) (N : ℕ) : ∑ d ∈ Finset.range N, Module.finrank k (S.layer d X Y) + Module.finrank k ↥(S.radPow N X Y) = Module.finrank k (X ⟶ Y)

Telescoping the radical filtration.

theorem MultiplicativeBasisDeformations.IndSkeleton.sum_finrank_layer_eq {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (X Y : S.Ind) {N : ℕ} (hN : ∀ (X Y : S.Ind), S.radPow N X Y = ⊥) : ∑ d ∈ Finset.range N, Module.finrank k (S.layer d X Y) = Module.finrank k (X ⟶ Y)

theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_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) : Module.finrank k (S.meshObj b x ⟶ S.meshObj b y) = Module.finrank k (S.label x ⟶ S.label y)

eq:graded-hom-dimensions: dim C(x, y) = dim Hom_A(x, y).