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_iff_isIndecomposableModule_of_algebraMap_surjective: indecomposability is unchanged by restricting scalars along a surjective algebra map.
• 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.
• TauCeti.isIndecomposableModule_self: a local ring is indecomposable over itself.
• TauCeti.IsIndecomposableModule.nonempty_linearEquiv_of_free: an indecomposable free module is isomorphic to the scalar semiring.

Implementation notes

IsIndecomposableModule, its two projections, and its transport along a semilinear equivalence are stated for a semimodule over a semiring, since the submodule lattice and the order isomorphism it inherits from a semilinear equivalence need no subtraction; so is nontrivial_of_isLocalRing_end, which only reads 0 ≠ 1 off the endomorphism semiring. The free-module theorem also works over a semiring. The idempotent, splitting, and Fitting results are stated over a ring, where Mathlib puts the tools they use: 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

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] {B : Type u_1} [Semiring B] {σ : A →+* B} {τ : B →+* A} [RingHomInvPair σ τ] [RingHomInvPair τ σ] {N : Type w} [AddCommMonoid N] [Module B N] (h : IsIndecomposableModule A M) (e : M ≃ₛₗ[σ] N) : IsIndecomposableModule B N

Indecomposability transfers along a semilinear equivalence over mutually inverse scalar homomorphisms.

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.

Restriction of scalars along a surjection

theorem TauCeti.isIndecomposableModule_iff_isIndecomposableModule_of_algebraMap_surjective {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] {R : Type u_1} [CommRing R] [Algebra R A] [Module R M] [IsScalarTower R A M] (h : Function.Surjective ⇑(algebraMap R A)) : IsIndecomposableModule R M ↔ IsIndecomposableModule A M

Indecomposability is insensitive to restriction of scalars along a surjection: when algebraMap R A is surjective, the R-submodules and the A-submodules of M are the same, so M is indecomposable over R exactly when it is over A.

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.

theorem TauCeti.IsIndecomposableModule.isSimpleModule {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] [IsSemisimpleModule A M] (h : IsIndecomposableModule A M) : IsSimpleModule A M

An indecomposable semisimple module is simple.

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.

theorem TauCeti.isIndecomposableModule_self (A : Type u) [Ring A] [IsLocalRing A] : IsIndecomposableModule A A

A local ring is indecomposable as a left module over itself: its endomorphism ring is the opposite ring, which is again local.

Indecomposable free modules

theorem TauCeti.IsIndecomposableModule.nonempty_linearEquiv_of_free {A : Type u} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] [Module.Free A M] (h : IsIndecomposableModule A M) : Nonempty (M ≃ₗ[A] A)

An indecomposable free module is isomorphic to the scalar semiring. For a basis vector b i, its span and the span of the remaining basis vectors are complementary, so the latter span is zero and i is the only index.