For any collection D and any S-linear space V, the S-linear structure of V induces one on the collection of mappings from D to V by, given (D|f:V) and (D|g:V) and a scalar s in S:
Note that no structure of any kind is assumed on D. Furthermore, for each d in D, we obtain a mapping, ({(D|:V)}: f-> f(d) :V), which is manifestly linear: it is called evaluate(d). Thus we embed D in {linear ({(D|:V)}| :V)} using evaluate.
Now, replace D with a second S-linear space, U, and consider some (U|f:V). Given u and w in U and a scalar, s: examine f(u+w) and f(s.u) in V and compare them to f(u)+f(w) and s.f(u), respectively. If the results agree for all u, w, s as appropriate, the mapping f is described as linear: it respects linear structure.
Note that the definitions of addition and scaling on functions to V imply that every sum of linear maps is linear and scaling a linear map also yields a linear map. So {linear (U|:V)} is a sub-space of {(U|:V)}. We have U embedded in {linear ({(U|:V)}| :V)} as before (for D), u-> evaluate(u) = (f-> f(u)): in general, mappings (U|f:V) aren't linear, so evaluate(u+w,f) = f(u+w) need not be equal to f(u)+f(w) = evaluate(u,f)+evaluate(w,f); however, when f is linear, these are equal and evaluate(u+w) agrees with evaluate(u)+evaluate(w). Thus (U| u-> ({linear (U|:V)}: evaluate(u) :V) :) is a linear embedding of U in {linear ({linear (U|:V)}| :V)}.
Linear algebra takes the view that linear maps from S-linear U to S suffice
to tell us everything about
U and linear maps from U to other S-linear
spaces: so consider the case V=S. The collection {linear (U|:S)} is known as
dual(U). Evaluation embeds U in {linear ({linear (U|:S)}| :S)} = dual(dual(U)),
and there is a strong sense in which the resulting image of U, which I refer to
as U when being fussy, is isomorphic to U and for all practical
purposes
is all of dual(dual(U)). [U is only truly all of
dual(dual(U)) when U is finite-dimensional: otherwise, however, U is
still dense in dual(dual(U)).]
By contrast, when U=S, evaluation embeds S in {linear ({linear (S|:V)}| :V)}. Now, given linear (S|f:V) we have, for any scalar s, f(s) = f(s.1) = s.f(1) by linearity, so f is wholly determined by f(1): we get an isomorphism (V| v-> (S| s-> s.v :V) :{linear (S|:V)}) with inverse ({linear (S|:V)}| f-> f(1) :V) between V and {linear (S|:V)}, which turns evaluation into S's embedding in {linear (V| :V)} given by s-> (v-> s.v), which is just S's multiplicative action on V. In particular, with V=S, S is naturaly isomorphic to {S-linear (S|:S)} = dual(S).
Written by Eddy.