feat(linear_algebra/free_module): a set of linearly independent vecto…

…rs over a ring S is also linearly independent over a subring R of S (#6993)



Zulip:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60algebra_map.2Einjective.2Elinear_independent.60

src/linear_algebra/free_module.lean

@@ -335,3 +335,11 @@ lemma submodule.exists_is_basis_of_le_span
 submodule.exists_is_basis_of_le le (is_basis_span hb)
 
 end principal_ideal_domain
+
+/-- A set of linearly independent vectors in a module `M` over a semiring `S` is also linearly
+independent over a subring `R` of `K`. -/
+lemma linear_independent.restrict_scalars_algebras {R S M ι : Type*} [comm_semiring R] [semiring S]
+  [add_comm_monoid M] [algebra R S] [semimodule R M] [semimodule S M] [is_scalar_tower R S M]
+  (hinj : function.injective (algebra_map R S)) {v : ι → M} (li : linear_independent S v) :
+  linear_independent R v :=
+linear_independent.restrict_scalars (by rwa algebra.algebra_map_eq_smul_one' at hinj) li

src/linear_algebra/linear_independent.lean

@@ -260,6 +260,22 @@ begin
   simpa only [this, zero_smul, zero_add] using total_eq
 end
 
+/-- A set of linearly independent vectors in a semimodule `M` over a semiring `K` is also linearly
+independent over a subring `R` of `K`.
+The implementation uses minimal assumptions about the relationship between `R`, `K` and `M`.
+The version where `K` is an `R`-algebra is `linear_independent.restrict_scalars_algebras`.
+ -/
+lemma linear_independent.restrict_scalars [semiring K] [smul_with_zero R K] [semimodule K M]
+  [is_scalar_tower R K M]
+  (hinj : function.injective (λ r : R, r • (1 : K))) (li : linear_independent K v) :
+  linear_independent R v :=
+begin
+  refine linear_independent_iff'.mpr (λ s g hg i hi, hinj (eq.trans _ (zero_smul _ _).symm)),
+  refine (linear_independent_iff'.mp li : _) _ _ _ i hi,
+  simp_rw [smul_assoc, one_smul],
+  exact hg,
+end
+
 section subtype
 /-! The following lemmas use the subtype defined by a set in `M` as the index set `ι`. -/