Minimal local lifts of simple quotient submodules

The direct biserial induction lifts two simple summands of rad L / rad² L to local submodules of rad L. Full inverse images need not be local. The correct construction chooses a minimal submodule mapping onto each simple summand; minimality makes the kernel its unique maximal submodule.

theorem MagnitudeConjecture.exists_local_submodule_mapping_onto_simple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] [IsArtinian R M] (f : M →ₗ[R] N) (S : Submodule R N) (hSsimple : IsSimpleModule R ↥S) (hSrange : S ≤ f.range) : ∃ (P : Submodule R M), Submodule.map f P = S ∧ IsSimpleModule R (↥P ⧸ Module.jacobson R ↥P) ∧ Nonempty ((↥P ⧸ Module.jacobson R ↥P) ≃ₗ[R] ↥S)

A simple submodule in the range of a map has a minimal lift whose top is canonically that simple module.

theorem MagnitudeConjecture.exists_spanning_local_lifts_of_complementary_simples {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (S T : Submodule R (M ⧸ Module.jacobson R M)) (hSsimple : IsSimpleModule R ↥S) (hTsimple : IsSimpleModule R ↥T) (hcompl : IsCompl S T) (hSTnoniso : ¬Nonempty (↥S ≃ₗ[R] ↥T)) : ∃ (P : Submodule R M) (Q : Submodule R M), P ⊔ Q = ⊤ ∧ IsSimpleModule R (↥P ⧸ Module.jacobson R ↥P) ∧ IsSimpleModule R (↥Q ⧸ Module.jacobson R ↥Q) ∧ Nonempty ((↥P ⧸ Module.jacobson R ↥P) ≃ₗ[R] ↥S) ∧ Nonempty ((↥Q ⧸ Module.jacobson R ↥Q) ≃ₗ[R] ↥T) ∧ ¬Nonempty ((↥P ⧸ Module.jacobson R ↥P) ≃ₗ[R] ↥Q ⧸ Module.jacobson R ↥Q) ∧ ¬Nonempty (↥P ≃ₗ[R] ↥Q)

Complementary nonisomorphic simple submodules of the top of a finite-length module lift to nonisomorphic local submodules which span the whole module.