Existence of a decomposition into indecomposable submodules

The Krull-Schmidt theorem has two halves: every module of finite length is a finite internal direct sum of indecomposable submodules, and that decomposition is unique up to a matching of the summands. This file proves the first half. Uniqueness, whose proof is the exchange argument on the local endomorphism rings supplied by TauCeti.isLocalRing_end_of_isIndecomposable, is TauCeti.exists_equiv_linearEquiv_of_iSupIndep, in TauCeti/RingTheory/KrullSchmidt/Uniqueness.lean.

Existence needs strictly less than finite length: the descending chain condition alone suffices. A nonzero submodule that is not indecomposable splits as N ⊕ Q with both summands nonzero, hence both strictly smaller, and the recursion terminates because an Artinian module has no infinite strictly decreasing chain of submodules. The proof below is exactly that recursion, run by well-founded induction on the submodule lattice, so the results are stated for [IsArtinian A M] and the finite-length form is a corollary.

Running the induction over the submodules of a fixed M — rather than over modules — is what keeps the argument short: the recursive calls land on submodules of M again, so the finite sets of summands produced by the two halves live in one type and are combined by Finset.union, with no transport along Submodule.map anywhere in the induction. The price is one translation lemma, TauCeti.isIndecomposableModule_coe_iff, which reads indecomposability of ↥P off the interval below P in the ambient lattice; it is proved once, at the start, out of Mathlib's order isomorphism Submodule.mapIic.

Main results

• TauCeti.isIndecomposableModule_coe_iff: a submodule P is indecomposable exactly when it is nonzero and admits no splitting P = N ⊕ Q into two nonzero submodules of the ambient module.
• TauCeti.exists_finset_isIndecomposableModule_supIndep_sup_eq: every submodule of an Artinian module is the internal direct sum of a finite set of indecomposable submodules. This is the induction, and the statement the recursion is strong enough to carry.
• TauCeti.exists_isInternal_isIndecomposableModule: existence of an indecomposable decomposition for an Artinian module, packaged as DirectSum.IsInternal.
• TauCeti.exists_indecomposable_decomposition: the same for a module of finite length, the form the Krull-Schmidt statement uses, and TauCeti.exists_isInternal_isIndecomposableModule_of_finiteDimensional for a module that is finite-dimensional over a division ring acting through a scalar tower.
• TauCeti.exists_isCompl_isIndecomposableModule: a nonzero Artinian module has an indecomposable direct summand.

Implementation notes

The two lattice lemmas read indecomposability off the submodule lattice and need no subtraction, so they are stated for a semimodule over a semiring, matching the generality of IsIndecomposableModule itself. The decomposition statements are over a ring: assembling the two halves of the induction is Finset.SupIndep.union, which needs IsModularLattice (Submodule A M), and Mathlib establishes that instance only for [Ring A] [AddCommGroup M], its proof going through Submodule.sup_inf_assoc_of_le_of_neg_le.

References

This implements the "existence of a decomposition" bullet of Layer 2 ("the Krull-Schmidt theorem") of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, pinned as exists_indecomposable_decomposition in its Suggested.lean.

See I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.4.

Reading a submodule's decompositions in the ambient lattice

theorem TauCeti.isIndecomposableModule_coe_iff {A : Type u} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] (P : Submodule A M) : IsIndecomposableModule A ↥P ↔ P ≠ ⊥ ∧ ∀ (N Q : Submodule A M), N ≤ P → Q ≤ P → Disjoint N Q → N ⊔ Q = P → N = ⊥ ∨ Q = ⊥

Indecomposability of a submodule, read in the ambient lattice. The module ↥P is indecomposable exactly when P is nonzero and every splitting of P as an internal direct sum of two submodules of M has a zero summand.

theorem TauCeti.exists_lt_lt_of_not_isIndecomposableModule {A : Type u} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] {P : Submodule A M} (hP : P ≠ ⊥) (h : ¬IsIndecomposableModule A ↥P) : ∃ (N : Submodule A M) (Q : Submodule A M), N < P ∧ Q < P ∧ Disjoint N Q ∧ N ⊔ Q = P

A nonzero submodule that is not indecomposable splits into two nonzero submodules of the ambient module, each of them strictly smaller.

Existence of the decomposition

theorem TauCeti.exists_finset_isIndecomposableModule_supIndep_sup_eq {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] [IsArtinian A M] (P : Submodule A M) : ∃ (s : Finset (Submodule A M)), (∀ N ∈ s, IsIndecomposableModule A ↥N) ∧ s.SupIndep id ∧ s.sup id = P

Every submodule of an Artinian module is the internal direct sum of a finite set of indecomposable submodules, recorded as a Finset of submodules that is Finset.SupIndep with supremum the given submodule.

For the module itself, see TauCeti.exists_isInternal_isIndecomposableModule.

theorem TauCeti.exists_isInternal_isIndecomposableModule {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] [IsArtinian A M] : ∃ (s : Finset (Submodule A M)), (∀ N ∈ s, IsIndecomposableModule A ↥N) ∧ DirectSum.IsInternal fun (N : ↥s) => ↑N

Existence of an indecomposable decomposition. An Artinian module is the internal direct sum of a finite set of indecomposable submodules.

theorem TauCeti.exists_isCompl_isIndecomposableModule {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] [IsArtinian A M] [Nontrivial M] : ∃ (N : Submodule A M) (Q : Submodule A M), IsCompl N Q ∧ IsIndecomposableModule A ↥N

A nonzero Artinian module has an indecomposable direct summand: some indecomposable submodule N admits a complement.

theorem TauCeti.exists_indecomposable_decomposition {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] (hM : IsFiniteLength A M) : ∃ (s : Finset (Submodule A M)), (∀ N ∈ s, IsIndecomposableModule A ↥N) ∧ DirectSum.IsInternal fun (N : ↥s) => ↑N

Existence of an indecomposable decomposition for a module of finite length: it is the internal direct sum of a finite set of indecomposable submodules.

This is the existence half of the Krull-Schmidt theorem, in the hypotheses that theorem is usually stated with; TauCeti.exists_isInternal_isIndecomposableModule is the same statement under the weaker Artinian hypothesis.

theorem TauCeti.exists_isInternal_isIndecomposableModule_of_finiteDimensional {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] (k : Type u_1) [DivisionRing k] [SMul k A] [Module k M] [IsScalarTower k A M] [FiniteDimensional k M] : ∃ (s : Finset (Submodule A M)), (∀ N ∈ s, IsIndecomposableModule A ↥N) ∧ DirectSum.IsInternal fun (N : ↥s) => ↑N

A module that is finite-dimensional over a division ring acting through a scalar tower — in particular a finite-dimensional module over a finite-dimensional algebra — is the internal direct sum of a finite set of indecomposable submodules.