Intrinsic radical-square comparison at an incoming-closed target

theorem MagnitudeConjecture.radical_comap_fullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.ObjectProperty C) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.comap P.ι QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal = QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal

The intrinsic radical in a full subcategory is the restricted ambient radical.

theorem MagnitudeConjecture.radicalSquare_fullSubcategory_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] (hdec : ∀ (M : C), Nonempty (CategoryTheory.FiniteIndecomposableDecomposition M)) (X Y : P.FullSubcategory) (hY : ∀ (Z : C), CategoryTheory.Indecomposable Z → ∀ (b : Z ⟶ Y.obj), b ≠ 0 → P Z) (f : X ⟶ Y) : f.hom ∈ (QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal ⋆ᵢ QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal).hom X.obj Y.obj ↔ f ∈ (QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal ⋆ᵢ QuotientSubmoduleEquidistribution.CategoricalRadical.homIdeal).hom X Y

If all nonzero incoming indecomposables to the target lie in the full subcategory, its intrinsic radical square agrees with the ambient one.