Bounding total incoming irreducible dimension

theorem MagnitudeConjecture.CategoricalIrreducible.finrank_eq_zero_of_hom_eq_zero (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) : Module.finrank k (Space k X Y) = 0

A zero Hom space has zero intrinsic irreducible dimension.

theorem MagnitudeConjecture.CategoricalIrreducible.sum_finrank_le_incoming_card_mul (k : Type u) [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {ι : Type z} [Fintype ι] (F : ι → C) (Y : C) (D : ℕ) (hD : ∀ (i : ι), Module.finrank k (Space k (F i) Y) ≤ D) : ∑ i : ι, Module.finrank k (Space k (F i) Y) ≤ Nat.card { i : ι // ∃ (f : F i ⟶ Y), f ≠ 0 } * D

A uniform quotient bound only needs to be counted over sources with a nonzero incoming morphism.