Actions of the ring radical on finite-length modules

Over a semiprimary ring, the module radical is generated by the ring Jacobson radical. Iterating this identity identifies the second and third module radicals with the actions of the corresponding powers of the ring radical. For a uniserial module of length three, a generator is consequently sent nontrivially into the socle by some element of the square.

theorem MagnitudeConjecture.moduleJacobson_eq_ringJacobson_smul_top {R : Type u} [Ring R] [IsSemiprimaryRing R] {M : Type v} [AddCommGroup M] [Module R M] : Module.jacobson R M = Ring.jacobson R • ⊤

Over a semiprimary ring, the radical of a module is the submodule generated by the action of the ring Jacobson radical.

theorem MagnitudeConjecture.map_iteratedModuleJacobson_eq_ringJacobson_sq_smul_top {R : Type u} [Ring R] [IsSemiprimaryRing R] {M : Type v} [AddCommGroup M] [Module R M] : Submodule.map (Module.jacobson R M).subtype (Module.jacobson R ↥(Module.jacobson R M)) = Ring.jacobson R ^ 2 • ⊤

The image in M of the iterated module radical is the action of the square of the ring Jacobson radical.

theorem MagnitudeConjecture.map_thriceIteratedModuleJacobson_eq_ringJacobson_cube_smul_top {R : Type u} [Ring R] [IsSemiprimaryRing R] {M : Type v} [AddCommGroup M] [Module R M] : Submodule.map ((Module.jacobson R M).subtype ∘ₗ (Module.jacobson R ↥(Module.jacobson R M)).subtype) (Module.jacobson R ↥(Module.jacobson R ↥(Module.jacobson R M))) = Ring.jacobson R ^ 3 • ⊤

The image in M of the third iterated module radical is the action of the cube of the ring Jacobson radical.

theorem MagnitudeConjecture.exists_radicalSquare_smul_ne_zero_mem_socle {R : Type u} [Ring R] [IsSemiprimaryRing R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] [Nontrivial M] (hM : IsUniserialModule R M) (hlength : Module.length R M = 3) (u : M) (hu : u ∉ Module.jacobson R M) : ∃ r ∈ Ring.jacobson R ^ 2, r • u ≠ 0 ∧ r • u ∈ moduleSocle R M

In a length-three uniserial module, some element of the square of the ring radical sends every vector outside the module radical to a nonzero socle vector.