Hacker News Reader

You said even when dim V is finite you need a basis to find an isomorphism with V**. But that’s not true. You’re right if you mean V*, but not the bidual.

View on HN

I'm talking about a practical task. Not an abstract existence result.

It’s not that abstract. You can literally write down the isomorphism: v —> [e_v: V* —> F, e_v(f) = f(v)].

Are you even trying to understand my point? Yes, in that direction, explicitly constructing an element of the bidual of V from an element of V is easy. To explicitly find an element of V from the element of the bidual, you need to choose a basis. Just try it, come on! Write down the inverse isomorphism. Let \alpha be an element of V**. Then v \in V such that f(v) = \alpha (where f is the isomorphism you wrote down) is given by...?

I will help you: if (e_i) is a basis of V and (e_i^*) is its dual basis, then v = \sum_i \alpha(e_i^*) e_i. Can you find such a formula without mentioning the word "basis"?

```case class Bidual[V](v: V) { def apply(f: Dual[V]) = f(v) }

def unwrap[V](ff: Bidual[V]): V = ff.v```

There's both directions of the isomorphism explicitly defined in a programming language. No choice of basis needed to define the maps, only to prove that the constructor for Bidual really gives you all linear functionals on the dual.

Reply on news.ycombinator.com