The first radical layer of a nonuniserial biserial module

For a finite-length biserial module with simple top, nonuniseriality forces the top of its Jacobson radical to have composition length two. Consequently that semisimple layer is the direct sum of two simple submodules. This is the radical-layer decomposition used in the direct Pogorzały--Skowroński induction.

theorem MagnitudeConjecture.isSimpleOrZeroModule_of_uniserial_of_semisimple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] (hM : IsUniserialModule R M) : IsSimpleOrZeroModule R M

A semisimple uniserial module is simple unless it is zero.

theorem MagnitudeConjecture.IsSimpleOrZeroModule.length_le_one {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (hM : IsSimpleOrZeroModule R M) : Module.length R M ≤ 1

A simple-or-zero finite-length module has length at most one.

theorem MagnitudeConjecture.IsUniserialModule.range {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (hM : IsUniserialModule R M) (f : M →ₗ[R] N) : IsUniserialModule R ↥f.range

The image of a uniserial module under a linear map is uniserial.

theorem MagnitudeConjecture.top_jacobson_length_le_two_of_biserial {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] [IsArtinian R M] [IsNoetherian R M] (hbis : IsBiserialModule R M) : Module.length R (↥(Module.jacobson R M) ⧸ Module.jacobson R ↥(Module.jacobson R M)) ≤ 2

The top of the Jacobson radical of a finite-length biserial module has composition length at most two.

theorem MagnitudeConjecture.top_jacobson_length_eq_two_of_biserial_of_not_uniserial {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] [IsArtinian R M] [IsNoetherian R M] (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) (hbis : IsBiserialModule R M) (hnotuni : ¬IsUniserialModule R M) : Module.length R (↥(Module.jacobson R M) ⧸ Module.jacobson R ↥(Module.jacobson R M)) = 2

If a finite-length module with simple top is biserial but not uniserial, then the top of its Jacobson radical has composition length two.

theorem MagnitudeConjecture.exists_complementary_simple_top_jacobson_of_biserial_of_not_uniserial {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] [IsArtinian R M] [IsNoetherian R M] (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) (hbis : IsBiserialModule R M) (hnotuni : ¬IsUniserialModule R M) : ∃ (S : Submodule R (↥(Module.jacobson R M) ⧸ Module.jacobson R ↥(Module.jacobson R M))) (T : Submodule R (↥(Module.jacobson R M) ⧸ Module.jacobson R ↥(Module.jacobson R M))), IsSimpleModule R ↥S ∧ IsSimpleModule R ↥T ∧ IsCompl S T

The length-two semisimple top of the radical splits as two complementary simple submodules.