English
If f is a linear map and hv asserts that f ∘ v is linearly independent, then the submodule spanned by the range of v is disjoint from the kernel of f.
Русский
Если линейное отображение f тождественно и hv утверждает, что f ∘ v линейно независимо, то подмодули, порожденный образами v, и ядро f пересекаются тривиально.
LaTeX
$$Disjoint (span_R (range v)) (ker f)$$
Lean4
/-- If `v` is an injective family of vectors such that `f ∘ v` is linearly independent, then `v`
spans a submodule disjoint from the kernel of `f`.
TODO : `LinearIndepOn` version. -/
theorem range_ker_disjoint {f : M →ₗ[R] M'} (hv : LinearIndependent R (f ∘ v)) :
Disjoint (span R (range v)) (LinearMap.ker f) :=
by
rw [LinearIndependent, Finsupp.linearCombination_linear_comp] at hv
rw [disjoint_iff_inf_le, ← Set.image_univ, Finsupp.span_image_eq_map_linearCombination, map_inf_eq_map_inf_comap,
(LinearMap.ker_comp _ _).symm.trans (LinearMap.ker_eq_bot_of_injective hv), inf_bot_eq, map_bot]
