No-reverse-map factorizations lie in the radical square #
theorem
MagnitudeConjecture.CategoryTheory.noBackwardFactorizations_le_radicalSquare
{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)
:
Absence of reverse maps forces both factors into the categorical radical.