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 (V:f|D) and (V:g|D) and a scalar s in S:

- f+g
- = (V: f(d)+g(d) ←d |D)
- s.f
- = (V: s.f(d) ←d |D)

Note that no structure of any kind is assumed on D. Furthermore, for each d in D, we obtain a mapping, (V: f(d) ←f :{mappings (V:|D)}), which is manifestly linear: it is called evaluate(d). Thus we embed D in {linear (V: |(mapping (V:|D)})}, for each linear space V, using evaluate.

Now, replace D with a second S-linear space, U, and consider some (V:f|U). 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 (V:|U)} is a sub-space of {(V:|U)}. We have U
embedded in {linear (V: |{mapping (V:|U)})} as before (for D), by (: f(u)
←f :): in general, mappings (V:f|U) 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 (: (V: evaluate(u) :{linear (V:|U)}) ←u
|U) is a linear embedding of U in {linear (V:|{linear (V:|U)})}.

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 (S:|U)} is
known as dual(U). Evaluation embeds U in {linear (S: |{linear (S:|U)})} =
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 (V: |{linear (V:|S)})}. Now, given linear (V:f|S) 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 ({linear (V:|S)}: (V: s.v ←s |S) ←v |V) with inverse (V: f(1) ←f :{linear (V:|S)}) between V and {linear (V:|S)}, which turns evaluation into S's embedding in {linear (V: |V)} given by (s.v ←v) ←s, 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.