The intrinsic linear space of irreducible morphisms

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

The intrinsic categorical radical as a linear subspace.

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

The square of the intrinsic radical as a linear subspace.

def MagnitudeConjecture.CategoricalIrreducible.denominator (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) : Submodule k ↥(radical k X Y)

The radical-square denominator inside the radical numerator.

@[reducible, inline]

abbrev MagnitudeConjecture.CategoricalIrreducible.Space (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) : Type w

The standard quotient rad(X,Y) / rad²(X,Y) in a linear category.

theorem MagnitudeConjecture.CategoricalIrreducible.finrank_le_hom (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (X Y : C) [FiniteDimensional k (X ⟶ Y)] : Module.finrank k (Space k X Y) ≤ Module.finrank k (X ⟶ Y)

The irreducible quotient cannot have dimension larger than its Hom space.