Finite-length semisimplicity reductions

A nonsemisimple finite-length module contains a nonsimple indecomposable submodule. The proof uses a submodule of minimal nonsemisimple length and does not require a separately chosen Krull--Schmidt decomposition.

theorem MagnitudeConjecture.exists_nonsimple_indecomposable_submodule_of_not_semisimple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (hM : ¬IsSemisimpleModule R M) : ∃ (E : Submodule R M), QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R ↥E ∧ ¬IsSimpleModule R ↥E

A finite-length nonsemisimple module has a nonsimple indecomposable submodule.

theorem MagnitudeConjecture.exists_nonsimple_indecomposable_simpleTop_submodule_of_not_semisimple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (hM : ¬IsSemisimpleModule R M) : ∃ (E : Submodule R M), QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R ↥E ∧ ¬IsSimpleModule R ↥E ∧ IsSimpleModule R (↥E ⧸ Module.jacobson R ↥E)

A finite-length nonsemisimple module contains a nonsimple indecomposable submodule with simple top. Choose a minimal nonsemisimple submodule. If its top split into two nonzero summands, their two proper inverse images would be semisimple and would sum to the chosen submodule.

theorem MagnitudeConjecture.exists_maximal_nonsimple_indecomposable_submodule_of_not_semisimple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (hM : ¬IsSemisimpleModule R M) : ∃ (E : Submodule R M), QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R ↥E ∧ ¬IsSimpleModule R ↥E ∧ ∀ (F : Submodule R M), E ≤ F → QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R ↥F → ¬IsSimpleModule R ↥F → F = E

A finite-length nonsemisimple module has a maximal nonsimple indecomposable submodule. Maximality is by inclusion among submodules with those two intrinsic properties.

theorem MagnitudeConjecture.exists_maximal_nonsimple_indecomposable_submodule_le_of_not_semisimple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (I : Submodule R M) (hI : ¬IsSemisimpleModule R ↥I) : ∃ E ≤ I, QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R ↥E ∧ ¬IsSimpleModule R ↥E ∧ ∀ (F : Submodule R M), E ≤ F → F ≤ I → QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R ↥F → ¬IsSimpleModule R ↥F → F = E

Ambient form of the maximal extraction: a nonsemisimple submodule contains an ambient submodule maximal among the nonsimple indecomposables which it contains.