Lemma 2.5 for mod A

The hypotheses of the abstract Lemma 2.5 (StrictLayers.strict) hold in mod A = FGModuleCat Aᵐᵒᵖ for a representation-finite algebra:

• the right radical approximation of a module Y is the right mesh of Y: the biproduct of the minimal right almost split maps of the indecomposable summands of Y (with rad P → P at projective summands) and its kernel, a biproduct of left almost split maps (graded-category.tex);
• the Krull–Schmidt split–radical normal form.

Both are supplied by the vendored Auslander--Reiten library (moduleRightMesh, moduleRightTau, labelRightMesh_f_mono, exists_splitMono_radical_normalForm).

theorem MultiplicativeBasisDeformations.IndSkeleton.hasSplitRadicalNormalForm {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) : StrictLayers.HasSplitRadicalNormalForm (ModCat A)

The Krull–Schmidt split–radical normal form in mod A.

theorem MultiplicativeBasisDeformations.IndSkeleton.moduleRightMesh_f_mono {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (Y : ModCat A) : CategoryTheory.Mono (S.toVendor.moduleRightMesh Y).f

The first map of the right mesh of a module is a monomorphism.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.rightRadicalApprox {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (Y : ModCat A) : StrictLayers.RightRadicalApprox Y

The right radical approximation of a module, from its right mesh.

theorem MultiplicativeBasisDeformations.IndSkeleton.strict_radical_layers {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (n : ℕ) {U Y : ModCat A} (a : U ⟶ Y) (ha : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism a) (hpert : ∀ h ∈ (StrictLayers.Ipow 2).hom U Y, CategoryTheory.Mono (a + h)) {W : ModCat A} (z : W ⟶ U) (hz : CategoryTheory.CategoryStruct.comp z a ∈ (StrictLayers.Ipow (n + 1)).hom W Y) : z ∈ (StrictLayers.Ipow n).hom W U

Lemma 2.5 (lem:strict-radical-layers) in mod A.