Corollary 12.1: the radical grading of ind(mod B) is C

deformation-refinements.tex: "The Hom normalization makes the M_i^B indecomposable and pairwise nonisomorphic. Proposition 6.5(3) identifies their categorical radical grading with C."

Formalization. The hypotheses of Proposition 6.5(3) hold for the evaluated modules of A₀ (liftHyp, and the graded Hom category is generated in degree one, hgen), so the qth power of the categorical radical of the lifted modules is the filtration order ≥ q (mem_radPow_lifted). Leading terms identify rad^q / rad^{q+1} with the degree-q part of C (leadL: surjective, kernel rad^{q+1}), compatibly with composition (leadC_comp).

The hypotheses of Proposition 6.5(3)

theorem MultiplicativeBasisDeformations.MeshWalk.rs_zero' {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {X Y : V} : rs D 0 = 0

theorem MultiplicativeBasisDeformations.MeshWalk.rs_isGrHom {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {X Y : V} {r : ℕ} {φ : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y} (hφ : φ ∈ ScalarMeshCategory.degreePart c r X Y) : PosFiltration.IsGrHom X Y (↑r) (rs D φ)

theorem MultiplicativeBasisDeformations.MeshWalk.exists_rs_of_isGrHom {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {X Y : V} {r : ℕ} {f : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)} (hf : PosFiltration.IsGrHom X Y (↑r) f) : ∃ φ ∈ ScalarMeshCategory.degreePart c r X Y, f = rs D φ

theorem MultiplicativeBasisDeformations.MeshWalk.liftHyp {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (J : D.InjData) (h1 : DegOne D) : PosFiltration.LiftHyp (gmodEv D hfin)

theorem MultiplicativeBasisDeformations.MeshWalk.rs_mem_grPow {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (n : ℕ) (X Y : V) (φ : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) : φ ∈ ScalarMeshCategory.degreePart c (n + 1) X Y → rs D φ ∈ PosFiltration.grPow n X Y

theorem MultiplicativeBasisDeformations.MeshWalk.hgen {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (n : ℕ) (X Y : V) (f : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c Y)) (hf : PosFiltration.IsGrHom X Y (↑(n + 1)) f) : f ∈ PosFiltration.grPow n X Y

theorem MultiplicativeBasisDeformations.MeshWalk.mem_radPow_lifted {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (Vx : (lenA0 D hfin).Vertices) (J : D.InjData) (h1 : DegOne D) (q : ℕ) {X Y : V} (g : FB Ls X ⟶ FB Ls Y) : toLin g ∈ PosFiltration.radPow Ls.L q X Y ↔ g ∈ filB Ls X Y q

The radical powers of ind(mod B) are the filtration orders (Proposition 6.5(3)).

Leading terms

theorem MultiplicativeBasisDeformations.MeshWalk.exists_lead' {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (Vx : (lenA0 D hfin).Vertices) {X Y : V} (r : ℕ) (f : ↥(filB Ls X Y r)) : ∃ φ ∈ ScalarMeshCategory.degreePart c r X Y, (gmodEv D hfin X).gr.comp (gmodEv D hfin Y).gr (↑r) (toLin ↑f) = rs D φ

noncomputable def MultiplicativeBasisDeformations.MeshWalk.leadC {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (Vx : (lenA0 D hfin).Vertices) {X Y : V} (r : ℕ) (f : ↥(filB Ls X Y r)) : ↥(ScalarMeshCategory.degreePart c r X Y)

The leading term of a map of order ≥ r, a morphism of C of degree r.

theorem MultiplicativeBasisDeformations.MeshWalk.rs_leadC {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (Vx : (lenA0 D hfin).Vertices) {X Y : V} (r : ℕ) (f : ↥(filB Ls X Y r)) : rs D ↑(leadC Ls Vx r f) = (gmodEv D hfin X).gr.comp (gmodEv D hfin Y).gr (↑r) (toLin ↑f)

theorem MultiplicativeBasisDeformations.MeshWalk.leadC_eq {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (Vx : (lenA0 D hfin).Vertices) {X Y : V} (r : ℕ) (f : ↥(filB Ls X Y r)) {φ : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y} (h : (gmodEv D hfin X).gr.comp (gmodEv D hfin Y).gr (↑r) (toLin ↑f) = rs D φ) : ↑(leadC Ls Vx r f) = φ

noncomputable def MultiplicativeBasisDeformations.MeshWalk.leadL {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (Vx : (lenA0 D hfin).Vertices) {X Y : V} (r : ℕ) : ↥(filB Ls X Y r) →ₗ[k] ↥(ScalarMeshCategory.degreePart c r X Y)

The leading-term map rad^r(M_X^B, M_Y^B) → C_r(X, Y).

theorem MultiplicativeBasisDeformations.MeshWalk.leadL_surjective {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (Vx : (lenA0 D hfin).Vertices) (J : D.InjData) (h1 : DegOne D) {X Y : V} (r : ℕ) : Function.Surjective ⇑(leadL Ls Vx r)

theorem MultiplicativeBasisDeformations.MeshWalk.leadL_eq_zero_iff {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (Vx : (lenA0 D hfin).Vertices) (J : D.InjData) (h1 : DegOne D) {X Y : V} (r : ℕ) (f : ↥(filB Ls X Y r)) : (leadL Ls Vx r) f = 0 ↔ ↑f ∈ filB Ls X Y (r + 1)

theorem MultiplicativeBasisDeformations.MeshWalk.comp_mem_filB {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) {X Y Z : V} {r s : ℕ} {f : FB Ls X ⟶ FB Ls Y} {g : FB Ls Y ⟶ FB Ls Z} (hf : f ∈ filB Ls X Y r) (hg : g ∈ filB Ls Y Z s) : CategoryTheory.CategoryStruct.comp f g ∈ filB Ls X Z (r + s)

theorem MultiplicativeBasisDeformations.MeshWalk.leadC_comp {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] {P : PosFiltration (lenA0 D hfin) B} (Ls : Lifts D hfin P) (Vx : (lenA0 D hfin).Vertices) {X Y Z : V} {r s : ℕ} (f : ↥(filB Ls X Y r)) (g : ↥(filB Ls Y Z s)) : ↑(leadC Ls Vx (r + s) ⟨CategoryTheory.CategoryStruct.comp ↑f ↑g, ⋯⟩) = CategoryTheory.CategoryStruct.comp ↑(leadC Ls Vx r f) ↑(leadC Ls Vx s g)

Leading terms are multiplicative: gr_J ind(mod B) ≅ C as categories.

Corollary 12.1

theorem MultiplicativeBasisDeformations.MeshWalk.positiveDeformationCompleteness {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {B : Type u} [Ring B] [Algebra k B] (P : PosFiltration (lenA0 D hfin) B) (J : D.InjData) (h1 : DegOne D) (hrad : ∀ (x y : V) (d : ℕ), 1 ≤ d → ∀ f ∈ ScalarMeshCategory.degreePart c d x y, f ∈ L.rad x y) : Nonempty (Lifts D hfin P) ∧ IsRepresentationFinite k B ∧ ∀ (Ls : Lifts D hfin P), (∀ (x : V), IsFiniteIndecomposable k B (FB Ls x)) ∧ (∀ (x y : V), Nonempty (FB Ls x ≅ FB Ls y) → x = y) ∧ (∀ (M : RightModuleCat B), IsFiniteIndecomposable k B M → ∃ (x : V), Nonempty (M ≅ FB Ls x)) ∧ (∀ (q : ℕ) (x y : V) (g : FB Ls x ⟶ FB Ls y), toLin g ∈ PosFiltration.radPow Ls.L q x y ↔ g ∈ filB Ls x y q) ∧ (∀ (r : ℕ) (x y : V), Function.Surjective ⇑(leadL Ls (vxIdem D hfin) r) ∧ ∀ (f : ↥(filB Ls x y r)), (leadL Ls (vxIdem D hfin) r) f = 0 ↔ ↑f ∈ filB Ls x y (r + 1)) ∧ ∀ (r s : ℕ) (x y z : V) (f : ↥(filB Ls x y r)) (g : ↥(filB Ls y z s)), ↑(leadC Ls (vxIdem D hfin) (r + s) ⟨CategoryTheory.CategoryStruct.comp ↑f ↑g, ⋯⟩) = CategoryTheory.CategoryStruct.comp ↑(leadC Ls (vxIdem D hfin) r f) ↑(leadC Ls (vxIdem D hfin) s g)

Corollary 12.1 (cor:positive-deformation-completeness) for mesh data whose positive degrees are radical. Every positive filtered deformation B of A₀ is representation-finite; the lifted modules M_x^B (which exist, Proposition 6.5) are indecomposable, pairwise nonisomorphic and exhaust the indecomposable B-modules; the qth radical power of ind(mod B) is the filtration order ≥ q, and leading terms identify rad^q / rad^{q+1} with C_q, compatibly with composition: gr_J ind(mod B) ≅ C with these labels.

theorem MultiplicativeBasisDeformations.IndSkeleton.arHrad {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) (d : ℕ) (hd : 1 ≤ d) (f : S.meshObj b x ⟶ S.meshObj b y) (hf : f ∈ ScalarMeshCategory.degreePart (S.arCoefficients b) d x y) : f ∈ (S.arLocal b).rad x y

In k(Γ_A), morphisms of positive degree are radical.

theorem MultiplicativeBasisDeformations.IndSkeleton.finiteDimensional_meshFam {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 (MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) x ⟶ MeshWalk.meshFam S.arTranslationQuiver (S.arCoefficients b) y)

theorem MultiplicativeBasisDeformations.IndSkeleton.positiveDeformationCompleteness_ar {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) {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration (MeshWalk.lenA0 (S.arMeshData b) ⋯) B) : Nonempty (MeshWalk.Lifts (S.arMeshData b) ⋯ P) ∧ IsRepresentationFinite k B ∧ ∀ (Ls : MeshWalk.Lifts (S.arMeshData b) ⋯ P), (∀ (x : S.ARVertex), IsFiniteIndecomposable k B (MeshWalk.FB Ls x)) ∧ (∀ (x y : S.ARVertex), Nonempty (MeshWalk.FB Ls x ≅ MeshWalk.FB Ls y) → x = y) ∧ (∀ (M : RightModuleCat B), IsFiniteIndecomposable k B M → ∃ (x : S.ARVertex), Nonempty (M ≅ MeshWalk.FB Ls x)) ∧ (∀ (q : ℕ) (x y : S.ARVertex) (g : MeshWalk.FB Ls x ⟶ MeshWalk.FB Ls y), MeshWalk.toLin g ∈ PosFiltration.radPow Ls.L q x y ↔ g ∈ MeshWalk.filB Ls x y q) ∧ (∀ (r : ℕ) (x y : S.ARVertex), Function.Surjective ⇑(MeshWalk.leadL Ls (MeshWalk.vxIdem (S.arMeshData b) ⋯) r) ∧ ∀ (f : ↥(MeshWalk.filB Ls x y r)), (MeshWalk.leadL Ls (MeshWalk.vxIdem (S.arMeshData b) ⋯) r) f = 0 ↔ ↑f ∈ MeshWalk.filB Ls x y (r + 1)) ∧ ∀ (r s : ℕ) (x y z : S.ARVertex) (f : ↥(MeshWalk.filB Ls x y r)) (g : ↥(MeshWalk.filB Ls y z s)), ↑(MeshWalk.leadC Ls (MeshWalk.vxIdem (S.arMeshData b) ⋯) (r + s) ⟨CategoryTheory.CategoryStruct.comp ↑f ↑g, ⋯⟩) = CategoryTheory.CategoryStruct.comp ↑(MeshWalk.leadC Ls (MeshWalk.vxIdem (S.arMeshData b) ⋯) r f) ↑(MeshWalk.leadC Ls (MeshWalk.vxIdem (S.arMeshData b) ⋯) s g)

Corollary 12.1 for the algebra A₀ of a basic representation-finite algebra A (Construction 2.8): every positive filtered deformation B of A₀ is representation-finite, the lifted modules M_x^B are a skeleton of ind(mod B), and gr_J ind(mod B) ≅ k(Γ_A) with these labels.