Minimal projective covers of finite-dimensional modules

An endomorphism of a finite-support pointwise finite-dimensional module has a uniform stable image. The induced endomorphism of that image is invertible, so a noninvertible endomorphism of a projective object exhibits a strictly smaller projective retract. Minimizing total dimension among projective presentations therefore produces a right-minimal projective epimorphism.

theorem MagnitudeConjecture.CoveringHom.minimalProjectivePresentation_nonempty_of_enoughProjectives {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.EnoughProjectives (FiniteDimensionalModuleCategory k)] (M : FiniteDimensionalModuleCategory k) : Nonempty (MinimalProjectivePresentation M)

Enough projectives imply existence of minimal projective presentations in the finite-support pointwise finite-dimensional module category.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_minimalProjectivePresentation_nonempty {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (M : FiniteDimensionalModuleCategory k) : Nonempty (MinimalProjectivePresentation M)

Finite representables therefore supply minimal projective presentations for every finite module.

theorem MagnitudeConjecture.CoveringHom.finiteDimensionalModule_twoStepMinimalProjectivePresentation_nonempty {k : Type uK} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (M : FiniteDimensionalModuleCategory k) : Nonempty (TwoStepMinimalProjectivePresentation M)

Finite representables supply two-step minimal projective presentations for every finite module.