draft(Module): Module length is additive in short exact sequences

[Raph-DG]

In this PR, we define the module length to be the krull dimension of the lattice of submodules and prove that it is additive in short exact sequences. Relies on #22069, #22036 and #21869

---

• depends on: [Merged by Bors] - feat(Set): Added some simple set lemmas #22036
• depends on: feat(LinearMap): Added lemmas relating kernels of linear maps to Submodule.map #22069
• depends on: feat(Order): Trimmed length of a RelSeries  #21869

[github-actions]

[lint-style (comment with "bot fix style" to have the bot commit all style suggestions)] _{reported by reviewdog 🐶}

Suggested change

	· let n' : Fin (rs.length) := {val := n, isLt := by rw[o] ; exact lt_add_one n}
	· let n' : Fin (rs.length) := {val := n, isLt := by rw[o]; exact lt_add_one n}

[github-actions]

PR summary 185ec73ce4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Order.TrimmedLength (new file)	1219
Mathlib.Algebra.Module.Length (new file)	1223

---

Declarations diff

+ Module.length
+ Module.length_additive
+ Module.length_additive_of_quotient
+ RelSeries.length_eq_trimmedLength_iff
+ RelSeries.moduleLength_ge_trimmedLength
+ RelSeries.trim
+ RelSeries.trimmedLength
+ RelSeries.trimmedLength_additive
+ RelSeries.trimmedLength_eraseLast_le
+ RelSeries.trimmedLength_eraseLast_of_eq
+ RelSeries.trimmedLength_eraseLast_of_lt
+ RelSeries.trimmedLength_exists_le
+ RelSeries.trimmedLength_le_length
+ add_iSup
+ coe_unbotD_iSup
+ iSup_add
+ iSup_le_add
+ instance (rs : RelSeries (α := α) (· ≤ ·)) :
+ ker_inf_lt_ker_inf
+ ker_inter_mono_of_map_eq
+ map_lt_map_of_ker_inf_eq
+ map_lt_map_or
+ map_mono_of_ker_inter_eq
+ ne_map_or_ne_kernel_inter_of_lt
+ range_inter_ssubset_iff_preimage_ssubset
+ rel_of_le
+ ssubset_iff_exists

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.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Set): Added some simple set lemmas #22036
• feat(LinearMap): Added lemmas relating kernels of linear maps to Submodule.map #22069
• feat(Order): Trimmed length of a RelSeries  #21869
  By Dependent Issues (🤖). Happy coding!

[erdOne]

I'm not entirely sure about this approach. I think we should show that the length is equal to the length of a composition series and then this result is immediate, instead of developing a whole new API reproving Jordan-Holder.

[Raph-DG]

I'm not entirely sure about this approach. I think we should show that the length is equal to the length of a composition series and then this result is immediate, instead of developing a whole new API reproving Jordan-Holder.

So I do agree that this is a lot of API to develop for this task (though I admit I can't yet see how what's proven here would imply Jordan Holder without some more work). We considered using this Jordan-Holder proof at one point, but we went for this other one because we thought on paper it looked like not much more work and that it would give the case for infinite length modules for free. But I agree that this small advantage over the Jordan-Holder based proof is definitely not worth all this API development.

That said, I still think the API itself is worthwhile for reasoning about chains of submodules because it makes moving them around with maps easier. I could be wrong about this applicability of the API because of my lack of experience, but if it is the case that this API is independently useful then I think it's less clear cut which approach to the proof we should use, because the actual proof of the main theorem here is fairly short once all the other stuff is built up.