Uniserial syzygies from coherent defect duality

This file packages the source-shaped implication in Auslander--Reiten, Proposition 1.3(a)(iii). Coherent duality carries a uniserial projective-stable contravariant representable to a uniserial degree-one Ext functor. Its canonical quotient makes the projective-stable covariant representable of the syzygy uniserial, and Proposition 1.1(a) then makes the syzygy itself uniserial when it is indecomposable and nonprojective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectivePresentation_kernel_isUniserialModule_of_stableContravariant {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt (FinitelyGeneratedCategory A)] {X : FinitelyGeneratedCategory A} (P : MinimalProjectivePresentation X) (hkernel : CategoryTheory.Indecomposable (CategoryTheory.Limits.kernel P.f)) (hkernelNonprojective : ¬CategoryTheory.Projective (CategoryTheory.Limits.kernel P.f)) (hstable : IsUniserialObject (S.finiteProjectiveStableContravariantRepresentable X)) : IsUniserialModule Aᵐᵒᵖ ↑(CategoryTheory.Limits.kernel P.f).obj

Auslander--Reiten Proposition 1.3(a)(iii), in the projective-presentation interface needed at a projective radical boundary.