Existence of projective covers over a semiprimary ring

TauCeti/Algebra/Module/ProjectiveCover/Basic.lean develops the projective cover of a module as a given datum: it is unique, and it receives every projective presentation, but nothing there produces one. This file supplies the existence theorem. Over a semiprimary ring — Mathlib's IsSemiprimaryRing, a ring whose Jacobson radical is nilpotent and whose radical quotient is semisimple, as a finite-dimensional algebra over a field is — every module has a projective cover (TauCeti.exists_isProjectiveCover), with no finiteness hypothesis on the module.

Some hypothesis on the ring is genuinely needed: ℤ ⧸ 2ℤ has no projective cover as a ℤ-module, although it has finite length.

The construction

Write J for the radical and M ↦ M ⧸ J • M for passage to the radical quotient. Fix a free module N with a surjection p : N ↠ M — the free module on the underlying set of M will do — and let q : N ⧸ J • N ↠ M ⧸ J • M be the induced surjection. The cover is cut out of N by an idempotent, in three steps.

• The radical quotient is semisimple. N ⧸ J • N is a module over R ⧸ J, which is a semisimple ring, so it is a semisimple R ⧸ J-module and hence a semisimple R-module (TauCeti.isSemisimpleModule_quotient_jacobson_smul_top). Therefore ker q has a complement C, and the projection onto C along ker q is an idempotent ē of End (N ⧸ J • N) with range ē = C.
• The idempotent lifts. Reduction of endomorphisms modulo J • N is a ring homomorphism Ideal.endMapQ J N : End N →+* End (N ⧸ J • N). It is surjective because N is projective (Ideal.endMapQ_surjective), and every element of its kernel is nilpotent because J is (Ideal.isNilpotent_of_mem_ker_endMapQ): a map with image inside J • N has k-th power with image inside J ^ k • N. Mathlib's exists_isIdempotentElem_eq_of_ker_isNilpotent therefore lifts ē to an idempotent e of End N.
• The cover is the image of the lift. P = range e is a direct summand of the free module N, so it is projective, and π = p|_P is the cover. It is onto because its image spans M modulo J • M — that is what ker ē = ker q says — and J • M is superfluous (TauCeti.isSuperfluous_smul_top_of_isNilpotent, Nakayama for a nilpotent ideal). Its kernel is superfluous because an element of it reduces into C ⊓ ker q = ⊥, hence lies in J • N, hence, being fixed by e, lies in J • P.

Nilpotence of J is used twice, and differently: once to make J • M superfluous in an arbitrary module — which is what removes every finiteness hypothesis, and is why a semiprimary ring covers all modules and not only the finitely generated ones a semiperfect ring covers — and once to make the kernel of the reduction map nil, which is what lets the idempotent lift.

Semiperfectness itself is TauCeti.IsSemiperfectRing, in TauCeti/RingTheory/Jacobson/Semiperfect.lean: the second use of nilpotence above, made at the level of the ring rather than of End N, is exactly the statement that a semiprimary ring is semiperfect.

Main statements

• TauCeti.exists_isProjectiveCover_comp_subtype: over a semiprimary ring, a surjection onto M from a projective module restricts to a projective cover of M on a submodule of its source.
• TauCeti.exists_isProjectiveCover: every module over a semiprimary ring has a projective cover, carried by a submodule of the free module on its underlying set.
• TauCeti.exists_isProjectiveCover_of_finite: the same statement for a module over a ring that is finite over an Artinian ring, such as a finite-dimensional algebra over a field; such a ring is semiprimary.

References

See T. Y. Lam, A First Course in Noncommutative Rings, §24 (semiperfect and semiprimary rings, idempotent lifting, and projective covers), and I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.5.

theorem TauCeti.exists_isProjectiveCover_comp_subtype {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] {N : Type w} [AddCommGroup N] [Module R N] [Module.Projective R N] (p : N →ₗ[R] M) (hp : Function.Surjective ⇑p) : ∃ (P : Submodule R N), IsProjectiveCover (p ∘ₗ P.subtype)

A projective cover is cut out of any projective presentation by an idempotent. Over a semiprimary ring, a surjection p : N ↠ M from a projective module restricts to a projective cover of M on a suitable submodule P of N; that cover property is all the statement records about P. See the module docstring for how P is produced.

theorem TauCeti.exists_isProjectiveCover (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] : ∃ (P : Submodule R (M →₀ R)), IsProjectiveCover (Finsupp.linearCombination R id ∘ₗ P.subtype)

Every module over a semiprimary ring has a projective cover.

The covering module is a submodule of the free module on the underlying set of M. No finiteness is assumed of M: a semiprimary ring is left perfect, so it covers every module, not only the finitely generated ones.

theorem TauCeti.exists_isProjectiveCover_of_finite (K : Type w) [Ring K] [IsArtinianRing K] (A : Type u) [Ring A] [Module K A] [IsScalarTower K A A] [Module.Finite K A] (V : Type v) [AddCommGroup V] [Module A V] : ∃ (P : Submodule A (V →₀ A)), IsProjectiveCover (Finsupp.linearCombination A id ∘ₗ P.subtype)

Every module over a ring finite over an Artinian ring has a projective cover. Here K is an Artinian ring acting on A compatibly with its multiplication, with A finite as a K-module; for instance, A may be a finite-dimensional algebra over a field. No finiteness is required of the module.