feat: define finite length modules and show equivalence with `IsNoeth…

…erian ∧ IsArtinian` (#17478)

and equivalence with the existence of a CompositionSeries.

Add order-theoretic results: a simple order is finite; WellFoundedLT implies every non-top element is covered by some other element, and the dual result; WellFoundedLT + WellFoundedGT implies there exists a finite sequence from ⊥ to ⊤ with each element covering the previous one.

Also generalize two proof_wanted statements about semisimple modules/rings.

Mathlib.lean

@@ -3891,6 +3891,7 @@ import Mathlib.RingTheory.EssentialFiniteness
 import Mathlib.RingTheory.Etale.Basic
 import Mathlib.RingTheory.EuclideanDomain
 import Mathlib.RingTheory.Filtration
+import Mathlib.RingTheory.FiniteLength
 import Mathlib.RingTheory.FinitePresentation
 import Mathlib.RingTheory.FiniteStability
 import Mathlib.RingTheory.FiniteType

Mathlib/Order/Atoms/Finite.lean

@@ -22,23 +22,26 @@ variable {α β : Type*}
 
 namespace IsSimpleOrder
 
+variable [LE α] [BoundedOrder α] [IsSimpleOrder α]
+
 section DecidableEq
 
 /- It is important that `IsSimpleOrder` is the last type-class argument of this instance,
 so that type-class inference fails quickly if it doesn't apply. -/
-instance (priority := 200) {α} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] :
-    Fintype α :=
+instance (priority := 200) [DecidableEq α] : Fintype α :=
   Fintype.ofEquiv Bool equivBool.symm
 
 end DecidableEq
 
+instance (priority := 200) : Finite α := by classical infer_instance
+
 end IsSimpleOrder
 
 namespace Fintype
 
 namespace IsSimpleOrder
 
-variable [PartialOrder α] [BoundedOrder α] [IsSimpleOrder α] [DecidableEq α]
+variable [LE α] [BoundedOrder α] [IsSimpleOrder α] [DecidableEq α]
 
 theorem univ : (Finset.univ : Finset α) = {⊤, ⊥} := by
   change Finset.map _ (Finset.univ : Finset Bool) = _

Mathlib/Order/Cover.lean

@@ -591,3 +591,19 @@ variable [Preorder α] {a b : α}
   simp only [wcovBy_iff_Ioo_eq, ← image_coe_Iio, bot_le, image_eq_empty, true_and, Iio_eq_empty_iff]
 
 end WithBot
+
+section WellFounded
+
+variable [Preorder α]
+
+lemma exists_covBy_of_wellFoundedLT [wf : WellFoundedLT α] ⦃a : α⦄ (h : ¬ IsMax a) :
+    ∃ a', a ⋖ a' := by
+  rw [not_isMax_iff] at h
+  exact ⟨_, wellFounded_lt.min_mem _ h, fun a' ↦ wf.wf.not_lt_min _ h⟩
+
+lemma exists_covBy_of_wellFoundedGT [wf : WellFoundedGT α] ⦃a : α⦄ (h : ¬ IsMin a) :
+    ∃ a', a' ⋖ a := by
+  rw [not_isMin_iff] at h
+  exact ⟨_, wf.wf.min_mem _ h, fun a' h₁ h₂ ↦ wf.wf.not_lt_min _ h h₂ h₁⟩
+
+end WellFounded

Mathlib/Order/OrderIsoNat.lean

@@ -232,3 +232,20 @@ theorem WellFounded.iSup_eq_monotonicSequenceLimit [CompleteLattice α]
   · cases' WellFounded.monotone_chain_condition'.1 h a with n hn
     have : n ∈ {n | ∀ m, n ≤ m → a n = a m} := fun k hk => (a.mono hk).eq_of_not_lt (hn k hk)
     exact (Nat.sInf_mem ⟨n, this⟩ m hm.le).ge
+
+theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (α) [Preorder α]
+    [Nonempty α] [wfl : WellFoundedLT α] [wfg : WellFoundedGT α] :
+    ∃ a : ℕ → α, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1) := by
+  choose next hnext using exists_covBy_of_wellFoundedLT (α := α)
+  have hα := Set.nonempty_iff_univ_nonempty.mp ‹_›
+  classical
+  let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
+  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ hα trivial, ?_⟩
+  have cov n (hn : ¬ IsMax (a n)) : a n ⋖ a (n + 1) := by
+    change a n ⋖ if ha : IsMax (a n) then a n else _
+    rw [dif_neg hn]
+    exact hnext hn
+  have H : ∃ n, IsMax (a n) := by
+    by_contra!
+    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded_of_decreasing_seq wfg.wf
+  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ fun h' ↦ wellFounded_lt.not_lt_min _ H h' h⟩

Mathlib/RingTheory/Artinian.lean

@@ -522,7 +522,7 @@ instance [IsReduced R] : DecompositionMonoid (Polynomial R) :=
 theorem isSemisimpleRing_of_isReduced [IsReduced R] : IsSemisimpleRing R :=
   (equivPi R).symm.isSemisimpleRing
 
-proof_wanted IsSemisimpleRing.isArtinianRing (R : Type*) [CommRing R] [IsSemisimpleRing R] :
+proof_wanted IsSemisimpleRing.isArtinianRing (R : Type*) [Ring R] [IsSemisimpleRing R] :
     IsArtinianRing R
 
 end IsArtinianRing

Mathlib/RingTheory/FiniteLength.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2024 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.Order.Atoms.Finite
+import Mathlib.RingTheory.Artinian
+
+/-!
+# 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]`.
+
+## Tag
+
+Finite length, Composition series
+-/
+
+universe u
+
+variable (R : Type*) [Ring R]
+
+/-- A module of finite length is either trivial or a simple extension of a module known
+to be of finite length. -/
+inductive IsFiniteLength : ∀ (M : Type u) [AddCommGroup M] [Module R M], Prop
+  | of_subsingleton {M} [AddCommGroup M] [Module R M] [Subsingleton M] : IsFiniteLength M
+  | of_simple_quotient {M} [AddCommGroup M] [Module R M] {N : Submodule R M}
+      [IsSimpleModule R (M ⧸ N)] : IsFiniteLength N → IsFiniteLength M
+
+variable {R} {M N : Type*} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+
+theorem LinearEquiv.isFiniteLength (e : M ≃ₗ[R] N)
+    (h : IsFiniteLength R M) : IsFiniteLength R N := by
+  induction' h with M _ _ _ M _ _ S _ _ ih generalizing N
+  · have := e.symm.toEquiv.subsingleton; exact .of_subsingleton
+  · have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
+      IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
+    exact .of_simple_quotient (ih <| e.submoduleMap S)
+
+variable (R M) in
+theorem exists_compositionSeries_of_isNoetherian_isArtinian [IsNoetherian R M] [IsArtinian R M] :
+    ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ := by
+  obtain ⟨f, f0, n, hn⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (Submodule R M)
+  exact ⟨⟨n, fun i ↦ f i, fun i ↦ hn.2 i i.2⟩, f0.eq_bot, hn.1.eq_top⟩
+
+theorem isFiniteLength_of_exists_compositionSeries
+    (h : ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤) :
+    IsFiniteLength R M :=
+  Submodule.topEquiv.isFiniteLength <| by
+    obtain ⟨s, s_head, s_last⟩ := h
+    rw [← s_last]
+    suffices ∀ i, IsFiniteLength R (s i) from this (Fin.last _)
+    intro i
+    induction' i using Fin.induction with i ih
+    · change IsFiniteLength R s.head; rw [s_head]; exact .of_subsingleton
+    let cov := s.step i
+    have := (covBy_iff_quot_is_simple cov.le).mp cov
+    have := ((s i.castSucc).comap (s i.succ).subtype).equivMapOfInjective
+      _ (Submodule.injective_subtype _)
+    rw [Submodule.map_comap_subtype, inf_of_le_right cov.le] at this
+    exact .of_simple_quotient (this.symm.isFiniteLength ih)
+
+theorem isFiniteLength_iff_isNoetherian_isArtinian :
+    IsFiniteLength R M ↔ IsNoetherian R M ∧ IsArtinian R M :=
+  ⟨fun h ↦ h.rec (fun {M} _ _ _ ↦ ⟨inferInstance, inferInstance⟩) fun M _ _ {N} _ _ ⟨_, _⟩ ↦
+    ⟨(isNoetherian_iff_submodule_quotient N).mpr ⟨‹_›, isNoetherian_iff'.mpr inferInstance⟩,
+      (isArtinian_iff_submodule_quotient N).mpr ⟨‹_›, inferInstance⟩⟩,
+    fun ⟨_, _⟩ ↦ isFiniteLength_of_exists_compositionSeries
+      (exists_compositionSeries_of_isNoetherian_isArtinian R M)⟩
+
+theorem isFiniteLength_iff_exists_compositionSeries :
+    IsFiniteLength R M ↔ ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ :=
+  ⟨fun h ↦ have ⟨_, _⟩ := isFiniteLength_iff_isNoetherian_isArtinian.mp h
+    exists_compositionSeries_of_isNoetherian_isArtinian R M,
+    isFiniteLength_of_exists_compositionSeries⟩

Mathlib/RingTheory/SimpleModule.lean

@@ -338,7 +338,7 @@ variable (ι R)
 
 proof_wanted IsSemisimpleRing.mulOpposite [IsSemisimpleRing R] : IsSemisimpleRing Rᵐᵒᵖ
 
-proof_wanted IsSemisimpleRing.module_end [IsSemisimpleRing R] [Module.Finite R M] :
+proof_wanted IsSemisimpleRing.module_end [IsSemisimpleModule R M] [Module.Finite R M] :
     IsSemisimpleRing (Module.End R M)
 
 proof_wanted IsSemisimpleRing.matrix [Fintype ι] [DecidableEq ι] [IsSemisimpleRing R] :