The finite-kernel dimension bound with explicit extension input #
theorem
MagnitudeConjecture.FiniteKernel.finrank_hom_le_one_of_finite_decompositions
{k : Type u}
[Field k]
[Infinite k]
{C : Type v}
[CategoryTheory.Category.{w, v} C]
[CategoryTheory.Abelian 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)))
(Z I : C)
[CategoryTheory.Injective I]
(hZ : ∀ (a : Z ⟶ Z), ∃ (c : k), a = c • CategoryTheory.CategoryStruct.id Z)
(hI : ∀ (a : I ⟶ I), ∃ (c : k), a = c • CategoryTheory.CategoryStruct.id I)
(hext :
∀ (f : Z ⟶ I),
f ≠ 0 →
∀ (h : CategoryTheory.Limits.kernel f ⟶ Z),
∃ (a : Z ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) a = h)
:
Module.finrank k (Z ⟶ I) ≤ 1
A finite additive classification bounds the possible kernel classes. If kernel maps extend to a scalar-endomorphism source and the target is injective with scalar endomorphisms, the Hom dimension is at most one.
theorem
MagnitudeConjecture.FiniteKernel.finrank_hom_le_one_of_finite_additive_family
{k : Type u}
[Field k]
[Infinite k]
{C : Type v}
[CategoryTheory.Category.{w, v} C]
[CategoryTheory.Abelian C]
[CategoryTheory.Linear k C]
[CategoryTheory.Limits.HasFiniteBiproducts C]
{ι : Type}
[Fintype ι]
[∀ (X Y : C), FiniteDimensional k (X ⟶ Y)]
(F : ι → C)
(hF : ∀ (i : ι), ¬CategoryTheory.Limits.IsZero (F i))
(hdec : ∀ (X : C), ∃ (n : ℕ) (label : Fin n → ι), Nonempty (X ≅ ⨁ fun (j : Fin n) => F (label j)))
(Z I : C)
[CategoryTheory.Injective I]
(hZ : ∀ (a : Z ⟶ Z), ∃ (c : k), a = c • CategoryTheory.CategoryStruct.id Z)
(hI : ∀ (a : I ⟶ I), ∃ (c : k), a = c • CategoryTheory.CategoryStruct.id I)
(hext :
∀ (f : Z ⟶ I),
f ≠ 0 →
∀ (h : CategoryTheory.Limits.kernel f ⟶ Z),
∃ (a : Z ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) a = h)
:
Module.finrank k (Z ⟶ I) ≤ 1
The sum of the finite family detects every nonzero summand, so a Hom-finite category with a finite additive classification satisfies the finite-kernel bound.