Finite decomposition codes under a Hom-dimension bound

@[reducible, inline]

abbrev MagnitudeConjecture.FiniteKernel.DecompositionCode (ι : Type) (D : ℕ) : Type

A bounded ordered list of labels from a finite family.

noncomputable def MagnitudeConjecture.FiniteKernel.codeObject {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] {ι : Type} (F : ι → C) {D : ℕ} (c : DecompositionCode ι D) : C

The biproduct specified by a decomposition code.

theorem MagnitudeConjecture.FiniteKernel.exists_bounded_decomposition {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] {ι : Type} [Fintype ι] (F : ι → C) (G : C) [∀ (X : C), FiniteDimensional k (G ⟶ X)] (hG : ∀ (i : ι), 1 ≤ Module.finrank k (G ⟶ F i)) (hdec : ∀ (X : C), ∃ (n : ℕ) (label : Fin n → ι), Nonempty (X ≅ ⨁ fun (j : Fin n) => F (label j))) (X : C) (D : ℕ) (hX : Module.finrank k (G ⟶ X) ≤ D) : ∃ (c : DecompositionCode ι D), Nonempty (X ≅ codeObject F c)

If G sees every family member, its Hom dimension bounds the number of summands and hence gives a finite code for every bounded object.

theorem MagnitudeConjecture.FiniteKernel.finrank_hom_le_of_mono {k : Type u} [Field k] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Limits.HasFiniteBiproducts C] (G : C) {X Z : C} (f : X ⟶ Z) [CategoryTheory.Mono f] [FiniteDimensional k (G ⟶ Z)] : Module.finrank k (G ⟶ X) ≤ Module.finrank k (G ⟶ Z)

A monomorphism bounds the Hom dimension of its source by that of its target.