Indecomposable modules and Fitting's lemma

A module is indecomposable when it is nonzero and is not the internal direct sum of two nonzero submodules. This file introduces the predicate, records its idempotent reformulation, and proves Fitting's lemma: an endomorphism of an indecomposable module of finite length is either nilpotent or bijective, so the endomorphism ring of such a module is local.

Mathlib has the Fitting decomposition of an endomorphism of a Noetherian and Artinian module (LinearMap.eventually_isCompl_ker_pow_range_pow) and CategoryTheory.Indecomposable for objects of a category with binary biproducts, but no module-level indecomposability predicate and no local-endomorphism-ring theorem. Both are supplied here.

Main definitions

• TauCeti.IsIndecomposableModule A M: M is a nonzero A-module admitting no decomposition M = N ⊕ P with N and P both nonzero.

Main results

• TauCeti.isIndecomposableModule_iff_nontrivial_and_forall_isIdempotentElem: indecomposability says exactly that M is nontrivial and 0 and 1 are the only idempotents of Module.End A M.
• TauCeti.IsIndecomposableModule.bijective_of_bijective_comp: a split injection into an indecomposable module is an isomorphism, that is, if g ∘ₗ f is bijective and the module f lands in is indecomposable, then f is bijective.
• TauCeti.IsIndecomposableModule.isNilpotent_or_bijective: Fitting's lemma, for a module that is Noetherian and Artinian, together with TauCeti.IsIndecomposableModule.isNilpotent_iff_not_isUnit, which reads it as an identification of the non-units of the endomorphism ring with its nilpotents.
• TauCeti.isLocalRing_end_of_isIndecomposable: the endomorphism ring of an indecomposable module of finite length is local, and TauCeti.nontrivial_of_isLocalRing_end for the converse direction that a local endomorphism ring forces the module to be nonzero.
• TauCeti.isIndecomposableModule_iff_isLocalRing_end: for a module of finite length the converse holds too, so indecomposability is equivalent to having a local endomorphism ring.

Implementation notes

IsIndecomposableModule, its two projections, and its transport along a linear equivalence are stated for a semimodule over a semiring, since the submodule lattice and the order isomorphism it inherits from a linear equivalence need no subtraction; so is nontrivial_of_isLocalRing_end, which only reads 0 ≠ 1 off the endomorphism semiring. Everything from the idempotent reformulation onwards is stated over a ring, which is where Mathlib puts the tools it uses: LinearMap.IsIdempotentElem.isCompl and Submodule.projection build a projection by subtracting, and IsSimpleModule is itself only defined for modules over a ring.

The finiteness hypothesis is carried as the pair of instances [IsNoetherian A M] [IsArtinian A M] on the lemmas that consume it, which is what Mathlib's Fitting decomposition asks for. The IsFiniteLength A M spelling appears on the headline statements isLocalRing_end_of_isIndecomposable and isIndecomposableModule_iff_isLocalRing_end, which unpack it through isFiniteLength_iff_isNoetherian_isArtinian.

References

This implements the Fitting's lemma bullet of Layer 2 ("the Krull-Schmidt theorem") of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, pinned as isLocalRing_end_of_isIndecomposable 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.

def TauCeti.IsIndecomposableModule (A : Type u) (M : Type v) [Semiring A] [AddCommMonoid M] [Module A M] : Prop

A module is indecomposable when it is nonzero and is not the internal direct sum of two nonzero submodules.

Equations

• TauCeti.IsIndecomposableModule A M = (Nontrivial M ∧ ∀ (N P : Submodule A M), IsCompl N P → N = ⊥ ∨ P = ⊥)

theorem TauCeti.isIndecomposableModule_iff_nontrivial_and_forall_isCompl {A : Type u} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] : IsIndecomposableModule A M ↔ Nontrivial M ∧ ∀ (N P : Submodule A M), IsCompl N P → N = ⊥ ∨ P = ⊥

IsIndecomposableModule restated as the conjunction defining it, so that clients can establish and consume it without unfolding the definition.

theorem TauCeti.isIndecomposableModule_of_forall_isCompl {A : Type u} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] [Nontrivial M] (h : ∀ (N P : Submodule A M), IsCompl N P → N = ⊥ ∨ P = ⊥) : IsIndecomposableModule A M

A nontrivial module along none of whose decompositions M = N ⊕ P both summands are nonzero is indecomposable.

theorem TauCeti.IsIndecomposableModule.nontrivial {A : Type u} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] (h : IsIndecomposableModule A M) : Nontrivial M

theorem TauCeti.IsIndecomposableModule.eq_bot_or_eq_bot {A : Type u} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] (h : IsIndecomposableModule A M) {N P : Submodule A M} (hNP : IsCompl N P) : N = ⊥ ∨ P = ⊥

theorem TauCeti.IsIndecomposableModule.of_linearEquiv {A : Type u} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] {N : Type w} [AddCommMonoid N] [Module A N] (h : IsIndecomposableModule A M) (e : M ≃ₗ[A] N) : IsIndecomposableModule A N

Indecomposability transfers along a linear equivalence: the induced order isomorphism of submodules carries a decomposition of the target back to one of the source.

theorem TauCeti.nontrivial_of_isLocalRing_end {A : Type u} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] [IsLocalRing (Module.End A M)] : Nontrivial M

A module with local endomorphism ring is nonzero: over the zero module the endomorphism ring is the zero ring, which is not local.

Indecomposability through idempotent endomorphisms

theorem TauCeti.IsIndecomposableModule.eq_zero_or_eq_one_of_isIdempotentElem {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] (h : IsIndecomposableModule A M) {f : Module.End A M} (hf : IsIdempotentElem f) : f = 0 ∨ f = 1

The idempotent endomorphisms of an indecomposable module are 0 and 1: an idempotent splits the module as the direct sum of its range and its kernel, and one of the two must vanish.

theorem TauCeti.isIndecomposableModule_of_forall_isIdempotentElem {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] [Nontrivial M] (h : ∀ (f : Module.End A M), IsIdempotentElem f → f = 0 ∨ f = 1) : IsIndecomposableModule A M

A nonzero module whose only idempotent endomorphisms are 0 and 1 is indecomposable: a decomposition M = N ⊕ P is witnessed by the projection onto N along P.

theorem TauCeti.isIndecomposableModule_iff_nontrivial_and_forall_isIdempotentElem {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] : IsIndecomposableModule A M ↔ Nontrivial M ∧ ∀ (f : Module.End A M), IsIdempotentElem f → f = 0 ∨ f = 1

Indecomposability of a module is exactly the statement that it is nontrivial and its endomorphism ring has no idempotents besides 0 and 1.

theorem TauCeti.IsSimpleModule.isIndecomposableModule {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] [IsSimpleModule A M] : IsIndecomposableModule A M

A simple module is indecomposable: it has no proper nonzero submodule to decompose along.

Splitting off an indecomposable module

theorem TauCeti.IsIndecomposableModule.bijective_of_bijective_comp {A : Type u} [Ring A] {N : Type u_1} {P : Type u_2} [AddCommGroup N] [Module A N] [AddCommGroup P] [Module A P] [Nontrivial N] (hP : IsIndecomposableModule A P) {f : N →ₗ[A] P} {g : P →ₗ[A] N} (h : Function.Bijective ⇑(g ∘ₗ f)) : Function.Bijective ⇑f

A split injection into an indecomposable module is an isomorphism. If g ∘ₗ f is bijective then f ∘ₗ (g ∘ₗ f)⁻¹ ∘ₗ g is an idempotent endomorphism of the indecomposable module f lands in, hence is 0 or 1; it cannot be 0, because that would force f to vanish on a nontrivial module, so it is the identity and f is surjective.

Fitting's lemma

theorem TauCeti.IsIndecomposableModule.isNilpotent_or_bijective {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] [IsNoetherian A M] [IsArtinian A M] (h : IsIndecomposableModule A M) (f : Module.End A M) : IsNilpotent f ∨ Function.Bijective ⇑f

Fitting's lemma: an endomorphism of an indecomposable module that is both Noetherian and Artinian is either nilpotent or bijective.

For a large enough exponent m, Mathlib's Fitting decomposition splits M as ker (f ^ m) ⊕ range (f ^ m). Indecomposability collapses one of the two summands: if the range vanishes then f ^ m = 0, and if the kernel vanishes then f is injective while the range, being everything, forces f to be surjective.

theorem TauCeti.IsIndecomposableModule.isNilpotent_or_isUnit {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] [IsNoetherian A M] [IsArtinian A M] (h : IsIndecomposableModule A M) (f : Module.End A M) : IsNilpotent f ∨ IsUnit f

Fitting's lemma, restated: an endomorphism of an indecomposable module that is both Noetherian and Artinian is either nilpotent or a unit of the endomorphism ring.

theorem TauCeti.IsIndecomposableModule.isNilpotent_iff_not_isUnit {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] [IsNoetherian A M] [IsArtinian A M] (h : IsIndecomposableModule A M) (f : Module.End A M) : IsNilpotent f ↔ ¬IsUnit f

On an indecomposable module that is Noetherian and Artinian, the non-units of the endomorphism ring are exactly the nilpotent endomorphisms. This identifies the maximal ideal produced by TauCeti.isLocalRing_end_of_isIndecomposable.

Local endomorphism rings

theorem TauCeti.isLocalRing_end_of_isIndecomposable {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] (hM : IsFiniteLength A M) (h : IsIndecomposableModule A M) : IsLocalRing (Module.End A M)

The endomorphism ring of an indecomposable module of finite length is local.

This is the form of Fitting's lemma that drives the Krull-Schmidt theorem: a non-unit endomorphism is nilpotent, and 1 - f is then a unit.

theorem TauCeti.isIndecomposableModule_of_isLocalRing_end {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] [IsLocalRing (Module.End A M)] : IsIndecomposableModule A M

A module with local endomorphism ring is indecomposable. This is the converse of TauCeti.isLocalRing_end_of_isIndecomposable, and needs no finiteness hypothesis; nontriviality comes for free, by TauCeti.nontrivial_of_isLocalRing_end.

theorem TauCeti.isIndecomposableModule_iff_isLocalRing_end {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] (hM : IsFiniteLength A M) : IsIndecomposableModule A M ↔ IsLocalRing (Module.End A M)

For a module of finite length, indecomposability is equivalent to having a local endomorphism ring.