Projective modules are determined by a radical quotient

Projective modules over a ring whose submodule lattices are coatomic (for instance, finitely generated projective modules) are determined by their reductions modulo an ideal in the Jacobson radical. Indeed, the quotient map from a projective module to its reduction is a projective cover, and uniqueness of projective covers identifies the two projective modules.

This is the algebraic lifting step used when integral projective modules are compared through a residue-field calculation. The result applies to noncommutative rings and does not require the ideal itself to be the whole Jacobson radical.

When the radical quotient R ⧸ J of the ring is finite, as for a finite ring or for the group algebra of a finite group over ℤ_p, the radical quotient P ⧸ J • P of a finitely generated module is semisimple and is determined by its composition factors. These are counted by the numbers of maps from P to the simple modules, #Hom(P, S) = #End(S) ^ [P ⧸ J • P : S], so a finitely generated projective module is determined by the numbers #Hom(P, S). This is the form in which a computation of such counts, for instance through characters, identifies a projective module.

Main results

• Ideal.nonempty_linearEquiv_of_quotient_smul_top: two projective modules with coatomic submodule lattices (e.g. finitely generated ones) and isomorphic quotients by an ideal in the Jacobson radical are isomorphic.
• TauCeti.finite_quotient_jacobson_smul_top: over a ring with finite radical quotient, the radical quotient of a finitely generated module is finite.
• TauCeti.nonempty_linearEquiv_of_projective_of_natCard_linearMap_eq: over a ring with finite radical quotient, two finitely generated projective modules with equally many maps to every simple module are isomorphic.

References

See T. Y. Lam, A First Course in Noncommutative Rings, Section 24, for projective covers over semiperfect rings and their uniqueness.

theorem Ideal.nonempty_linearEquiv_of_quotient_smul_top {R : Type u} [Ring R] (I : Ideal R) (M : Type v) (N : Type w) [AddCommGroup M] [Module R M] [IsCoatomic (Submodule R M)] [Module.Projective R M] [AddCommGroup N] [Module R N] [IsCoatomic (Submodule R N)] [Module.Projective R N] (hI : I ≤ Ring.jacobson R) (h : Nonempty ((M ⧸ I • ⊤) ≃ₗ[R] N ⧸ I • ⊤)) : Nonempty (M ≃ₗ[R] N)

Projectives are determined by a radical quotient. If I lies in the Jacobson radical of R, then an R-linear equivalence between M / IM and N / IN implies that the projective modules M and N are R-linearly equivalent, provided their submodule lattices are coatomic (as is the case for finitely generated modules).

Only existence of the resulting equivalence is asserted: both quotient maps are projective covers of the same reduced module, so uniqueness of projective covers identifies their sources.

theorem TauCeti.finite_quotient_jacobson_smul_top {R : Type u} [Ring R] [Finite (R ⧸ Ring.jacobson R)] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] : Finite (M ⧸ Ring.jacobson R • ⊤)

The radical quotient of a finitely generated module is finite over a ring R whose radical quotient R ⧸ J is finite. It is a finitely generated module over the semisimple ring R ⧸ J, hence a finite product of simple modules, and simple modules are quotients of R ⧸ J.

theorem TauCeti.nonempty_linearEquiv_of_projective_of_natCard_linearMap_eq {R : Type u} [Ring R] [Finite (R ⧸ Ring.jacobson R)] (P : Type v) (Q : Type w) [AddCommGroup P] [Module R P] [Module.Finite R P] [Module.Projective R P] [AddCommGroup Q] [Module R Q] [Module.Finite R Q] [Module.Projective R Q] (h : ∀ (S : Type u) [inst : AddCommGroup S] [inst_1 : Module R S] [IsSimpleModule R S], Nat.card (P →ₗ[R] S) = Nat.card (Q →ₗ[R] S)) : Nonempty (P ≃ₗ[R] Q)

Projectives are determined by their maps to simple modules, over a ring R whose radical quotient R ⧸ J is finite (a finite ring, or the group algebra of a finite group over ℤ_p). Two finitely generated projective R-modules P and Q are isomorphic as soon as, for every simple module S, there are as many R-linear maps P → S as Q → S.

The number of maps P → S is #End_R(S) ^ [P ⧸ J • P : S], and End_R(S) is a finite ring with at least two elements, so the hypothesis says that the semisimple radical quotients of P and Q have the same composition factors. They are then isomorphic, and projective covers lift the isomorphism to P ≃ Q.