Tops of indecomposable projective modules

Let P be a projective module over a ring R, and let I be a nilpotent ideal. Then P is indecomposable exactly when P / IP is.

Over a semiprimary ring with Jacobson radical J, the top of P is P / JP. A projective module is indecomposable exactly when its top is simple. For an indecomposable projective module P, the submodule JP is maximal and is the kernel of every surjection onto a simple module, and every such surjection is a projective cover.

Main definitions

• TauCeti.IsIndecomposableModule.quotientJacobsonEquivOfSurjective: the equivalence between the top of an indecomposable projective module and any simple module it maps onto.

Main results

• TauCeti.isIndecomposableModule_quotient_smul_top_iff: for a nilpotent ideal I, a projective module P is indecomposable exactly when P / IP is; the reflecting direction TauCeti.IsIndecomposableModule.of_quotient_smul_top holds for every module.
• TauCeti.isIndecomposableModule_iff_isSimpleModule_quotient_jacobson_smul_top: over a semiprimary ring, a projective module is indecomposable exactly when its top is simple.
• TauCeti.IsIndecomposableModule.isCoatom_jacobson_smul_top: the radical of an indecomposable projective module is its unique maximal submodule, so it is the kernel of every surjection onto a simple module (TauCeti.ker_eq_jacobson_smul_top_of_surjective).
• TauCeti.IsIndecomposableModule.isProjectiveCover_of_surjective: such a surjection is a projective cover.

References

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

theorem TauCeti.IsIndecomposableModule.of_quotient_smul_top {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] {I : Ideal R} (hI : IsNilpotent I) (h : IsIndecomposableModule R (P ⧸ I • ⊤)) : IsIndecomposableModule R P

Indecomposability reflects from the top. If I is nilpotent and P / IP is indecomposable, then so is P. This holds for every module P, projective or not.

theorem TauCeti.isIndecomposableModule_quotient_smul_top_iff {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] [Module.Projective R P] {I : Ideal R} (hI : IsNilpotent I) : IsIndecomposableModule R (P ⧸ I • ⊤) ↔ IsIndecomposableModule R P

Indecomposability of a projective module is read off its top. If I is nilpotent, a projective module P is indecomposable exactly when P / IP is.

theorem TauCeti.isIndecomposableModule_iff_isSimpleModule_quotient_jacobson_smul_top {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] [Module.Projective R P] [IsSemiprimaryRing R] : IsIndecomposableModule R P ↔ IsSimpleModule R (P ⧸ Ring.jacobson R • ⊤)

A projective module is indecomposable exactly when its top is simple. Here R is semiprimary with Jacobson radical J, and the top of P is P / JP.

theorem TauCeti.IsIndecomposableModule.isCoatom_jacobson_smul_top {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] [Module.Projective R P] [IsSemiprimaryRing R] (h : IsIndecomposableModule R P) : IsCoatom (Ring.jacobson R • ⊤)

The radical of an indecomposable projective module over a semiprimary ring is a maximal submodule.

theorem TauCeti.IsIndecomposableModule.isProjectiveCover_of_surjective {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] [Module.Projective R P] [IsSemiprimaryRing R] (h : IsIndecomposableModule R P) (M : Type w) [AddCommGroup M] [Module R M] [IsSimpleModule R M] (f : P →ₗ[R] M) (hf : Function.Surjective ⇑f) : IsProjectiveCover f

An indecomposable projective module is the projective cover of each of its simple quotients. Over a semiprimary ring, any surjection from an indecomposable projective module onto a simple module is a projective cover.

noncomputable def TauCeti.IsIndecomposableModule.quotientJacobsonEquivOfSurjective {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] [Module.Projective R P] [IsSemiprimaryRing R] (h : IsIndecomposableModule R P) (M : Type w) [AddCommGroup M] [Module R M] [IsSimpleModule R M] (f : P →ₗ[R] M) (hf : Function.Surjective ⇑f) : (P ⧸ Ring.jacobson R • ⊤) ≃ₗ[R] M

A surjection from an indecomposable projective module P onto a simple module induces the canonical equivalence from the simple top of P to that module.

Equations

• h.quotientJacobsonEquivOfSurjective M f hf = ((Ring.jacobson R • ⊤).quotEquivOfEq f.ker ⋯).trans (f.quotKerEquivOfSurjective hf)

@[simp]

theorem TauCeti.IsIndecomposableModule.quotientJacobsonEquivOfSurjective_mk {R : Type u} [Ring R] {P : Type v} [AddCommGroup P] [Module R P] [Module.Projective R P] [IsSemiprimaryRing R] (h : IsIndecomposableModule R P) (M : Type w) [AddCommGroup M] [Module R M] [IsSimpleModule R M] (f : P →ₗ[R] M) (hf : Function.Surjective ⇑f) (x : P) : (h.quotientJacobsonEquivOfSurjective M f hf) (Submodule.Quotient.mk x) = f x