Modules of finite length

We define modules of finite length (IsFiniteLength) to be finite iterated extensions of simple modules, and show that a module is of finite length iff it is both Noetherian and Artinian, iff it admits a composition series.

We do not make IsFiniteLength a class, instead we use [IsNoetherian R M] [IsArtinian R M].

Tags

Finite length, Composition series

inductive IsFiniteLength (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] : Prop

A module of finite length is either trivial or a simple extension of a module known to be of finite length.

• of_subsingleton {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [Subsingleton M] : IsFiniteLength R M
• of_simple_quotient {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Submodule R M} [IsSimpleModule R (M ⧸ N)] : IsFiniteLength R ↥N → IsFiniteLength R M

theorem LinearEquiv.isFiniteLength {R : Type u_1} [Ring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) (h : IsFiniteLength R M) : IsFiniteLength R N

theorem exists_compositionSeries_of_isNoetherian_isArtinian (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsNoetherian R M] [IsArtinian R M] : ∃ (s : CompositionSeries (Submodule R M)), RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤

theorem isFiniteLength_of_exists_compositionSeries {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (h : ∃ (s : CompositionSeries (Submodule R M)), RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤) : IsFiniteLength R M

theorem isFiniteLength_iff_isNoetherian_isArtinian {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] : IsFiniteLength R M ↔ IsNoetherian R M ∧ IsArtinian R M

theorem isFiniteLength_iff_exists_compositionSeries {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] : IsFiniteLength R M ↔ ∃ (s : CompositionSeries (Submodule R M)), RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤

theorem IsSemisimpleModule.finite_tfae {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M, ∃ (s : Set (Submodule R M)), s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE

instance instIsArtinianOfIsSemisimpleModuleOfFinite {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Module.Finite R M] : IsArtinian R M

theorem IsFiniteLength.of_injective {R : Type u_1} [Ring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (H : IsFiniteLength R N) (hf : Function.Injective ⇑f) : IsFiniteLength R M

theorem IsFiniteLength.of_surjective {R : Type u_1} [Ring R] {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} (H : IsFiniteLength R M) (hf : Function.Surjective ⇑f) : IsFiniteLength R N