Irreducible morphisms from finite indecomposable cores

A finite control window for indecomposable objects cannot literally contain every decomposable intermediate object of a factorization. This file gives the precise replacement. Decompose an arbitrary intermediate object and retain only those summands on which both incident coordinate maps are nonzero. The resulting finite biproduct is a factorization core: deleting the other summands does not change the composite.

theorem MagnitudeConjecture.indecomposable_of_faithful_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Faithful] (X : C) (hX : CategoryTheory.Indecomposable (F.obj X)) : CategoryTheory.Indecomposable X

An additive faithful functor reflects indecomposability. Fullness is not needed: faithfulness already reflects zero objects, and additivity preserves binary biproduct decompositions.

def MagnitudeConjecture.IsLocallyIndecomposableBifactorClosed {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (F : CategoryTheory.Functor C D) (X Y : C) : Prop

Every indecomposable object which supports nonzero maps between the two fixed endpoints belongs to the essential image of F.

theorem MagnitudeConjecture.irreducible_map_of_full_faithful_of_finiteIndecomposableCore {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] [F.Faithful] (decomposition : ∀ (M : D), Nonempty (CategoryTheory.FiniteIndecomposableDecomposition M)) {X Y : C} {f : X ⟶ Y} (hf : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) (hclosed : IsLocallyIndecomposableBifactorClosed F X Y) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (F.map f)

A fully faithful additive functor preserves an irreducible morphism when the target category has finite indecomposable decompositions and the indecomposable objects that interact nontrivially with both endpoints lie in the local essential image.

theorem MagnitudeConjecture.isIrreducibleMorphism_map_iff_of_finiteIndecomposableCore {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] [F.Faithful] (decomposition : ∀ (M : D), Nonempty (CategoryTheory.FiniteIndecomposableDecomposition M)) {X Y : C} {f : X ⟶ Y} (hclosed : IsLocallyIndecomposableBifactorClosed F X Y) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (F.map f) ↔ QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f

Under finite indecomposable-core closure, full faithfulness identifies irreducibility on the nose.