Irreducible morphisms do not lie in the categorical radical square

In a finite Krull--Schmidt category, a finite sum of composites of radical morphisms can be consolidated into one factorization through a finite biproduct. Both consolidated factors remain radical. Hence a morphism in the square of the categorical radical cannot be irreducible.

theorem MagnitudeConjecture.FiniteTauMatrix.exists_radical_factorization_of_mem_mul {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) {x y : Ind} {f : T.obj x ⟶ T.obj y} (hf : f ∈ (T.radical.ideal ⋆ᵢ T.radical.ideal).hom (T.obj x) (T.obj y)) : ∃ (M : C) (g : T.obj x ⟶ M) (h : M ⟶ T.obj y), g ∈ T.radical.ideal.hom (T.obj x) M ∧ h ∈ T.radical.ideal.hom M (T.obj y) ∧ CategoryTheory.CategoryStruct.comp g h = f

Membership in the product of the categorical radical with itself can be represented by one composite of two radical morphisms.

theorem MagnitudeConjecture.FiniteTauMatrix.not_isIrreducibleMorphism_of_mem_radical_mul {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 : QuotientSubmoduleEquidistribution.Iyama.FiniteRightTauCategoryData C Ind) {x y : Ind} {f : T.obj x ⟶ T.obj y} (hf : f ∈ (T.radical.ideal ⋆ᵢ T.radical.ideal).hom (T.obj x) (T.obj y)) : ¬QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f

A morphism in the square of the categorical radical between chosen indecomposables is not irreducible.