The socle of a module

The socle of a module is the supremum of its simple submodules. Mathlib already uses the submodule sSup {m | IsSimpleModule R m} as the object measuring how far a module is from being semisimple — IsSemisimpleModule.of_sSup_simples_eq_top and sSup_simples_eq_top_iff_isSemisimpleModule are stated with it — but does not name it. This file names it and records the two properties that pin it down: it is itself semisimple, and its submodules are exactly the semisimple submodules. So it is the largest semisimple submodule, and it is everything exactly when the module is semisimple.

Main definitions

• TauCeti.socle: the supremum of the simple submodules of a module.

Main results

• TauCeti.le_socle and TauCeti.socle_le: the defining supremum property.
• TauCeti.isSemisimpleModule_socle: the socle is a semisimple module.
• TauCeti.le_socle_iff_isSemisimpleModule: a submodule lies in the socle exactly when it is semisimple, so the socle is the largest semisimple submodule.
• TauCeti.socle_eq_top_iff: the socle is everything exactly for a semisimple module.

def TauCeti.socle (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] : Submodule R M

The socle of a module: the supremum of its simple submodules. It is the largest semisimple submodule, by TauCeti.isSemisimpleModule_socle and TauCeti.le_socle_iff_isSemisimpleModule.

theorem TauCeti.le_socle {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {m : Submodule R M} (hm : IsSimpleModule R ↥m) : m ≤ socle R M

Every simple submodule lies in the socle.

theorem TauCeti.socle_le {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} (h : ∀ (m : Submodule R M), IsSimpleModule R ↥m → m ≤ N) : socle R M ≤ N

A submodule containing every simple submodule contains the socle.

instance TauCeti.isSemisimpleModule_socle {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : IsSemisimpleModule R ↥(socle R M)

The socle is semisimple.

theorem TauCeti.le_socle_iff_isSemisimpleModule {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} : N ≤ socle R M ↔ IsSemisimpleModule R ↥N

A submodule lies in the socle exactly when it is semisimple, so the socle is the largest semisimple submodule.

theorem TauCeti.socle_eq_top_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] : socle R M = ⊤ ↔ IsSemisimpleModule R M

The socle is everything exactly for a semisimple module.

@[simp]

theorem TauCeti.socle_eq_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : socle R M = ⊤

The socle of a semisimple module is everything.