Biserial representables from pointwise thinness

This file packages the variance-neutral finite-category step in the frozen manuscript. Pointwise thinness of every indecomposable finite module is transported to canonical idempotent-coordinate thinness for a small category algebra; the direct biserial induction then applies to each representable.

theorem MagnitudeConjecture.CoveringHom.finiteCovariantRepresentable_isBiserialObject_of_pointwiseThin {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hthin : ∀ (M : FiniteDimensionalModuleCategory k), CategoryTheory.Indecomposable M → IsPointwiseThin M.obj.obj) (X : C) : IsBiserialObject ((finiteDimensionalLinearCoyonedaFunctor hP).obj (Opposite.op X))

On a finite linear category with local endomorphism rings, pointwise thinness of all indecomposable finite modules makes every covariant representable intrinsically biserial.