Semisimple submodules of biserial modules

A semisimple submodule contained in the sum of two uniserial branches has composition length at most two. This is the structural length bound used for the intersection of the two local branches in the Pogorzały--Skowroński induction.

theorem MagnitudeConjecture.semisimple_submodule_le_moduleSocle {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P : Submodule R M) [IsSemisimpleModule R ↥P] : P ≤ moduleSocle R M

Every semisimple submodule is contained in the socle of the ambient module.

theorem MagnitudeConjecture.semisimple_submodule_length_le_two_of_le_sup_uniserial {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (U V P : Submodule R M) (hU : IsUniserialModule R ↥U) (hV : IsUniserialModule R ↥V) (hP : P ≤ U ⊔ V) [IsSemisimpleModule R ↥P] : Module.length R ↥P ≤ 2

A semisimple submodule contained in the sum of two uniserial submodules has composition length at most two. Quotienting by the first branch makes the kernel embed in the first branch and the range embed in the second.

theorem MagnitudeConjecture.semisimple_submodule_length_le_two_of_biserial_of_le_jacobson {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (hM : IsBiserialModule R M) (P : Submodule R M) (hP : P ≤ Module.jacobson R M) [IsSemisimpleModule R ↥P] : Module.length R ↥P ≤ 2

A semisimple submodule of the radical of a biserial module has composition length at most two.

theorem MagnitudeConjecture.semisimple_submodule_eq_moduleSocle_of_biserial_of_simple_top_of_length_eq_two {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (hMbis : IsBiserialModule R M) (hMtop : IsSimpleModule R (M ⧸ Module.jacobson R M)) (P : Submodule R M) [IsSemisimpleModule R ↥P] (hPjac : P ≤ Module.jacobson R M) (hPlength : Module.length R ↥P = 2) : P = moduleSocle R M

A semisimple length-two submodule of the radical of a local biserial module is its whole socle.

theorem MagnitudeConjecture.isSimpleModule_of_nontrivial_of_length_le_two_of_ne_two {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial M] (hle : Module.length R M ≤ 2) (hne : Module.length R M ≠ 2) : IsSimpleModule R M

A nonzero finite-length module of length at most two is simple as soon as the length-two case has been excluded.

theorem MagnitudeConjecture.exists_complementary_simple_of_semisimple_of_length_eq_two {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] [IsSemisimpleModule R M] (hlength : Module.length R M = 2) : ∃ (S : Submodule R M) (T : Submodule R M), IsSimpleModule R ↥S ∧ IsSimpleModule R ↥T ∧ IsCompl S T

A semisimple module of composition length two is a direct sum of two simple submodules.

theorem MagnitudeConjecture.IsBiserialModule.of_semisimple_jacobson_length_le_two {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] [IsSemisimpleModule R ↥(Module.jacobson R M)] (hlength : Module.length R ↥(Module.jacobson R M) ≤ 2) : IsBiserialModule R M

A module whose Jacobson radical is semisimple of composition length at most two is biserial. At length two, split the radical into two simple summands; below length two, the radical is simple or zero.

theorem MagnitudeConjecture.exists_three_simple_nested_complements_of_semisimple_of_length_not_le_two {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] [IsSemisimpleModule R M] (hlength : ¬Module.length R M ≤ 2) : ∃ (S : Submodule R M) (C : Submodule R M) (T : Submodule R ↥C) (D : Submodule R ↥C) (U : Submodule R ↥D) (V : Submodule R ↥D), IsSimpleModule R ↥S ∧ IsCompl S C ∧ IsSimpleModule R ↥T ∧ IsCompl T D ∧ IsSimpleModule R ↥U ∧ IsCompl U V

A semisimple finite-length module of length greater than two admits three successive simple summands. The nested complement form is convenient for later quotient constructions: M = S ⊕ C, C = T ⊕ D, and D = U ⊕ V.