Minimal finite projective presentations

Ringel's construction of the Auslander--Reiten translate starts from a minimal projective presentation. This file supplies the first step: over a finite-dimensional algebra, every finitely generated module admits a right-minimal epimorphism from a finitely generated projective module.

The proof starts with a finite free epimorphism and minimizes the scalar dimension of its projective source. If an endomorphism fixing such an epimorphism were not invertible, Fitting decomposition would replace its source by a proper projective stable image, contradicting minimality.

theorem MagnitudeConjecture.minimalProjectivePresentation_nonempty {R : Type u} [Ring R] [IsNoetherianRing R] (k : Type u) [Field k] [Algebra k R] [FiniteDimensional k R] (X : FGModuleCat R) : Nonempty (MinimalProjectivePresentation X)

Every finitely generated module over a finite-dimensional algebra has a minimal finite projective presentation.

theorem MagnitudeConjecture.twoStepMinimalProjectivePresentation_nonempty {R : Type u} [Ring R] [IsNoetherianRing R] (k : Type u) [Field k] [Algebra k R] [FiniteDimensional k R] (X : FGModuleCat R) : Nonempty (TwoStepMinimalProjectivePresentation X)

Two-step minimal projective presentations exist over every finite-dimensional algebra.

theorem MagnitudeConjecture.TwoStepMinimalProjectivePresentation.hasProjectiveDimensionLE_one_of_mono_differential {R : Type u} [Ring R] [IsNoetherianRing R] {X : FGModuleCat R} (P : TwoStepMinimalProjectivePresentation X) (hmono : CategoryTheory.Mono P.differential) : CategoryTheory.HasProjectiveDimensionLE X 1

If the first differential in a two-step minimal presentation is monic, then the presented module has projective dimension at most one.