Lemma 2.5 for an Artin algebra

lem:strict-radical-layers (graded-category.tex): "Let A be any Artin algebra, let J be the radical of its category of finite-length modules […]". The manuscript assumes ordinary Auslander–Reiten theory (main.tex): every indecomposable module Y has a right almost split map E → Y, with kernel 0 (rad P → P at projectives) or a left almost split map out of the indecomposable τY (the almost split sequence). With this input (ARData), Lemma 2.5 holds in the category of finitely generated modules over an Artin algebra (strict_radical_layers_artin).

The Krull–Schmidt input is proved: finitely generated modules are finite biproducts of indecomposables (induction on the length, decomp_module), whose endomorphism rings are local (Fitting, end_isLocalRing); the split–radical normal form and the right radical approximations then come from KrullSchmidtForm.

theorem MultiplicativeBasisDeformations.StrictLayers.end_isLocalRing {A : Type u} [Ring A] (M : ModuleCat A) [IsArtinian A ↑M] [IsNoetherian A ↑M] (hM : CategoryTheory.Indecomposable M) : IsLocalRing (CategoryTheory.End M)

Fitting: the endomorphism ring of an indecomposable finite-length module is local.

theorem MultiplicativeBasisDeformations.StrictLayers.fl_of_split {A : Type u} [Ring A] {M X : ModuleCat A} [IsArtinian A ↑M] [IsNoetherian A ↑M] (i : X ⟶ M) (q : M ⟶ X) (hiq : CategoryTheory.CategoryStruct.comp i q = CategoryTheory.CategoryStruct.id X) : IsArtinian A ↑X ∧ IsNoetherian A ↑X

A split summand of a finite-length module has finite length.

theorem MultiplicativeBasisDeformations.StrictLayers.decomp_module {A : Type u} [Ring A] (d : ℕ) (M : ModuleCat A) [IsArtinian A ↑M] [IsNoetherian A ↑M] : (Module.length A ↑M).toNat = d → Nonempty (MBDVendor.Magnitude.CategoryTheory.FiniteIndecomposableDecomposition M)

Krull–Schmidt existence: a finite-length module is a finite biproduct of indecomposables, by induction on the length.

Finitely generated modules over an Artin algebra

theorem MultiplicativeBasisDeformations.StrictLayers.artin_isArtinianRing {A : Type u} [Ring A] (R : Type u) [CommRing R] [IsArtinianRing R] [Algebra R A] [Module.Finite R A] : IsArtinianRing A

theorem MultiplicativeBasisDeformations.StrictLayers.artin_isNoetherianRing {A : Type u} [Ring A] (R : Type u) [CommRing R] [IsArtinianRing R] [Algebra R A] [Module.Finite R A] : IsNoetherianRing A

theorem MultiplicativeBasisDeformations.StrictLayers.decomp_artin {A : Type u} [Ring A] (R : Type u) [CommRing R] [IsArtinianRing R] [Algebra R A] [Module.Finite R A] [IsNoetherianRing A] (X : FGModuleCat A) : ∃ (n : ℕ) (F : Fin n → FGModuleCat A), (∀ (i : Fin n), ¬CategoryTheory.Limits.IsZero (F i) ∧ IsLocalRing (CategoryTheory.End (F i))) ∧ Nonempty (X ≅ ⨁ F)

Krull–Schmidt for an Artin algebra: every finitely generated module is a finite biproduct of nonzero modules with local endomorphism rings.

theorem MultiplicativeBasisDeformations.StrictLayers.strict_radical_layers_artin {A : Type u} [Ring A] (R : Type u) [CommRing R] [IsArtinianRing R] [Algebra R A] [Module.Finite R A] [IsNoetherianRing A] (hAR : ∀ (Y : FGModuleCat A), ¬CategoryTheory.Limits.IsZero Y → IsLocalRing (CategoryTheory.End Y) → Nonempty (ARData Y)) (n : ℕ) {U Y : FGModuleCat A} (a : U ⟶ Y) (ha : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism a) (hpert : ∀ h ∈ (Ipow 2).hom U Y, CategoryTheory.Mono (a + h)) {W : FGModuleCat A} (z : W ⟶ U) (hz : CategoryTheory.CategoryStruct.comp z a ∈ (Ipow (n + 1)).hom W Y) : z ∈ (Ipow n).hom W U

Lemma 2.5 (lem:strict-radical-layers) for an Artin algebra A over a commutative Artinian ring R, in the category of finitely generated (finite-length) modules, with ordinary Auslander–Reiten theory as input (hAR, assumed by the manuscript, main.tex): for a radical monomorphism-type map a : U → Y with a + h monic for all h ∈ J²(U, Y), z ≫ a ∈ J^{n+1} implies z ∈ J^n.

theorem MultiplicativeBasisDeformations.StrictLayers.strict_radical_layers_artin_iff {A : Type u} [Ring A] (R : Type u) [CommRing R] [IsArtinianRing R] [Algebra R A] [Module.Finite R A] [IsNoetherianRing A] (hAR : ∀ (Y : FGModuleCat A), ¬CategoryTheory.Limits.IsZero Y → IsLocalRing (CategoryTheory.End Y) → Nonempty (ARData Y)) (n : ℕ) {U Y : FGModuleCat A} (a : U ⟶ Y) (ha : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism a) (hpert : ∀ h ∈ (Ipow 2).hom U Y, CategoryTheory.Mono (a + h)) {W : FGModuleCat A} (z : W ⟶ U) : CategoryTheory.CategoryStruct.comp z a ∈ (Ipow (n + 1)).hom W Y ↔ z ∈ (Ipow n).hom W U

Lemma 2.5 (lem:strict-radical-layers) as stated, both directions: for a radical monomorphism a all of whose perturbations by J² are monic, z ≫ a ∈ J^{n+1} if and only if z ∈ J^n.