Quotients when every nonzero map is irreducible

theorem MagnitudeConjecture.CategoricalIrreducible.radical_eq_top_of_no_reverse (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) (h : ∀ (g : Y ⟶ X), g = 0) : radical k X Y = ⊤

No reverse maps implies that every forward map is radical.

theorem MagnitudeConjecture.CategoricalIrreducible.radicalSquare_eq_bot_of_all_nonzero_irreducible (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) (hi : ∀ (f : X ⟶ Y), f ≠ 0 → QuotientSubmoduleEquidistribution.IsIrreducibleMorphism f) : radicalSquare k X Y = ⊥

A Hom space consisting of zero and irreducible maps has zero radical square.

def MagnitudeConjecture.CategoricalIrreducible.spaceEquivHom (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) (hr : radical k X Y = ⊤) (hs : radicalSquare k X Y = ⊥) : Space k X Y ≃ₗ[k] X ⟶ Y

If the radical is all of Hom and its square is zero, the intrinsic irreducible quotient is linearly equivalent to Hom itself.