Covariant stable representables detect uniserial modules

This file completes Auslander--Reiten, Proposition 1.1(a), in the finite right-module skeleton: a nonzero indecomposable nonprojective module whose projective-stable covariant representable is uniserial is itself uniserial.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.isUniserialModule_of_projectiveStableCovariantRepresentable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FinitelyGeneratedCategory A} (hX : CategoryTheory.Indecomposable X) (hXnonprojective : ¬CategoryTheory.Projective X) (hstable : IsUniserialObject (S.finiteProjectiveStableCovariantRepresentable X)) : IsUniserialModule Aᵐᵒᵖ ↑X

Auslander--Reiten Proposition 1.1(a), in the exact finite-skeleton interface used by the magnitude campaign.