The radical filtration of ind(mod A)

The powers J^n of the categorical radical of ind(mod A) (graded-category.tex) form a decreasing multiplicative filtration: J^{n+1} ⊆ J^n and J^m ∘ J^n ⊆ J^{m+n}. For a representation-finite algebra the radical is nilpotent: the manuscript argues that J consists of the matrix entries of the Jacobson radical of the endomorphism algebra of a finite additive generator (graded-category.tex). The formal nilpotence uses the vendored nilpotence of the categorical radical of mod A, which is proved by that argument (MBDVendor.Magnitude.Algebra.RightModuleRadical, nilpotentRadicalDataOfArtinianGenerator).

@[simp]

theorem MultiplicativeBasisDeformations.IndSkeleton.radPow_zero {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) (X Y : S.Ind) : S.radPow 0 X Y = ⊤

J^0 is everything.

theorem MultiplicativeBasisDeformations.IndSkeleton.mem_radPow_succ_of {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Z Y : S.Ind} {f : X ⟶ Z} {g : Z ⟶ Y} (hf : S.IsRadical f) {n : ℕ} (hg : g ∈ S.radPow n Z Y) : CategoryTheory.CategoryStruct.comp f g ∈ S.radPow (n + 1) X Y

theorem MultiplicativeBasisDeformations.IndSkeleton.isRadical_precomp {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) {W X Y : S.Ind} (a : W ⟶ X) {f : X ⟶ Y} (hf : S.IsRadical f) : S.IsRadical (CategoryTheory.CategoryStruct.comp a f)

Precomposition with any morphism preserves radical morphisms.

theorem MultiplicativeBasisDeformations.IndSkeleton.isRadical_postcomp {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Y Z : S.Ind} {f : X ⟶ Y} (hf : S.IsRadical f) (b : Y ⟶ Z) : S.IsRadical (CategoryTheory.CategoryStruct.comp f b)

Postcomposition with any morphism preserves radical morphisms.

theorem MultiplicativeBasisDeformations.IndSkeleton.comp_mem_radPow_left {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Y Z : S.Ind} {n : ℕ} {f : X ⟶ Y} (hf : f ∈ S.radPow n X Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f g ∈ S.radPow n X Z

J^n is closed under postcomposition with any morphism.

theorem MultiplicativeBasisDeformations.IndSkeleton.comp_mem_radPow_right {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Y Z : S.Ind} {n : ℕ} (f : X ⟶ Y) {g : Y ⟶ Z} (hg : g ∈ S.radPow n Y Z) : CategoryTheory.CategoryStruct.comp f g ∈ S.radPow n X Z

J^n is closed under precomposition with any morphism.

theorem MultiplicativeBasisDeformations.IndSkeleton.comp_mem_radPow {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) {X Y Z : S.Ind} {m n : ℕ} {f : X ⟶ Y} {g : Y ⟶ Z} (hf : f ∈ S.radPow m X Y) (hg : g ∈ S.radPow n Y Z) : CategoryTheory.CategoryStruct.comp f g ∈ S.radPow (m + n) X Z

The filtration is multiplicative: J^m ∘ J^n ⊆ J^{m+n}.

theorem MultiplicativeBasisDeformations.IndSkeleton.radPow_succ_le {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) (n : ℕ) (X Y : S.Ind) : S.radPow (n + 1) X Y ≤ S.radPow n X Y

The filtration is decreasing: J^{n+1} ⊆ J^n.

theorem MultiplicativeBasisDeformations.IndSkeleton.radPow_anti {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : IndSkeleton k A) {m n : ℕ} (h : m ≤ n) (X Y : S.Ind) : S.radPow n X Y ≤ S.radPow m X Y

theorem MultiplicativeBasisDeformations.IndSkeleton.map_mem_pow_of_mem_radPow {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {n : ℕ} {X Y : S.Ind} {f : X ⟶ Y} (hf : f ∈ S.radPow n X Y) : S.toFG.map f ∈ (S.toVendor.fgNilpotentRadicalData.ideal.pow n).hom (S.toFG.obj X) (S.toFG.obj Y)

The image of J^n in mod A lies in the n-th power of the vendored radical ideal.

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_radPow_eq_bot {k A : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) : ∃ (N : ℕ), ∀ (X Y : S.Ind), S.radPow N X Y = ⊥

For a representation-finite algebra the radical of ind(mod A) is nilpotent.