Primitive idempotents and simple heads

In a left Artinian ring R, an idempotent e is primitive exactly when the head of its left ideal Re is simple. The head is the quotient Re / J Re, where J is the Jacobson radical. Every surjection from Re onto a nonzero module is then a projective cover. If the target is semisimple, it is necessarily simple. Given a complete primitive orthogonal family, these ideals supply projective covers of every simple module. Since an indecomposable finitely generated projective module is the projective cover of its simple head, every such module is isomorphic to one of these ideals.

This connects the decomposition of the regular module by primitive idempotents to the simple modules. It uses the general simple-head theorem for indecomposable projectives and the existing occurrence theorem for simple quotients of a complete orthogonal family.

References

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

theorem TauCeti.isPrimitiveIdempotent_of_isSimpleModule_quotient_jacobson_smul_top {R : Type u_1} [Ring R] {e : R} (he : IsIdempotentElem e) [IsSimpleModule R (↥(Ideal.span {e}) ⧸ Ring.jacobson R • ⊤)] : IsPrimitiveIdempotent e

If the head of the left ideal of an idempotent is simple, the idempotent is primitive. This implication does not need an Artinian hypothesis.

theorem TauCeti.IsPrimitiveIdempotent.isSimpleModule_quotient_jacobson_smul_top {R : Type u_1} [Ring R] {e : R} [IsArtinianRing R] (he : IsPrimitiveIdempotent e) : IsSimpleModule R (↥(Ideal.span {e}) ⧸ Ring.jacobson R • ⊤)

The head Re / J Re of the left ideal of a primitive idempotent in a left Artinian ring is simple.

theorem TauCeti.IsPrimitiveIdempotent.isProjectiveCover_of_surjective {R : Type u_1} [Ring R] {e : R} [IsArtinianRing R] (he : IsPrimitiveIdempotent e) {S : Type u_2} [AddCommGroup S] [Module R S] [Nontrivial S] {f : ↥(Ideal.span {e}) →ₗ[R] S} (hf : Function.Surjective ⇑f) : IsProjectiveCover f

Every surjection from the left ideal of a primitive idempotent onto a nonzero module is a projective cover.

theorem TauCeti.IsPrimitiveIdempotent.isSimpleModule_of_surjective {R : Type u_1} [Ring R] {e : R} [IsArtinianRing R] (he : IsPrimitiveIdempotent e) {S : Type u_2} [AddCommGroup S] [Module R S] [IsSemisimpleModule R S] [Nontrivial S] {f : ↥(Ideal.span {e}) →ₗ[R] S} (hf : Function.Surjective ⇑f) : IsSimpleModule R S

Every nonzero semisimple quotient of the left ideal of a primitive idempotent in a left Artinian ring is simple.

theorem CompleteOrthogonalIdempotents.exists_isProjectiveCover_of_isSimpleModule {R : Type u_1} [Ring R] [IsArtinianRing R] {ι : Type u_2} [Fintype ι] {e : ι → R} (he : CompleteOrthogonalIdempotents e) (hprim : ∀ (i : ι), TauCeti.IsPrimitiveIdempotent (e i)) (S : Type u_3) [AddCommGroup S] [Module R S] [IsSimpleModule R S] : ∃ (i : ι) (f : ↥(Ideal.span {e i}) →ₗ[R] S), TauCeti.IsProjectiveCover f

A complete family of primitive orthogonal idempotents supplies projective covers of every simple module by its principal left ideals.

theorem CompleteOrthogonalIdempotents.exists_nonempty_linearEquiv_span_singleton {R : Type u_1} [Ring R] [IsArtinianRing R] {ι : Type u_2} [Fintype ι] {e : ι → R} (he : CompleteOrthogonalIdempotents e) (hprim : ∀ (i : ι), TauCeti.IsPrimitiveIdempotent (e i)) (P : Type u_3) [AddCommGroup P] [Module R P] [Module.Finite R P] [Module.Projective R P] (hP : TauCeti.IsIndecomposableModule R P) : ∃ (i : ι), Nonempty (P ≃ₗ[R] ↥(Ideal.span {e i}))

The ideals of a complete primitive orthogonal family exhaust the indecomposable finitely generated projectives.