Simple heads of indecomposable projective modules

Over a ring with semisimple radical quotient, a projective module with local endomorphism ring and coatomic submodule lattice has simple head P / J P. In particular this holds for indecomposable projective modules of finite length. Every surjection from such a module onto a simple module has kernel J P and is a projective cover. Thus its simple quotient is unique up to isomorphism.

The locality argument uses Ideal.endMapQ: projectivity makes reduction of endomorphisms surjective, so the endomorphism ring of the head is local as well.

References

• T. Y. Lam, A First Course in Noncommutative Rings, 2nd ed., §§23–24.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, §I.4.

theorem TauCeti.isSimpleModule_quotient_jacobson_smul_top_of_isLocalRing_end {R : Type u_1} {P : Type u_2} [Ring R] [AddCommGroup P] [Module R P] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] [IsCoatomic (Submodule R P)] [Module.Projective R P] [IsLocalRing (Module.End R P)] : IsSimpleModule R (P ⧸ Ring.jacobson R • ⊤)

A projective module with local endomorphism ring and coatomic submodule lattice has simple head, provided the ring's radical quotient is semisimple.

theorem TauCeti.IsIndecomposableModule.isSimpleModule_quotient_jacobson_smul_top {R : Type u_1} {P : Type u_2} [Ring R] [AddCommGroup P] [Module R P] [IsSemisimpleRing (R ⧸ Ring.jacobson R)] [Module.Projective R P] (hP : IsIndecomposableModule R P) (hfin : IsFiniteLength R P) : IsSimpleModule R (P ⧸ Ring.jacobson R • ⊤)

An indecomposable projective module of finite length has simple head over any ring whose radical quotient is semisimple.

theorem TauCeti.ker_eq_jacobson_smul_top_of_surjective {R : Type u_1} {P : Type u_2} {S : Type u_3} [Ring R] [AddCommGroup P] [Module R P] [AddCommGroup S] [Module R S] [IsSimpleModule R (P ⧸ Ring.jacobson R • ⊤)] [IsSimpleModule R S] {f : P →ₗ[R] S} (hf : Function.Surjective ⇑f) : f.ker = Ring.jacobson R • ⊤

If a module has simple head, every surjection onto a simple module has kernel exactly J P. This identifies all its simple quotients with its head.

theorem TauCeti.isProjectiveCover_of_isSimpleModule_quotient_jacobson_smul_top {R : Type u_1} {P : Type u_2} {S : Type u_3} [Ring R] [AddCommGroup P] [Module R P] [AddCommGroup S] [Module R S] [IsCoatomic (Submodule R P)] [Module.Projective R P] [IsSimpleModule R (P ⧸ Ring.jacobson R • ⊤)] [IsSimpleModule R S] {f : P →ₗ[R] S} (hf : Function.Surjective ⇑f) : IsProjectiveCover f

A surjection from a projective module with simple head and coatomic submodule lattice onto a simple module is a projective cover.

theorem TauCeti.IsProjectiveCover.isIndecomposableModule {R : Type u_1} {P : Type u_2} {S : Type u_3} [Ring R] [AddCommGroup P] [Module R P] [AddCommGroup S] [Module R S] [IsSimpleModule R S] {f : P →ₗ[R] S} (hf : IsProjectiveCover f) : IsIndecomposableModule R P

A projective cover of a simple module is indecomposable. No finiteness or assumption on the radical of the ring is needed.