Vanishing when every nonzero morphism is invertible

theorem MagnitudeConjecture.CategoricalIrreducible.radical_eq_bot_of_nonzero_isIso (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) (h : ∀ (f : X ⟶ Y), f ≠ 0 → CategoryTheory.IsIso f) : radical k X Y = ⊥

A Hom space with only invertible nonzero morphisms has zero radical.

theorem MagnitudeConjecture.CategoricalIrreducible.finrank_eq_zero_of_radical_eq_bot (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) (h : radical k X Y = ⊥) : Module.finrank k (Space k X Y) = 0

A zero radical numerator has zero irreducible quotient dimension.