Minimality of the finite-representable Nakayama kernel

Minimality of the first projective syzygy presentation rules out nonzero injective retracts of the kernel of its Nakayama differential. This is the categorical finite-functor analogue of the classical transpose argument.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.finiteRepresentableNakayamaMapLinearEquiv_differential {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) : (finiteRepresentableNakayamaMapLinearEquiv hP hI P.syzygyPresentation.matrixObject P.augmentation.matrixObject) P.toTwoStepFiniteRepresentablePresentation.differential = nakayamaDifferential hI P

The abstract finite-projective Nakayama equivalence sends the actual first differential to the displayed Nakayama differential.

theorem MagnitudeConjecture.CoveringHom.TwoStepMinimalFiniteRepresentablePresentation.nakayamaKernel_isZero_of_injective_retract {k : Type v} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] {hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)} (hI : ∀ (X : C), IsFiniteDimensionalModule k (dualLinearYonedaLinearModule X)) {M : FiniteDimensionalModuleCategory k} (P : TwoStepMinimalFiniteRepresentablePresentation hP M) {I : FiniteDimensionalModuleCategory k} [CategoryTheory.Injective I] (r : CategoryTheory.Retract I (nakayamaKernel hI P)) : CategoryTheory.Limits.IsZero I

Minimality of the projective presentation rules out nonzero injective retracts of its Nakayama kernel.