English
If hv is LI, i is surjective, j preserves zero, and hc expresses compatibility with scalar action, then j ∘ v is LI.
Русский
Если hv линейно независимо, i сюръективно, j сохраняет нуль, и hc выражает совместимость со скалярным действием, тогда j ∘ v линейно независимо.
LaTeX
$$$\\text{LinearIndependent } R\\ v \\\\rightarrow i:\\ R'\\to R\\, (\\text{surjective}) \\, j:\\ M\\to M' \\, (hc) \\\\Rightarrow \\text{LinearIndependent } R' (j \\circ v)$$$
Lean4
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a surjective map which maps zero to zero,
`j : M →+ M'` is a monoid map which sends non-zero elements to non-zero elements, such that the
scalar multiplications on `M` and `M'` are compatible, 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_surjective_injective {R' M' : Type*} [Semiring R'] [AddCommMonoid M'] [Module R' M']
(hv : LinearIndependent R v) (i : R → R') (j : M →+ M') (hi : Surjective i) (hj : ∀ m, j m = 0 → m = 0)
(hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : LinearIndependent R' (j ∘ v) :=
hv.map_of_surjective_injectiveₛ i _ hi ((injective_iff_map_eq_zero _).mpr hj) hc
