English
If v is linearly independent, i is injective, j is an injective linear map, and the compatibility condition holds, then j ∘ v is linearly independent over the target ring R'.
Русский
Если v линейно независимо, i инъективно, j — инъекционное линейное отображение и соблюдается совместимость скаляров, тогда j ∘ v линейно независимо над R'.
LaTeX
$$$\text{LinearIndependent}_{R'}(j \circ v)$$$
Lean4
/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is a map, `j : M →+ M'` is a monoid map,
such that they are both injective, and compatible with the scalar
multiplications on `M` and `M'`, then `j` sends linearly independent families of vectors to
linearly independent families of vectors. As a special case, taking `R = R'`
it is `LinearIndependent.map_injOn`.
TODO : `LinearIndepOn` version. -/
theorem map_of_injective_injectiveₛ {R' M' : Type*} [Semiring R'] [AddCommMonoid M'] [Module R' M']
(hv : LinearIndependent R v) (i : R' → R) (j : M →+ M') (hi : Injective i) (hj : Injective j)
(hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : LinearIndependent R' (j ∘ v) :=
by
rw [linearIndependent_iff'ₛ] at hv ⊢
intro S r₁ r₂ H s hs
simp_rw [comp_apply, ← hc, ← map_sum] at H
exact hi <| hv _ _ _ (hj H) s hs
