English
For M, N submodules of S with a linear disjointness K, the span of the image of v under a linear map is disjoint from the kernel, under the appropriate flatness assumptions.
Русский
Для M и N подмодулей S при линейной взаимной независимости сохраняется разобщенность порожденного образа и ядра, при необходимых условиях плоскости.
LaTeX
$$Disjoint (span_R (range v)) (ker f)$$
Lean4
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a surjective map,
and `j : M →+ M'` is an injective monoid map, 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_injOn`.
TODO : `LinearIndepOn` version. -/
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 : Injective j)
(hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : LinearIndependent R' (j ∘ v) :=
by
obtain ⟨i', hi'⟩ := hi.hasRightInverse
refine hv.map_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_
· apply_fun i at h
rwa [hi', hi'] at h
rw [hc (i' r) m, hi']
