An indecomposability criterion for the biserial obstruction modules

The kernel modules in the Pogorzały--Skowroński proof are shown indecomposable by considering a hypothetical complementary decomposition. Induction makes both summands uniserial; one summand escapes an ambient radical and the element calculation then forces that summand to contain the whole socle. The other nonzero summand must meet the socle, contradicting disjointness. This file packages the general lattice argument, leaving only the source-specific element calculation as a later obligation.

theorem MagnitudeConjecture.simple_moduleSocles_of_isCompl_of_length_eq_two {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] (P Q : Submodule R M) (hPQ : IsCompl P Q) (hP : P ≠ ⊥) (hQ : Q ≠ ⊥) (hlength : Module.length R ↥(moduleSocle R M) = 2) : IsSimpleModule R ↥(moduleSocle R ↥P) ∧ IsSimpleModule R ↥(moduleSocle R ↥Q)

If the ambient socle has composition length two, the two nonzero summands in any complementary decomposition both have simple socle.

theorem MagnitudeConjecture.isIndecomposableModule_of_complement_uniserial_of_capture_socle {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [Nontrivial M] (J : Submodule R M) (hJ : J ≠ ⊤) (huniserial : ∀ (P Q : Submodule R M), IsCompl P Q → P ≠ ⊥ → Q ≠ ⊥ → IsUniserialModule R ↥P ∧ IsUniserialModule R ↥Q) (hcapture : ∀ (P : Submodule R M), P ≠ ⊥ → IsUniserialModule R ↥P → ¬P ≤ J → moduleSocle R M ≤ P) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R M

A complementary decomposition is impossible if induction makes both nonzero summands uniserial and every uniserial summand escaping J contains the whole socle.

theorem MagnitudeConjecture.complement_uniserial_of_length_five_of_two_socle_layers {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (hlength : Module.length R M = 5) (hsocleLength : Module.length R ↥(moduleSocle R M) = 2) (hnextLength : Module.length R ↥(moduleSocle R (M ⧸ moduleSocle R M)) = 2) (P Q : Submodule R M) (hPQ : IsCompl P Q) (hP : P ≠ ⊥) (hQ : Q ≠ ⊥) (hpNextLe : Module.length R ↥(moduleSocle R (↥P ⧸ moduleSocle R ↥P)) ≤ 1) (hqNextLe : Module.length R ↥(moduleSocle R (↥Q ⧸ moduleSocle R ↥Q)) ≤ 1) : IsUniserialModule R ↥P ∧ IsUniserialModule R ↥Q

The precise two-layer length argument behind the source's assertion that the two nonzero summands of its length-five kernel are uniserial. The final two premises are the summand-specific multiplicity-free bounds: neither complement can contribute both factors in the next socle layer.