Linear maps prescribed on a linearly independent family #
This file proves that a linearly independent family of vectors can be sent to any family of
values by a linear map: given hv : LinearIndependent K v and w : ι → W, there is a linear map
f with f (v i) = w i for every i. The map is built on the span of v by
Module.Basis.constr and extended to the whole space by LinearMap.exists_extend.
Main results #
LinearIndependent.exists_linearMap_apply_eq: a linear map with prescribed values on a linearly independent family.
theorem
LinearIndependent.exists_linearMap_apply_eq
{ι : Type u_1}
{K : Type u_2}
{V : Type u_3}
{W : Type u_4}
[Field K]
[AddCommGroup V]
[Module K V]
[AddCommGroup W]
[Module K W]
{v : ι → V}
(hv : LinearIndependent K v)
(w : ι → W)
:
∃ (f : V →ₗ[K] W), ∀ (i : ι), f (v i) = w i
A linear map may take any values on a linearly independent family.