[senderista]

No, the isomorphism between V and V** (for finite-dimensional V) is canonical. The canonical isomorphism T:V->V** is easy to construct: map a vector v in V to the element of V** which takes an element w from V* and applies it to v: T(v)(w) = w(v).

[g15jv2dp]

GP is giving you an element of V**. You want to turn it into a vector. To do that, please make the inverse isomorphism explicit without using a basis. I'll wait...

[senderista]

Why? All I need to prove is that I have a canonical linear map going in one direction, and that this map is a bijection. (Since I already constructed such a bijection, I could just answer "for any z in V**, take the unique element v in V such that for all w in V*, w(v) = z(w)".) Do you disagree that I provided such a map? You are correct that V** is not isomorphic to V when V is infinite-dimensional, but your statement that "when dim V is finite, you need to choose a basis of V to find an isomorphism with the bidual" is incorrect. This is elementary textbook stuff (e.g. first chapter of Wald's GR book), so I won't argue further.

[g15jv2dp]

I responded to a sibling comment with an explanation: https://news.ycombinator.com/item?id=41234913 But good on you for the condescension even though you didn't understand my point ;)

[xanderlewis]

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.

[g15jv2dp]

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

[xanderlewis]

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

[g15jv2dp]

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"?

[ndriscoll]

```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.