Finite minimal projective presentations

Over a semiprimary Noetherian ring, a finitely generated module has a minimal presentation by finitely generated projectives. This file packages that presentation using FiniteProjectivePresentation, retaining the minimality proof needed to form an Auslander–Reiten translate independent of choices up to actual isomorphism.

The ring need only be small in the universe of the module. The construction cuts projective covers out of finite projective surjections, so both covering modules stay in that universe.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Sections I.2 and IV.1.

theorem TauCeti.FiniteProjectivePresentation.exists_isMinimal {A : Type u} [Ring A] [IsSemiprimaryRing A] [IsNoetherianRing A] {M : ModuleCat A} [Module.Finite A ↑M] [Small.{v, u} A] : ∃ (P : FiniteProjectivePresentation M), IsMinimalProjectivePresentation P.p P.π

A finitely generated module over a semiprimary Noetherian ring has a finite minimal projective presentation in its own universe.

noncomputable def TauCeti.FiniteProjectivePresentation.minimal {A : Type u} [Ring A] [IsSemiprimaryRing A] [IsNoetherianRing A] {M : ModuleCat A} [Module.Finite A ↑M] [Small.{v, u} A] : FiniteProjectivePresentation M

A chosen finite minimal projective presentation. Its minimality is recorded by isMinimal_minimal; constructions using it should provide independence of this choice.

Equations

• TauCeti.FiniteProjectivePresentation.minimal = ⋯.choose

theorem TauCeti.FiniteProjectivePresentation.isMinimal_minimal {A : Type u} [Ring A] [IsSemiprimaryRing A] [IsNoetherianRing A] {M : ModuleCat A} [Module.Finite A ↑M] [Small.{v, u} A] : IsMinimalProjectivePresentation minimal.p minimal.π

The chosen finite projective presentation is minimal.