Ideal membership of the factors in an incoming-summand expansion

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.outgoingComponent_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] {X M : C} (d : FiniteIndecomposableDecomposition M) (I : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal C) (a : X ⟶ M) (ha : a ∈ I.hom X M) (j : Fin d.n) : d.outgoingComponent a j ∈ I.hom X (d.summand j)

Projecting the first factor to a summand preserves membership in any categorical ideal, in particular in the radical.

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.incomingComponent_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] {M Y : C} (d : FiniteIndecomposableDecomposition M) (I : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal C) (b : M ⟶ Y) (hb : b ∈ I.hom M Y) (j : Fin d.n) : d.incomingComponent b j ∈ I.hom (d.summand j) Y

Restricting the second factor to a summand likewise preserves ideal membership. Thus the reduced sum preserves both radical constraints.