Projectives over a self-injective ring

This file relates module-theoretic self-injectivity to projective and injective objects in the category FGModuleCat R of finitely generated modules.

Categorical projectivity of a finitely generated module implies module-theoretic projectivity (FGModuleCat.moduleProjective_of_projective). Consequently, over a ring whose regular left module is injective, every projective object of FGModuleCat R is injective.

These results supply one direction of the projective--injective identification for the Frobenius exact category of finite-dimensional modules over a self-injective finite-dimensional algebra.

Main results

• FGModuleCat.injective_of_projective_of_moduleInjective_self: over a self-injective ring, every projective object of FGModuleCat R is injective.

References

• T. Y. Lam, Lectures on Modules and Rings, Sections 3 and 16.
• D. Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.

theorem FGModuleCat.injective_of_projective_of_moduleInjective_self {R : Type u} [Ring R] [Small.{v, u} R] (hR : Module.Injective R R) (X : FGModuleCat R) [CategoryTheory.Projective X] : CategoryTheory.Injective X

Over a self-injective ring, every projective object among the finitely generated modules is injective. The smallness hypothesis holds automatically when the modules live in a universe containing R.