English
If hv is LI and i is a map and j is a monoid hom with suitable preservation of zero, then j ∘ v is LI.
Русский
Если hv линейно независимо и i, j удовлетворяют условиям сохранения нуля, то j ∘ v линейно независимо.
LaTeX
$$$\\text{LinearIndependent } R\\ v \\\\rightarrow i:\\ R'\\to R,\\ j:\\ M\\to_{+} M'\\text{, с условиями} \\,\\Rightarrow \\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 send non-zero elements to non-zero elements, 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'`. -/
theorem map_of_injective_injective {R' M' : Type*} [Ring R'] [AddCommGroup M'] [Module R' M']
(hv : LinearIndependent R v) (i : R' → R) (j : M →+ M') (hi : ∀ r, i r = 0 → r = 0) (hj : ∀ m, j m = 0 → m = 0)
(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' H s hs
simp_rw [comp_apply, ← hc, ← map_sum] at H
exact hi _ <| hv _ _ (hj _ H) s hs
