Duality of Vector Spaces (2017)

In other words: if vectors are column vectors, then covectors are row vectors, and vice versa. In this case, taking the dual is transposing your vectors, and the transpose of a transpose gives you back the original vectors.

But mathematicians try to build the most general, most abstract framework, which doesn't rely on the specifics of a concrete example (i.e. the dot product of finite-dimensional real vectors).

You are asking if every covector f can be written as dot(v,—) for some v.

This is true for finite-dimensional spaces (take v = f(e1)e1 + ... + f(en)en, where e1,...,en is a orthogonal basis for dot). Since v is unique, this gives an isomorphism between V and V٭ and applying the same argument to V٭ and V٭٭, those are isomorphic, so V and V٭٭ are also isomorphic. But the isomorphism depends on the choice of dot.

However the map V -> V٭٭ does not depend on the choice of dot. The type is V -> (V->F) -> F so this is just (reversed) function application. You can easily show this is injective. Furthermore when V is finite-dimensional, we know from above that dim(V)=dim(V٭)=dim(V٭٭), so we know in this case it is also an iso.

(dot v) is a member of the dual space. To double it up with dual dual, and to do it with the same partial application construction, we need to introduce an inner product on the dual space.

ddot :: (V F -> F) -> (V F -> F) -> F

ddot (dot v) :: (V F -> F) -> F

To identify these things, we need a bijection and we need vector space properties to match up (inner product, addition, and scaling). Starting with an inner product:

dddot (ddot (dot v)) (ddot (dot w)) = dot v w

Then the bijection:

phi :: V F -> (V F -> F) -> F

phi_inv :: ((V F -> F) -> F) -> V F

phi v = ddot (dot v)

phi_inv (ddot (dot v)) = v

Then we'd also have to show that phi (v+w) = (phi v) +* (phi w) and the same for dual space addition and scaling phi (a v) = a phi v, etc, but it's starting to get less fun, so that's left as an exercise for the reader/next commenter. I think they fall out of my dddot definition.

A gotcha here is that my dual space isn't the entire type (V F -> F), just the subset that's in the image of dot (linear transformations). That's why we can do the pattern matching in my definition of phi_inv.

That's the typey way to do it and it was fun to think through. What's easier is to just think of the currying as the transpose operation and multiplication. Then appeal to transpose transpose = identity. It's handwavier, but still has the same elements if you flesh it out, I think.

All that said, it's not the easiest mental model. My mental model is that vectors and one forms are for measuring against each other. You have a vector v and a form x. You apply x to measure how much v is in that direction. Like, your vector might be some coordinateless physical thing, and your one form is "meters per second in the north direction" and you can apply your form to the vector to get a good old fashioned number for its north component in meters per second.

The difference comes in that for Hilbert spaces, "dual" is usually taken to mean only the continuous linear functionals.