feat: finitely related modules

[YaelDillies]

Define finitely related modules, which are modules admitting a presentation with finitely many relations.

This notion does not seem to appear in the literature. However it is useful to unify the two main cases where a module M is separated by its dual M →ₗ[R] R:

• when M is free
• when M is finitely generated

Co-authored-by: Calle Sönne [email protected]

---

• depends on: [Merged by Bors] - chore(FreeModule): clean up #23996
• depends on: feat: ι →₀ R is a finite R-module iff ι is finite #23997

[github-actions]

PR summary 38b4dba78f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ FinitePresentation
+ FinitePresentation.equiv_quotient
+ FinitePresentation.exists_fin
+ FinitePresentation.fg_ker
+ FinitePresentation.fg_ker_iff
+ FinitePresentation.of_equiv
+ FinitePresentation.of_finite
+ FinitePresentation.of_finite_isFinitelyRelated
+ Free.to_isFinitelyRelated
+ IsFinitelyRelated
+ IsFinitelyRelated.exists_set
+ IsFinitelyRelated.of_set
+ _root_.LinearEquiv.finitePresentation_iff
+ finitePresentation_iff_finite
+ finitePresentation_iff_finite_isFinitelyRelated
+ finitePresentation_of_finite
+ finitePresentation_of_free
+ finitePresentation_of_free_of_surjective
+ finitePresentation_of_ker
+ finitePresentation_of_projective
+ finitePresentation_of_projective_of_exact
+ finitePresentation_of_split_exact
+ finitePresentation_of_surjective
+ finite_finsupp
+ instance (priority := 100) FinitePresentation.to_finite [h : FinitePresentation R M] :
+ instance (priority := 100) FinitePresentation.to_isFinitelyRelated [FinitePresentation R M] :
+ instance : FinitePresentation R (ι → R) := finitePresentation_of_projective _ _
+ instance : FinitePresentation R (ι →₀ R) := finitePresentation_of_projective _ _
+ instance : FinitePresentation R R := finitePresentation_of_projective _ _
+ isFinitelyRelated_iff_exists_set
+ linearCombination_subtypeVal
+ linearIndependent_single_one
- LinearEquiv.finitePresentation_iff
- Module.FinitePresentation
- Module.FinitePresentation.equiv_quotient
- Module.FinitePresentation.exists_fin
- Module.FinitePresentation.fg_ker
- Module.FinitePresentation.fg_ker_iff
- Module.FinitePresentation.of_equiv
- Module.finitePresentation_iff_finite
- Module.finitePresentation_of_finite
- Module.finitePresentation_of_free
- Module.finitePresentation_of_free_of_surjective
- Module.finitePresentation_of_ker
- Module.finitePresentation_of_projective
- Module.finitePresentation_of_projective_of_exact
- Module.finitePresentation_of_split_exact
- Module.finitePresentation_of_surjective
- instance (priority := 100) [h : Module.FinitePresentation R M] : Module.Finite R M := by
- instance : Module.FinitePresentation R (ι → R) := Module.finitePresentation_of_projective _ _
- instance : Module.FinitePresentation R (ι →₀ R) := Module.finitePresentation_of_projective _ _
- instance : Module.FinitePresentation R R := Module.finitePresentation_of_projective _ _

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] - chore(FreeModule): clean up #23996
• feat: ι →₀ R is a finite R-module iff ι is finite #23997
  By Dependent Issues (🤖). Happy coding!