Radical and nonmonicity foundations for Iyama ladders

This file supplies the elementwise starting point of Iyama's ladder extraction. Failure of monicity gives a literal nonzero left annihilator; nilpotence lets that annihilator escape some radical power; and, on a chosen indecomposable with local endomorphism ring, categorical-radical membership is equivalent to failure of split monicity.

theorem QuotientSubmoduleEquidistribution.Iyama.exists_nonzero_comp_eq_zero_of_not_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {X Y : C} {f : X ⟶ Y} (hf : ¬CategoryTheory.Mono f) : ∃ (W : C) (s : W ⟶ X), s ≠ 0 ∧ CategoryTheory.CategoryStruct.comp s f = 0

In a preadditive category, failure of monicity has a literal nonzero left annihilator.

theorem QuotientSubmoduleEquidistribution.Iyama.exists_power_not_mem_of_ne_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {X Y : C} {f : X ⟶ Y} (hf : f ≠ 0) : ∃ (n : ℕ), f ∉ (R.ideal.pow n).hom X Y

A nonzero morphism escapes some power of a nilpotent categorical radical.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.isRadicalMorphism_iff_not_isSplitMono_from_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {x : Ind} {Y : C} (f : T.obj x ⟶ Y) : CategoricalRadical.IsRadicalMorphism f ↔ ¬CategoryTheory.IsSplitMono f

For a chosen indecomposable with local endomorphism ring, the intrinsic categorical radical consists exactly of the morphisms which are not split monomorphisms. No module-category realization is used.

theorem QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData.isRadicalMorphism_iff_not_isSplitEpi_to_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteRightTauCategoryData C Ind) {x : Ind} {M : C} (f : M ⟶ T.obj x) : CategoricalRadical.IsRadicalMorphism f ↔ ¬CategoryTheory.IsSplitEpi f

Dually, a morphism into a chosen indecomposable is radical exactly when it is not a split epimorphism. This uses only the finite Krull--Schmidt skeleton, not any chosen left tau-sequences.