Irreducible quotient spaces across an incoming-closed full subcategory

def MagnitudeConjecture.CategoricalIrreducible.radicalFullSubcategoryEquiv (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (P : CategoryTheory.ObjectProperty C) (X Y : P.FullSubcategory) : ↥(radical k X.obj Y.obj) ≃ₗ[k] ↥(radical k X Y)

Fullness identifies the intrinsic radical numerator with the ambient one.

theorem MagnitudeConjecture.CategoricalIrreducible.denominator_map_fullSubcategory (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k 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) : Submodule.map (↑(radicalFullSubcategoryEquiv k P X Y)) (denominator k X.obj Y.obj) = denominator k X Y

The numerator equivalence carries the intrinsic radical-square denominator onto the full-subcategory denominator at an incoming-closed target.

def MagnitudeConjecture.CategoricalIrreducible.spaceFullSubcategoryEquiv (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k 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) : Space k X.obj Y.obj ≃ₗ[k] Space k X Y

Interior restriction identifies the actual linear irreducible quotient spaces, not just the existence of irreducible maps.