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.

def MBDVendor.QSE.Foundation.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.

theorem MBDVendor.QSE.Foundation.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.

theorem MBDVendor.QSE.Foundation.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 both summands are nonzero is indecomposable.

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

theorem MBDVendor.QSE.Foundation.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 MBDVendor.QSE.Foundation.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.

Indecomposability through idempotent endomorphisms

theorem MBDVendor.QSE.Foundation.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.

theorem MBDVendor.QSE.Foundation.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.

theorem MBDVendor.QSE.Foundation.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 is equivalent to nontriviality together with having no idempotent endomorphisms besides 0 and 1.

theorem MBDVendor.QSE.Foundation.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.

Fitting's lemma

theorem MBDVendor.QSE.Foundation.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 Noetherian and Artinian module is either nilpotent or bijective.

theorem MBDVendor.QSE.Foundation.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 using units of the endomorphism ring.

theorem MBDVendor.QSE.Foundation.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 Noetherian and Artinian module, the non-units of the endomorphism ring are exactly its nilpotents.

Local endomorphism rings

theorem MBDVendor.QSE.Foundation.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 finite-length module is local.

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

A nonzero module with local endomorphism ring is indecomposable.

theorem MBDVendor.QSE.Foundation.isIndecomposableModule_iff_nontrivial_and_isLocalRing_end {A : Type u} {M : Type v} [Ring A] [AddCommGroup M] [Module A M] (hM : IsFiniteLength A M) : IsIndecomposableModule A M ↔ Nontrivial M ∧ IsLocalRing (Module.End A M)

For a finite-length module, indecomposability is equivalent to being nontrivial and having a local endomorphism ring.