Essential simple socles of finite functors #
A finite-dimensional functor has a simple subfunctor whenever it is nonzero. Consequently a simple subfunctor through which every simple subfunctor factors is essential. This is the finite-length bridge used in the Auslander--Reiten Corollary 3.8 argument.
theorem
MagnitudeConjecture.CoveringHom.finiteDimensionalModule_isEssentialMono_of_simple_factors
{k : Type v}
[Field k]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Linear k C]
{L F : FiniteDimensionalModuleCategory k}
[CategoryTheory.Simple L]
(l : L ⟶ F)
[CategoryTheory.Mono l]
(hfactor :
∀ {T : FiniteDimensionalModuleCategory k} [CategoryTheory.Simple T] (t : T ⟶ F) [CategoryTheory.Mono t],
t ≠ 0 → ∃ (a : T ⟶ L), CategoryTheory.CategoryStruct.comp a l = t)
:
A simple subfunctor of a finite functor is essential when every simple subfunctor factors through it.