[Merged by Bors] - feat(Mathlib/LinearAlgebra): embeddings of free modules

[artie2000]

• A free module embeds linearly into any module of strictly greater rank
• A free module embeds linearly into another free module iff the other one has greater rank

The proofs have been generalised as much as possible.

Co-authored-by: Aaron Liu aaronliu2008@outlook.com

---

[github-actions]

PR summary 09037d340e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ exists_linearMap_injective_of_lift_rank_lt
+ exists_linearMap_injective_of_linearIndependent_of_lift_rank_le
+ exists_linearMap_injective_of_linearIndependent_of_rank_le
+ exists_linearMap_injective_of_rank_lt
+ exists_set_linearIndependent_of_lt_lift_rank
+ finrank_le_iff_exists_linearMap
+ injective_constr_of_linearIndependent
+ lift_rank_le_iff_exists_linearMap
+ rank_le_iff_exists_linearMap
+-+ exists_set_linearIndependent_of_lt_rank

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

[riccardobrasca]

There the comment by Eric, but otherwise LGTM, thanks!

bors d+

[mathlib-bors]

✌️ artie2000 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

Suggested change

	theorem exists_set_of_lt_lift_rank {α : Cardinal.{w}}
	theorem exists_linearIndepOn_of_lt_lift_rank {α : Cardinal.{w}}

[artie2000]

going with exists_set_linearIndependent_of_lt_lift_rank by analogy with existing exists_set_linearIndependent_of_lt_rank

[artie2000]

How do I un-delegate?

[riccardobrasca]

bors d-

[mathlib-bors]

🚫 All delegations have been removed from this PR. To re-add a delegation, reply with bors d+ (to delegate the PR author) or bors d=list,of,github,usernames to delegate multiple users.

[Copilot]

Pull request overview

This PR extends Mathlib’s dimension theory for free modules by proving existence/characterization results for injective linear maps (linear embeddings) between free modules in terms of Module.rank/finrank, with universe-polymorphic (“lift”) statements where appropriate.

Changes:

• Add existence theorems producing injective linear maps M →ₗ[R] N from rank inequalities, and rank/finrank ≤ characterizations via existence of an injective linear map.
• Generalize/move “existence of a linearly independent set of prescribed cardinality below rank” into Dimension/Basic.lean, and deprecate the old lemma location/name in Dimension/Finite.lean.
• Add a new basis lemma showing Basis.constr is injective when its images of basis vectors are linearly independent (used to build embeddings).

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.

File	Description
Mathlib/LinearAlgebra/Dimension/Free.lean	Adds rank-/lift-rank-based existence of injective linear maps and rank ≤ / finrank ≤ iff-exists-injective-linear-map lemmas (under StrongRankCondition where needed).
Mathlib/LinearAlgebra/Dimension/Finite.lean	Removes the old exists_set_linearIndependent_of_lt_rank lemma and replaces it with a deprecated alias to the new canonical lemma in Module.
Mathlib/LinearAlgebra/Dimension/Basic.lean	Introduces Module.exists_set_linearIndependent_of_lt_lift_rank and Module.exists_set_linearIndependent_of_lt_rank, making the construction available in the core dimension file.
Mathlib/LinearAlgebra/Basis/Basic.lean	Adds Module.Basis.injective_constr_of_linearIndependent, enabling injectivity of Basis.constr from linear independence of assigned vectors.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[riccardobrasca]

@eric-wieser are you happy with this?

[riccardobrasca]

LGTM. @eric-wieser can you have another quick look? Thanks!

[eric-wieser]

bors merge

Thanks!

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step