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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule.nontrivial {A : Type u} {M : Type v} [Semiring A] [AddCommMonoid M] [Module A M] (h : IsIndecomposableModule A M) : Nontrivial M

theorem QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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.