feat(Mathlib/LinearAlgebra): embeddings of free modules (#37919)

* 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>

Author: artie2000

Mathlib/LinearAlgebra/Basis/Basic.lean

@@ -93,6 +93,12 @@ protected lemma linearIndepOn (s : Set ι) : LinearIndepOn R b s :=
 protected theorem ne_zero [Nontrivial R] (i) : b i ≠ 0 :=
   b.linearIndependent.ne_zero i
 
+theorem injective_constr_of_linearIndependent
+    [Semiring R₂] [Module R₂ M'] [SMulCommClass R R₂ M'] {v : ι → M'}
+    (hv : LinearIndependent R v) : Injective (b.constr R₂ v) :=
+  fun _ _ hab ↦ b.repr.injective <| hv.finsuppLinearCombination_injective <| by
+    simpa [constr_def] using hab
+
 end Properties
 
 variable {v : ι → M} {x y : M}

Mathlib/LinearAlgebra/Dimension/Basic.lean

@@ -108,8 +108,23 @@ end LinearIndependent
 
 namespace Module
 
-variable [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R]
+variable [Semiring R] [AddCommMonoid M] [Module R M]
+
+theorem exists_set_linearIndependent_of_lt_lift_rank {c : Cardinal.{w}}
+    (h : Cardinal.lift.{v} c < Cardinal.lift.{w} (Module.rank R M)) :
+    ∃ s : Set M, Cardinal.lift.{w} #s = Cardinal.lift.{v} c ∧ LinearIndepOn R id s := by
+  rcases Cardinal.lt_lift_iff.mp h with ⟨c', hc', hcc'⟩
+  rcases exists_lt_of_lt_ciSup (by simpa [← hcc', Module.rank_def] using h) with ⟨⟨s, hs⟩, h⟩
+  rcases Cardinal.le_mk_iff_exists_subset.mp h.le with ⟨t, hst, ht⟩
+  exact ⟨t, by simp [ht, hcc'], hs.mono hst⟩
+
+theorem exists_set_linearIndependent_of_lt_rank {c : Cardinal.{v}} (h : c < Module.rank R M) :
+    ∃ s : Set M, #s = c ∧ LinearIndepOn R id s := by
+  simpa using exists_set_linearIndependent_of_lt_lift_rank (Cardinal.lift_lt.mpr h)
+
+variable [Nontrivial R]
 
+-- TODO: the forward directions of the next few theorems don't need [Nontrivial R]
 /-- Note: if the rank of a module is infinite, it may not contain a linear independent subset
 with cardinality equal to the rank, see
 https://mathoverflow.net/questions/263020/maximum-cardinal-of-a-set-of-linearly-independent-vectors-in-a-module. -/

Mathlib/LinearAlgebra/Dimension/Finite.lean

@@ -187,12 +187,6 @@ theorem setFinite [Module.Finite R M] {b : Set M}
 
 end LinearIndependent
 
-lemma exists_set_linearIndependent_of_lt_rank {n : Cardinal} (hn : n < Module.rank R M) :
-    ∃ s : Set M, #s = n ∧ LinearIndepOn R id s := by
-  obtain ⟨⟨s, hs⟩, hs'⟩ := exists_lt_of_lt_ciSup' (hn.trans_eq (Module.rank_def R M))
-  obtain ⟨t, ht, ht'⟩ := le_mk_iff_exists_subset.mp hs'.le
-  exact ⟨t, ht', hs.mono ht⟩
-
 lemma exists_finset_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.rank R M) :
     ∃ s : Finset M, s.card = n ∧ LinearIndepOn R id (s : Set M) := by
   rcases hn.eq_or_lt with h | h
@@ -206,6 +200,9 @@ lemma exists_finset_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.ra
     cases nonempty_fintype s
     exact ⟨s.toFinset, by simpa using hs, by simpa⟩
 
+@[deprecated (since := "2026-04-13")]
+alias exists_set_linearIndependent_of_lt_rank := Module.exists_set_linearIndependent_of_lt_rank
+
 lemma exists_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.rank R M) :
     ∃ f : Fin n → M, LinearIndependent R f :=
   have ⟨_, hs, hs'⟩ := exists_finset_linearIndependent_of_le_rank hn

Mathlib/LinearAlgebra/Dimension/Free.lean

@@ -70,13 +70,52 @@ theorem Module.finrank_mul_finrank : finrank F K * finrank K A = finrank F A :=
 end Tower
 
 variable {R : Type u} {S : Type*} {M M₁ : Type v} {M' : Type v'}
-variable [Semiring R] [StrongRankCondition R]
+variable [Semiring R]
 variable [AddCommMonoid M] [Module R M] [Module.Free R M]
 variable [AddCommMonoid M'] [Module R M'] [Module.Free R M']
 variable [AddCommMonoid M₁] [Module R M₁] [Module.Free R M₁]
 
 namespace Module.Free
 
+variable {N : Type v} [AddCommMonoid N] [Module R N]
+variable {N' : Type v'} [AddCommMonoid N'] [Module R N']
+
+theorem exists_linearMap_injective_of_linearIndependent_of_lift_rank_le
+    {ι : Type w} {v : ι → N'} (hv : LinearIndependent R v)
+    (cnd : Cardinal.lift.{w} (Module.rank R M) ≤ Cardinal.lift.{v} #ι) :
+    ∃ f : M →ₗ[R] N', Function.Injective f := by
+  nontriviality M
+  have := Module.nontrivial R M
+  rcases Module.Free.exists_set R M with ⟨_, ⟨B⟩⟩
+  replace cnd := (Cardinal.lift_le.2 B.linearIndependent.cardinal_le_rank).trans cnd
+  rw [Cardinal.lift_mk_le'] at cnd
+  rcases cnd with ⟨i, hi⟩
+  refine ⟨B.constr ℕ (v ∘ i), B.injective_constr_of_linearIndependent (hv.comp _ hi)⟩
+
+theorem exists_linearMap_injective_of_linearIndependent_of_rank_le
+    {ι : Type v} {v : ι → N} (hv : LinearIndependent R v) (cnd : Module.rank R M ≤ #ι) :
+    ∃ f : M →ₗ[R] N, Function.Injective f :=
+  exists_linearMap_injective_of_linearIndependent_of_lift_rank_le hv (by simpa using cnd)
+
+theorem exists_linearMap_injective_of_lift_rank_lt
+    (cnd : Cardinal.lift.{v'} (Module.rank R M) < Cardinal.lift.{v} (Module.rank R N')) :
+    ∃ f : M →ₗ[R] N', Function.Injective f := by
+  rcases exists_set_linearIndependent_of_lt_lift_rank cnd with ⟨s, hs, hs₂⟩
+  exact exists_linearMap_injective_of_linearIndependent_of_lift_rank_le
+    hs₂.linearIndependent hs.symm.le
+
+theorem exists_linearMap_injective_of_rank_lt (cnd : Module.rank R M < Module.rank R N) :
+    ∃ f : M →ₗ[R] N, Function.Injective f :=
+  exists_linearMap_injective_of_lift_rank_lt (by simpa using cnd)
+
+end Module.Free
+
+section StrongRankCondition
+
+variable [StrongRankCondition R]
+
+namespace Module.Free
+
 variable (R M)
 
 /-- The rank of a free module `M` over `R` is the cardinality of `ChooseBasisIndex R M`. -/
@@ -105,6 +144,23 @@ open Module.Free
 
 open Cardinal
 
+theorem lift_rank_le_iff_exists_linearMap :
+    Cardinal.lift.{v'} (Module.rank R M) ≤ Cardinal.lift.{v} (Module.rank R M') ↔
+    ∃ f : M →ₗ[R] M', Function.Injective f where
+  mp h := by
+    rcases Module.Free.exists_set R M' with ⟨_, ⟨B⟩⟩
+    exact exists_linearMap_injective_of_linearIndependent_of_lift_rank_le B.linearIndependent
+      (B.mk_eq_rank''.symm ▸ h)
+  mpr := fun ⟨f, hf⟩ ↦ LinearMap.lift_rank_le_of_injective f hf
+
+theorem rank_le_iff_exists_linearMap :
+    Module.rank R M ≤ Module.rank R M₁ ↔ ∃ f : M →ₗ[R] M₁, Function.Injective f := by
+  simp [← lift_rank_le_iff_exists_linearMap]
+
+theorem finrank_le_iff_exists_linearMap [Module.Finite R M] [Module.Finite R M'] :
+    finrank R M ≤ finrank R M' ↔ ∃ f : M →ₗ[R] M', Function.Injective f := by
+  simp [← lift_rank_le_iff_exists_linearMap, ← finrank_eq_rank]
+
 /-- Two vector spaces are isomorphic if they have the same dimension. -/
 theorem nonempty_linearEquiv_of_lift_rank_eq
     (cnd : Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')) :
@@ -306,6 +362,8 @@ noncomputable def _root_.LinearEquiv.smul_id_of_finrank_eq_one (d1 : Module.finr
 
 end Module
 
+end StrongRankCondition
+
 namespace Algebra
 
 instance (R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S]