[Merged by Bors] - feat: define finite length modules and show equivalence with IsNoetherian ∧ IsArtinian

[alreadydone]

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.

---

• depends on: [Merged by Bors] - feat: Noetherian/Artinian is closed under extensions (submodule form) #17425

[github-actions]

PR summary 2bb78d082e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.RingTheory.FiniteLength	1237

---

Declarations diff

+ IsFiniteLength
+ LinearEquiv.isFiniteLength
+ exists_compositionSeries_of_isNoetherian_isArtinian
+ exists_covBy_of_wellFoundedGT
+ exists_covBy_of_wellFoundedLT
+ exists_covBy_seq_of_wellFoundedLT_wellFoundedGT
+ instance (priority := 200) : Finite α := by classical infer_instance
+ instance (priority := 200) [DecidableEq α] : Fintype α
+ isFiniteLength_iff_exists_compositionSeries
+ isFiniteLength_iff_isNoetherian_isArtinian
+ isFiniteLength_of_exists_compositionSeries
- instance (priority := 200) {α} [DecidableEq α] [LE α] [BoundedOrder α] [IsSimpleOrder α] :

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: Noetherian/Artinian is closed under extensions (submodule form) #17425
  By Dependent Issues (🤖). Happy coding!

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[ocfnash]

Firstly thank you for doing this work, I'm really glad that we now have these results.

However since I was whining about this on Zulip I thought I might outline the API that I would have preferred. Instead of having the definition IsFiniteLength and its API, we would have the following two results (and whatever was required to support them):

theorem isNoetherian_and_isArtinian_iff_exists_compositionSeries :
    IsNoetherian R M ∧ IsArtinian R M ↔
    ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤ := by
  sorry

theorem isNoetherian_and_isArtinian_iff_exists_submodule :
    IsNoetherian R M ∧ IsArtinian R M ↔
    Subsingleton M ∨
    ∃ p : Submodule R M, IsSimpleModule R (M ⧸ p) ∧ IsNoetherian R p ∧ IsArtinian R p := by
  sorry

I have just too many draws on my time at the moment to make PR with this refactor but I think it should be easy given what you've already done ;-)

[alreadydone]

Hi, thanks for the feedback! My main purpose of making an inductive definition IsFiniteLength is to get the nice induction principle, which is used to prove noether/artinianity. This was also my answer to Kevin's questioning about the definition on Zulip. If you define IsFiniteLength using CompositionSeries, you can still prove the same induction principle using an induction similar to my proof of isFiniteLength_of_exists_compositionSeries, but why not get it directly if you can.