A linear subspace of factorizations with no reverse maps

def MagnitudeConjecture.CategoryTheory.noBackwardFactorizations {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] (X Y : C) : Submodule k (X ⟶ Y)

Maps factoring through an object with no maps back to the source or from the target. Finite biproducts make these maps a linear subspace.

theorem MagnitudeConjecture.CategoryTheory.not_irreducible_of_noBackwardFactorization {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Limits.HasFiniteBiproducts C] {X Y : C} {f : X ⟶ Y} (hf : f ≠ 0) (h : f ∈ noBackwardFactorizations X Y) : ¬QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f

A nonzero map in this subspace has a factorization with neither factor split.