Radical powers of ind(mod A) and of mod A

For morphisms between indecomposables, the manuscript-literal radical power J^n of ind(mod A) (composites of n radical maps through indecomposable modules) coincides with the n-th power of the categorical radical of mod A (composites through arbitrary finitely generated modules). This is the general form of mem_radPow_two_iff: an intermediate module is decomposed into indecomposable summands, and the components of radical maps are radical.

theorem MultiplicativeBasisDeformations.IndSkeleton.mem_radPow_iff {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) : f ∈ S.radPow n X Y ↔ S.toFG.map f ∈ (StrictLayers.Ipow n).hom (S.toFG.obj X) (S.toFG.obj Y)

J^n of ind(mod A) is the n-th power of the radical of mod A, on indecomposables.