Expanding a factorization through its nonzero incoming summands

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.incomingComponent {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) (b : M ⟶ Y) (j : Fin d.n) : d.summand j ⟶ Y

The component from a summand to the target.

@[reducible, inline]

abbrev MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.IncomingIndex {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) (b : M ⟶ Y) : Type

The summands that actually contribute to a map to the target.

noncomputable def MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.outgoingComponent {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) (a : X ⟶ M) (j : Fin d.n) : X ⟶ d.summand j

The source component in the same displayed decomposition.

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.comp_eq_sum_incoming {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] {X M Y : C} (d : FiniteIndecomposableDecomposition M) (a : X ⟶ M) (b : M ⟶ Y) : CategoryTheory.CategoryStruct.comp a b = ∑ j : d.IncomingIndex b, CategoryTheory.CategoryStruct.comp (d.outgoingComponent a ↑j) (d.incomingComponent b ↑j)

A composite is the sum of its components through the summands whose maps to the target are nonzero.

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.incoming_summand_property {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) (P : C → Prop) (hP : ∀ (Z : C), CategoryTheory.Indecomposable Z → ∀ (f : Z ⟶ Y), f ≠ 0 → P Z) (b : M ⟶ Y) (j : d.IncomingIndex b) : P (d.summand ↑j)

Any property shared by all indecomposables mapping nontrivially to Y holds for each intermediate object in the reduced sum.

theorem MagnitudeConjecture.CategoryTheory.FiniteIndecomposableDecomposition.exists_factorization_decomposition {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] {X M Y : C} (P : C → Prop) (hP : ∀ (Z : C), CategoryTheory.Indecomposable Z → ∀ (f : Z ⟶ Y), f ≠ 0 → P Z) (hd : Nonempty (FiniteIndecomposableDecomposition M)) (a : X ⟶ M) (b : M ⟶ Y) : ∃ (d : FiniteIndecomposableDecomposition M), (∀ (q : d.IncomingIndex b), P (d.summand ↑q)) ∧ CategoryTheory.CategoryStruct.comp a b = ∑ q : d.IncomingIndex b, CategoryTheory.CategoryStruct.comp (d.outgoingComponent a ↑q) (d.incomingComponent b ↑q)

A displayed decomposition supplies a reduced factorization whose intermediates all have the incoming-object property.